Synthesis of Distributed Systems

Distributed and parallel systems have an increasing influence on our lives. Defective systems can endanger our lives or health (e.g., in the control of airbags) and cause considerable costs (e.g., transactions processing). For computer science this implies the challenge to establish a sound mathematical foundation for the development of such systems. This book provides a central contribution in this field: It presents a solution to the synthesis problem of distributed systems, that is, for automatically deriving an implementation from its specification. Synthesis is inspired by Alonzo Churchs' famous solvability problem, which first distinguished the construction of programmes that satisfy a specification by construction from the problem of finding a model of a given logic formula. To exemplified this difference, it is simple to constructing a model for the property "the output predicts the next input", but obviously no program can implement such a specification; synthesis procedures have to take the interfaces of a system into account that determine what a process knows and which influence it can have on the behaviour of the system. Distributed systems have interfaces between the individual components, and it has proven an easy task to abuse them to give Turing power to simple logics like LTL even for simple two processes architectures. However, synthesis has been known to be decidable for specific architectures like pipelines or rings. The fundamental question about the deeper causes for this undecidability and thus the possibility of a general solution for the synthesis problem, however, remained open.
This book provides a complete characterisation of the system architectures for which an automatic synthesis is feasible, the information fork criterion, and presents a uniform decision procedure for all decidable cases.