Logical fragments for infinite and partially commutative objects
Final Report Abstract
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.
Publications
- Partially ordered two-way Büchi automata. Int. J. Found. Comput. Sci., 22(8):1861–1876, 2011
M. Kufleitner and A. Lauser
(See online at https://doi.org/10.1142/S0129054111009082) - Around dot-depth one. Int. J. Found. Comput. Sci., 23(6):1323–1339, 2012
M. Kufleitner and A. Lauser
(See online at https://doi.org/10.1142/S0129054112400552) - On logical hierarchies within FO2-definable languages. Log. Methods Comput. Sci., 8(3):1–30, 2012
M. Kufleitner and P. Weil
(See online at https://doi.org/10.2168/LMCS-8(3:11)2012) - Omega-rational expressions with bounded synchronization delay. Theory of Computing Systems, 56:686–696, 2015
V. Diekert and M. Kufleitner
(See online at https://doi.org/10.1007/s00224-013-9526-4) - The half-levels of the fo2 alternation hierarchy. Theory Comput. Syst., 61(2):352–370, 2017
L. Fleischer, M. Kufleitner, and A. Lauser
(See online at https://doi.org/10.1007/s00224-016-9712-2) - Green’s Relations in Deterministic Finite Automata. Theory Comput. Syst., 2018
L. Fleischer and M. Kufleitner
(See online at https://doi.org/10.1007/s00224-018-9847-4) - Level two of the quantifier alternation hierarchy over infinite words. Theory of Computing Systems, 62:467–480, 2018
M. Kufleitner and T. Walter
(See online at https://doi.org/10.1007/s00224-017-9801-x) - The complexity of weakly recognizing morphisms. RAIRO-Theor. Inf. Appl., 2018
L. Fleischer and M. Kufleitner
(See online at https://doi.org/10.1051/ita/2018006) - 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
(See online at https://doi.org/10.1007/s00224-017-9763-z) - The complexity of properties of transformation semigroups. International Journal of Algebra and Computation, 30(03):585–606, 2020
L. Fleischer and T. Jack
(See online at https://doi.org/10.1142/S0218196720500125)
