Synthesis of distributed systems
Sven Schewe · 2008
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