Logikfragmente für unendliche und partiell-kommutative Objekte

• Antragsteller: Professor Dr. Volker Diekert
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2010 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 166222852

• Erstellungsjahr: 2020

Zusammenfassung der Projektergebnisse

Reguläre Sprachen bilden eines der Kerngebiete der theoretischen Informatik. Bei den vielfältigen Anwendungen im Bereich der formalen Verifikation steht die Korrespondenz zwischen Automaten und Logikbeschreibungen hierbei oft im Mittelpunkt. Einfachere Logikbeschreibungen lassen in vielen Fällen auch einfachere Algorithmen zu. Dies führt unmittelbar zur Untersuchung von Logikfragmenten. Für das Verständnis von Logikfragmenten haben sich algebraische Charakterisierungen in Form von endlichen Monoiden als außerst nützlich herausgestellt. Über diesen Umweg kann in einigen Fällen entschieden werden, ob eine gegebene reguläre (oder omega-reguläre) Sprache in einem bestimmten Logikfragment ausdrückbar ist. Im Rahmen dieses Projekts haben wir auf diesem Weg effektive Charakterisierungen für zahlreiche Logikfragmente erarbeitet. Eines der Highlights hierbei ist eine effektive algebraische Charakterisierung der Quantorenalternierungen innerhalb von Zweivariablenlogik FO2. Zusätzlich haben wir viele der für endliche Wörter bekannten Charakterisierungen auch auf unendliche Wörter ausgedehnt. Neben den Ergebnissen selbst sind vor allem neue Methoden und Beweistechniken ein wichtiger Beitrag dieses Projekts. Über unendlichen Wörtern liefert die Kombination von algebraischen und topologischen Eigenschaften oft direkte Verallgemeinerungen der entsprechenden Charakterisierungen über unendlichen Wörtern. Es liegt hier in der Natur der Sache, dass man stets bei den Charakterisierungen über endlichen Wörtern ansetzt, wenn man nach geeigneten Charakterisierungen über unendlichen Wörtern sucht. Nicht jede Charakterisierung und nicht jeder Beweis ist jedoch für eine solche Verallgemeinerung auf unendliche Wörter geeignet; deshalb mussten in vielen Fällen neue Beweismethoden (auch für endliche Wörter) entwickelt werden. Als ein sehr reichhaltiges Forschungsgebiet haben sich Berechnungs- und Entscheidungsprobleme mit endlichen Monoiden als Eingabe erwiesen. Für viele solcher Probleme konnten wir effiziente Algorithmen entwickeln bzw. ihre Komplexität untersuchen. Die von uns betrachteten Probleme ergeben sich zum einen aus den entsprechenden Problemen mit Automaten als Eingabe und zum anderen durch die Verallgemeinerung von endlichen auf unendliche Wörter. Da jeder Automat durch die Transformationen auf seinen Zuständen ein Monoid definiert, ist in diesem Zusammenhang auch interessant, wie sich diese Übersetzung von Automaten in Monoide auf diverse Parameter auswirkt. Wir konnten hier eine exponentielle untere Schranke für die sogenannte R-Höhe zeigen; diese Schranke gilt bereits bei einem festen Alphabet.

Projektbezogene Publikationen (Auswahl)

• Partially ordered two-way Büchi automata. Int. J. Found. Comput. Sci., 22(8):1861–1876, 2011
  M. Kufleitner and A. Lauser
  
• Around dot-depth one. Int. J. Found. Comput. Sci., 23(6):1323–1339, 2012
  M. Kufleitner and A. Lauser
  
• On logical hierarchies within FO2-definable languages. Log. Methods Comput. Sci., 8(3):1–30, 2012
  M. Kufleitner and P. Weil
  
• Omega-rational expressions with bounded synchronization delay. Theory of Computing Systems, 56:686–696, 2015
  V. Diekert and M. Kufleitner
  
• The half-levels of the fo2 alternation hierarchy. Theory Comput. Syst., 61(2):352–370, 2017
  L. Fleischer, M. Kufleitner, and A. Lauser
  
• Green’s Relations in Deterministic Finite Automata. Theory Comput. Syst., 2018
  L. Fleischer and M. Kufleitner
  
• Level two of the quantifier alternation hierarchy over infinite words. Theory of Computing Systems, 62:467–480, 2018
  M. Kufleitner and T. Walter
  
• The complexity of weakly recognizing morphisms. RAIRO-Theor. Inf. Appl., 2018
  L. Fleischer and M. Kufleitner
  
• The word problem for omega-terms over the Trotter-Weil hierarchy. Theory of Computing Systems, 62:682–738, 2018
  M. Kufleitner and J. P. Wächter
  
• The complexity of properties of transformation semigroups. International Journal of Algebra and Computation, 30(03):585–606, 2020
  L. Fleischer and T. Jack