Nichtklassische Logik auf Strukturen mit Datenwerten

• Antragsteller: Professor Dr. Thomas Schwentick
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2008 bis 2014
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 75507430

Strukturen mit Markierungen aus einem endlichen Wertebereich (z.B.: Strings und Bäume) spielen in der Informatik eine wichtige Rolle. Viele in der Informatik relevanten Objekte können mit solchen Strukturen modelliert werden, zum Beispiel mögliche Systemläufe in der automatischen Verifikation oder XML-Dokumente im Bereich der Datenbanktheorie. Als formale Werkzeuge stehen hier logische Formeln zur Spezifikation und Automaten zu ihrer Implementierung zur Verfügung.Im Mittelpunkt des beantragten Projektes steht die Erweiterung solcherStrukturen um Datenwerte aus einem unendlichen Wertebereich und dieEntwicklung entsprechender Werkzeuge im Bereich von Logiken,Automatenmodellen und Algorithmen. Bei den Logiken liegt der Fokusdabei auf modalen, temporalen und hybriden Logiken, die hier unter demSchlagwort "nichtklassische Logiken" zusammengefasst werden.In der Verifikation dienen Datenwerte beispielsweise der Modellierungunbeschränkter Datentypen, als Zeitwerte oder alsProzess-IDs in Multi-Prozess-Systemen. Im Bereich semistrukturierterDaten treten sie als Text- oder Attributwerte in XML-Dokumenten auf. In der Fortsetzung des Projektes sollen Modelle für verteilte Systeme mit dynamischer Prozesserzeugung und Datenlogiken mit linearer oder verzweigender Zeit entwickelt werden, die einegute Balance zwischen Ausdrucksstärke und algorithmischen Eigenschaften haben. Als Grundlage für Systeme sollen klassische zustandsbasierte Systeme und Message Sequence Charts verwendet werden. Um Szenarien mit (möglichst effizient) entscheidbaren Model-Checking-Problem zu finden, sollen Einschränkungen sowohl der verwendeten Logiken als auch der Systemmodelle hinsichtlich der Struktur der sich ergebenden Systemläufe oder Berechnungsbäume untersucht werden.

• DFG-Verfahren: Sachbeihilfen