Non-classical Logics on Labelled Structures with Data

• Applicant: Professor Dr. Thomas Schwentick
• Subject Area: Theoretical Computer Science
• Term: from 2008 to 2014
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 75507430

• Final Report Year: 2015

Final Report Abstract

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 logische Formeln zur Spezifikation und Automaten zu ihrer Implementierung zur Verfügung. Im Mittelpunkt des beantragten Projektes standen Datenstrings und, in geringerem Maße, Datenbäume, die sich als Erweiterung von solchen Strings und Bäumen um Datenwerte aus einem unendlichen Wertebereich ergeben, und die Entwicklung zugehöriger Werkzeuge im Bereich von Logiken, Automatenmodellen und Algorithmen. Bei den Logiken lag der Fokus dabei auf modalen, temporalen und hybriden Logiken, die hier unter dem Schlagwort „nichtklassische Logiken“ zusammengefasst sind. In der automatischen Verifikation können Datenwerte beispielsweise der Modellierung von unbeschränkt vielen Prozess-IDs in Multi-Prozess-Systemen dienen. Im Bereich semistrukturierter Daten treten sie als Text- oder Attributwerte in XML-Dokumenten auf. Es wurden die Ausdrucksstärke und die algortihmischen Eigenschaften von einigen nichtklassischen Logiken für Datenstrings untersucht. Dabei wurden neue Logiken vorgeschlagen, die neben der üblichen Navigation entlang der durch die Positionen eines Strings gegebene Zeitachse auch eine auf Datenwerte bezogene Navigation verwenden können, und gezeigt, dass auf diesem Wege ausdrucksstarke Logiken mit entscheidbarem Erfüllbarkeitsproblem gewonnen werden können. Neben dem ausschließlichen Vergleich von Datenwerten bezüglich Gleichheit wurden auch Logiken für geordnete Datenwerte untersucht und ein weitgehend vollständiges Bild der Lösbarkeit des Erfüllbarkeitsproblems der Zwei-Variablenlogik fär lineare Strukturen mit geordneten Datenwerten erzielt. Im Kontext der Datenbanktheorie und der Theorie semistrukturierter Daten wurde das Zusammenspiel von Logiken für Strukturen mit Datenwerten und verschiedenen Integritätsbedingungen (Constraints) untersucht. In der zweiten Projektphase lag der Schwerpunkt auf der Entwicklung von Spezifikationsmodellen und Implementierungsmodellen für verteilte Systeme mit dynamischer Prozesserzeugung. Darüber hinaus wurde das Model-Checking-Problem für solche Modelle in Ansätzen untersucht.

Publications

• “Temporal Logics on Words with Multiple Data Values”. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010. 2010, S. 481–492
  Ahmet Kara, Thomas Schwentick und Thomas Zeume
  
• “Expressiveness of Hybrid Temporal Logic on Data Words”. In: Electr. Notes Theor. Comput. Sci. 278 (2011), S. 115–128
  Ahmet Kara und Thomas Schwentick
  
• “Two-Variable Logic and Key Constraints on Data Words”. In: International Conference on Database Theory - ICDT 2011. 2011, S. 138–149
  Matthias Niewerth und Thomas Schwentick
  
• “Feasible Automata for Two- Variable Logic with Successor on Data Words”. In: Language and Automata Theory and Applications, LATA 2012. 2012, S. 351–362
  Ahmet Kara, Thomas Schwentick und Tony Tan
  
• “Two-Variable Logic with Two Order Relations”. In: Logical Methods in Computer Science 8.1 (2012)
  Thomas Schwentick und Thomas Zeume.
  
• “Dynamic Communicating Automata and Branching High-Level MSCs”. In: Language and Automata Theory and Applications, LATA 2013. Hrsg. von Adrian Horia Dediu, Carlos Martın-Vide und Bianca Truthe. Bd. 7810. Lecture Notes in Computer Science. Springer, 2013, S. 177–189
  Benedikt Bollig, Aiswarya Cyriac, Loïc Hélouët, Ahmet Kara und Thomas Schwentick
  
• “Two-Variable Logic on 2-Dimensional Structures”. In: Computer Science Logic 2013 (CSL 2013). Hrsg. von Simona Ronchi Della Rocca. Bd. 23. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013, S. 484–499
  Amaldev Manuel und Thomas Zeume
  
• “Verification of Dynamic Register Automata”. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTT-CS 2014. 2014, S. 653–665
  Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara und Othmane Rezine
  (See online at https://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.653)