Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.
You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.
After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.
digitally watermarked, no DRM
The eBook version of this title will be available soon
Excellently written overview of an area of interest in logic and theoretical computer science
Makes a central contribution to the mathematical foundation for the development of distributed systems
Model checking has become a hot topic also in other fields such as biology
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.