Synthesis of distributed systems

Abstract

This thesis offers a comprehensive solution of the distributed synthesis problem. It starts with the problem of solving Parity games, which form an integral part of the automata-theoretic synthesis algorithms we use. We improve the known complexity bound for solving parity games with n positions and c colors approximately from O(n^(1/2*c)) to O(n^(1/3*c)), and introduce an accelerated strategy improvement technique that can consider all combinations of local improvements in every update step, selecting the globally optimal combination. We then demonstrate the decidability and finite model property of alternating-time specification languages, and determine the complexity of the satisfiability and synthesis problem for the alternating-time μ-calculus and the temporal logic ATL*. The impact of the architecture, that is, the set of system processes with known (white-box) and unknown (black-box) implementation, and the com- munication structure between them, is determined. We introduce information forks, a simple but comprehensive criterion that characterizes all architectures for which the synthesis problem is undecidable. The information fork crite- rion takes the impact of nondeterminism, the communication topology, and the specification language into account. For decidable architectures, we present an automata-based synthesis algorithm. We introduce bounded synthesis, which deviates from general synthesis by considering only implementations up to a predefined size, and thus avoids the expensive representation of all solutions. We develop a SAT based approach to bounded synthesis, which is nondeterministic quasilinear in the minimal implementation instead of nonelementary in the system specification. We determine the complexity of open synthesis under the assumption of probabilistic or reactive environments. Our automata based approach allows for a seamless integration of the new environment models into the uniform synthesis algorithm. Finally, we study the synthesis problem for asynchronous systems. We show that distributed synthesis remains only decidable for architectures with a single black-box process, and determine the complexity of the synthesis problem for different scheduler types. Furthermore, we combine the undecidability results and synthesis procedures for synchronous and asynchronous systems; systems that are globally asynchronous and locally synchronous are decidable if all black-box components are contained in a single fork-free synchronized component.

Diese Dissertation löst das Syntheseproblem für verteilte Systeme. Sie beginnt mit verbesserten Algorithmen zum Lösen von Parity Spielen, die einen integralen Bestandteil der Automaten basierten Synthese bilden. Die bekannte Komplexitätsschranke für das Lösen von Parity Spielen mit n Knoten und c Farben wird von ca. O(n^(1/2*c)) auf ca. O(n^(1/3*c)) verbessert, und es wird eine beschleunigte Strategie Verbesserungsmethode entwickelt, die, in jedem Schritt, die optimale Kombination aller lokalen Verbesserungen findet. Die Entscheidbarkeit alternierender Logiken wird gezeigt, und die Komplexität des Erfüllbarkeits- und Syntheseproblems für das Alternierende µ-Kalkül (EXPTIME-vollständig) und die Temporallogik ATL* (2EXPTIME-vollständig) bestimmt. Der Einfluss der Systemarchitektur, der Spezifikationssprache und, damit verbunden, des Implementierungsmodells (deterministisch vs. nichtdeterministisch) auf die Entscheidbarkeit und Komplexität des Syntheseproblems wird herausgearbeitet. Es wird gezeigt, dass die Klasse der entscheidbaren Architekturen durch die Abwesenheit von Information Forks, einem einfachen und leicht prüfbaren Kriterium auf der Kommunikationsarchitektur, vollständig beschrieben werden kann. Für entscheidbare Architekturen wird ein einheitliches Automaten basiertes Syntheseverfahren entwickelt. Darüber hinaus wird ein SAT basiertes Verfahren entwickelt, dass die Repräsentation aller Lösungen in einem Automaten umgeht. Die Komplexität des SAT basierten Verfahrens ist nichtdeterministisch quasilinear in der Größe des minimalen Modells, statt nicht-elementar in der Größe der Spezifikation. Für probabilistische und reaktive Umgebungen wird die Komplexität des offenen Syntheseproblems bestimmt, und jeweils ein Automaten basiertes Syntheseverfahren entwickelt, dass sich nahtlos in das Syntheseverfahren für verteilte Systeme integrieren lässt. Ferner wird gezeigt, dass verteilte Synthese für asynchrone Systeme nur dann entscheidbar bleibt, wenn lediglich die Implementierung einer Komponente konstruiert werden soll. Schließlich werden die Entscheidbarkeitsresultate und Synthese Algorithmen für synchrone und asynchrone Modelle zusammengeführt: Global asynchrone lokal synchrone Systeme sind entscheidbar, wenn alle zu synthetisierenden Prozesse in der gleichen synchronisierten Komponente liegen, und diese Komponente keine Information Forks enthält.