Classifications of Recognizable Infinitary Trace Languages and the Distributed Synthesis Problem

Chaturvedi, Namit; Muscholl, Anca; Thomas, Wolfgang

doi:urn:nbn:de:hbz:82-rwth-2015-003199

Classifications of Recognizable Infinitary Trace Languages and the Distributed Synthesis Problem = Klassifikationen von erkennbaren Sprachen unendlicher Spuren und das Problem der Synthese verteilter Systeme

Chaturvedi, Namit

2015

Verantwortlichkeitsangabevorgelegt von Namit Chaturvedi

ImpressumAachen : Publikationsserver der RWTH Aachen University 2015

UmfangX, 105 S. : Ill., graph. Darst.

Aachen, Techn. Hochsch., Diss., 2014

Prüfungsjahr: 2014. - Publikationsjahr: 2015

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Thomas, Wolfgang (Thesis advisor) ; Muscholl, Anca (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2014-12-10

Online
URN: urn:nbn:de:hbz:82-rwth-2015-003199
URL: http://publications.rwth-aachen.de/record/461238/files/461238.pdf
URL: http://publications.rwth-aachen.de/record/461238/files/461238.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Mathematik (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
Die Klassifikation erkennbarer ω-Wortsprachen in Stufen der Borel-Hierarchie ist die Basis zahlreicher angepasster Lösungen in den Bereichen der formalen Verifikation und der algorithmischen Controller-Synthese. Jede dieser Stufen wird durch eine Klasse deterministischer ω-Automaten charakterisiert, nämlich durch deterministische schwache Automaten (Erreichbarkeits- und Sicherheitsbedingungen), deterministische Büchi-Automaten und deterministische Muller-Automaten. Die vorliegende Arbeit analysiert das allgemeinere Rahmenwerk der unendlichen Mazurkiewicz-Spuren, die als Modelle für nicht terminierende, nebenläufige Läufe verteilter Systeme dienen. Das Studium der Sprachen endlicher Spuren verallgemeinert das der Wortsprachen, und zahlreiche Ergebnisse haben auch eine Erweiterung auf Sprachen unendlicher Spuren erreicht (Gastin, Petit, Diekert, Muscholl und andere). Doch liefern die verfügbaren Definitionen von asynchronen ω-Automaten keine Klassifizierung der ω-Spursprachen, die mit der Borel-Hierarchie verträglich ist. Wir schließen diese seit den 1990’er Jahren bestehende Lücke durch die Einführung der Familie der ,,synchronisationsbewussten`` Automaten.Wir zeigen auch die Semi-Entscheidbarkeit des Problems, ob eine gegebene erkennbare ω-Spursprache durch einen deterministischen synchronisationsbewussten Büchi-Automaten erkannt werden kann.Obwohl asynchrone Automaten in der Implementierung verteilter Monitore und verteilter Controller ihren Nutzen haben, ist ihre Konstruktion extrem aufwändig, sogar im Vergleich zu bekannten komplexen Verfahren für ω-Automaten. Dagegen finden ,,Linearisierungen`` infinitärer Spursprachen, die auf Spur-abgeschlossenen ω-Wortsprachen beruhen, unmittelbare Anwendungen im Model-Checking und der formalen Verifikation verteilter Systeme. Dies hat seinen Grund darin, dass Wortautomaten, die Spur-abgeschlossene Sprachen erkennen, effizientere Analysen der für verteilte Systeme wesentlichen Eigenschaften ermöglichen. In diesem Rahmen präsentieren wir eine weitere Klassifikation von ω-Spursprachen in einer Borel-ähnlichen Hierarchie von Spur-abgeschlossenen ω-Wortsprachen.Abschließend führen wir eine Version des Church’schen Synthese-Problems für verteilte Systeme ein und vergleichen es mit zwei bekannten Varianten der verteilten Controller-Synthese, nämlich der aktionsbasierten Kontrolle (Gastin, Lerman, Zeitoun) und der prozessbasierten Kontrolle (Madhusudan, Thiagarajan, Yang). Die algorithmische Lösung dieser Probleme bleibt zwar eine offene Frage, doch erweitern wir Ergebnisse von Muscholl, Walukiewicz und Zeitoun und vergleichen Ihre Problemklassen mit Varianten des Church'schen Syntheseproblems durch dem Nachweis von Reduktionen in dem Sinne, dass eine Lösung eines Problems in die Lösung eines anderen überführt werden kann.

The classification of recognizable ω-word languages into Borel levels is the basis of many specialized solutions in the fields of formal verification and algorithmic controller synthesis. Each of these levels is characterized by a class of deterministic ω-automata, namely deterministic weak (reachability and safety), deterministic Büchi, and deterministic Muller automata. This thesis analyses the more general setting of infinitary Mazurkiewicz traces, which model nonterminating, concurrent computation of distributed systems. The study of finitary trace-languages generalizes that of word-languages, and numerous results have been extended to infinitary trace-languages (due to Gastin, Petit, Diekert, Muscholl, and others). However, the current definitions of asynchronous ω-automata fail to yield a classification of ω-trace languages that is compatible with the Borel hierarchy. We close this gap, which had been open since the 1990's, by introducing the family of "synchronization aware'' automata. We also demonstrate the semi-decidability of the problem to determine whether a given recognizable ω-trace language is also recognized by a deterministic synchronization aware Büchi automaton.Although asynchronous automata are useful in implementing distributed monitors and distributed controllers, their constructions are prohibitively expensive even by automata-theoretic standards. On the other hand, "linearizations'' of infinitary trace languages, which invoke the framework of "trace-closed'' ω-word languages, can find immediate applications in model checking and formal verification of distributed systems. This is because word automata recognizing trace-closed languages support more efficient analyses of most of the interesting properties pertaining to distributed computations. In this setting, we present another classification of ω-trace languages in terms of a Borel-like hierarchy of trace-closed ω-word languages.Finally, we introduce a distributed version of Church's synthesis problem and compare it with two well known variants of distributed controller synthesis, viz. action-based control (due to Gastin, Lerman, and Zeitoun) and process-based control (due to Madhusudan, Thiagarajan, and Yang). While the algorithmic solution of these problems remains an open area of investigation, we build upon the work of Muscholl, Walukiewicz, and Zeitoun, and compare their problem classes with variants of distributed Church's synthesis problem by demonstrating suitable reductions in the sense that a solution of any one problem can be converted into a solution of the other.

OpenAccess:
PDF PDF (PDFA)
(additional files)