Automatic Synthesis of Distributed Systems

Introduction In this project we studied the problem of automatically synthesising a distributed system starting from a formal specification. 1.1 Motivation Automatic synthesis can be seen as a complementary approach to verification. Both approaches were proposed in the early 80s in the seminal works [10, 14]. The verification procedure needs beside a specification also a candidate model. If this candidate fails to fulfill the specification, the designer must iteratively improve the model and check it again. In automatic synthesis, the system is automatically derived from the specification, and, moreover, it is correct by construction. Despite these advantages, and the fact that the two approaches have similar computational complexity for logics like LTL or CTL, automatic synthesis has been far less successful than verification, both from a theoretical and a practical point of view. The project is based on the following hypothesis: Specification languages like LTL and CTL are not a