Distributed Games For Reactive Systems
Tobias Maurer
In system synthesis, a specification is transformed into a framework which is guaranteed to satisfy the specification. When the system is distributed, the goal is to construct the system’s underlying processes.
Results on multi-player games imply that the synthesis problem for linear specifications is undecidable for general architectures. If the processes are linearly ordered and information among them flows in one direction the problem becomes decidable with non-elementary complexity. It seems plausible that the problem cannot be implemented in practice. However, LTL specifications and distributed systems are used in system design. This suggests, that the blowup does not really occur in practice. Former works concentrated on the theoretical complexity of the problem. Here a proof of concept for practical use is given by ReaSyn.
ReaSyn is based on the provided implementations. In case of realizability ReaSyn produces a valid PROMELA implementation, that simulates the distributed system. This thesis shows that for practical examples distributed synthesis is possible.
Diploma Thesis.