Automatic synthesis of distributed transition systems

Abstract

This thesis investigates the synthesis problem for two classes of distributed transition systems: synchronous products and asynchronous automata. The underlying structure of these models consist of local automata synchronizing on common actions. The synthesis problem discussed is as follows: Given a global specification as a transition system TS and a distribution pattern D, find a distributed transition system over D whose global state space is equivalent' to TS. As criteria for the correctness of the (distributed) implementation vs. the specification (i.e., their equivalence') we use: transition system isomorphism, language equivalence, and bisimilarity respectively. In particular, the synthesis of asynchronous automata modulo language equivalence is a notoriously hard problem solved by Zielonka at the end of the 80s. One of the motivations behind our work was to bring this theory closer to practical applications.

From the theoretical point of view, we conduct a detailed analysis of the synthesis problem for both models of distributed systems, look at effective algorithmic approaches and draw a map of computational complexity results. E.g., we provide several matching lower and upper complexity bounds for the distributed implementability problem.

From the practical perspective, we provide prototype implementations for most of the synthesis algorithms discussed in the thesis. Moreover, we offer assistance when a given specification is not distributable by trying to modify this specification such that distributed synthesis can be applied. By using several heuristics to overcome the classical state space explosion, we are able to automatically generate small distributed algorithms for problems such as mutual exclusion.

Diese Dissertation erforscht das Syntheseproblem für zwei verschiedene Arten von verteilten Transitionssysteme: synchrone Produkte und asynchrone Automaten. Diese Modelle bestehen aus lokalen Automaten, die sich über gemeinsame Aktionen synchronisieren. Das betrachtete Syntheseproblem ist Folgendes: Für ein gegebenes Transitionssystem TS und eine Verteilungsstruktur D sucht man ein verteiltes Transitionssystem über D mit einem globalen Zustandraum äquivalent' zu TS. Als Kriterien für die Korrektheit der Implementierung bezüglich der Spezifikation (d.h., ihre Äquivalenz'), verwenden wir Transitionssystem-Isomorphismus, Sprachenäquivalenz bzw. Bisimilarität. Insbesondere ist die Synthese der asynchronen Automaten Modulo-Sprachenäquivalenz ein bekanntes hartes Problem, das von Zielonka Ende der 80iger Jahre gelöst wurde. Einer der Beweggründe hinter unserer Arbeit war diese Theorie näher an praktische Anwendungen zu holen.

Aus theoretische Sicht leiten wir eine ausführliche Analyse des Syntheseproblems für beide Modelle der verteilten Systeme, betrachten wirkungsvolle Algorithmische Verfahren und erarbeiten eine Übersicht der Berechnungskomplexität. So z.B. stellen wir einige untere und obere Komplexitätsgrenzen für das verteilte Implementierungsproblem zur Verfügung.

Von einer praktischen Ansicht leifern wir Prototypimplementierungen für die meisten Synthesealgorithmen, die in diese Dissertation besprochen werden. Außerdem bieten wir Unterstützung an, falls eine gegebene Spezifikation nicht verteilbar ist und versuchen, sie zu ändern, so daß verteilte Synthese möglich wird. Indem wir einige Heuristiken verwenden, zum der klassischen Zustandraumsexplosion zu überwinden, sind wir in der Lage, kleine verteilte Algorithmen für Probleme, wie z.B. der gegenseitige Ausschluß (Mutex), automatisch zu erzeugen.