Graphen mit entscheidbaren Logiken

• Applicant: Professor Dr. Markus Lohrey
• Subject Area: Theoretical Computer Science
• Term: from 2004 to 2008
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5430209

Das zentrale Anliegen dieses Projekts ist die Untersuchung von unendlichen Graphen mit entscheidbaren Logiken. Auf Grund potentieller Anwendungen im Bereich der Verifikation von Systemen mit unendlichen Zustandsräumen, wie sie etwa in der Softwarevalidierung oder bei der Beschreibung dynamischer Netzwerktopologien auftreten, hat dieses Gebiet in jüngster Vergangenheit wachsende Aufmerksamkeit erhalten. Unendliche Zustandsräume lassen sich adäquat durch unendliche Graphen beschreiben, während Logiken ein geeignetes Ausdrucksmittel zur Formulierung von Systemeigenschaften darstellen. Eine logikorientierte Theorie unendlicher Graphen ist jedoch erst am Entstehen und soll in diesem Projekt maßgeblich weiterentwickelt werden. Zu diesem Zweck wollen wir Antworten im Rahmen der folgenden allgemeinen Fragestellung finden: Welche Logiken sind für welche Klassen von unendlichen Graphen noch entscheidbar und wie hoch ist dabei die Berechnungskomplexität? Konkret sollen folgende Klassen von unendlichen Graphen untersucht werden: Graphen von Ersetzungssystemen, automatische Graphen, baumautomatische Graphen, Cayley-Graphen von Monoiden sowie die Graphen der Caucal-Hierarchie. Diese Graphklassen sollen untereinander und mit weiteren bereits in der Literatur betrachteten Klassen verglichen werden. Potentielle Anwendungen für die Validierung reaktiver Systeme mit unendlichen Zustandsräumen sollen in unseren Betrachtungen stets im Auge behalten werden. In einem allgemeineren Kontext betrachtet kann unsere Arbeit als ein Beitrag zur mathematischen Logik angesehen werden.

• DFG Programme: Priority Programmes
• Subproject of: SPP 1126: Algorithmics of Large and Complex Networks
• Participating Person: Professor Dr. Volker Diekert