Synthesis of Distributed Systems
Sven Schewe
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^(c/2)) to O(n^(c/3)), 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 mu-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 communication 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 criterion 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.
PhD Thesis.