Graphen mit entscheidbaren Logiken

• Antragsteller: Professor Dr. Markus Lohrey
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2004 bis 2008
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 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-Verfahren: Schwerpunktprogramme
• Teilprojekt zu: SPP 1126: Algorithmik großer und komplexer Netzwerke
• Beteiligte Person: Professor Dr. Volker Diekert