Graphen mit entscheidbaren Logiken (GELO)

• Antragsteller: Professor Dr. Markus Lohrey
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2006 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 31332468

Das zentrale Anliegen dieses Projekts ist die Untersuchung von unendlichen Graphen mit entscheidbaren Logiken. Aufgrund zahlreicher 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. Die 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: Sachbeihilfen