Bounded Synthesis of Distributed Architectures
Synthesis derives an implementation that satisfies a certain specification. Contrary to verification, synthesis can be even more time consuming and very complex. A few years ago bounded synthesis was introduced. This approach bounds a system parameter, i.e. its size, and the search space is limited to all implementations within this bound. We will briefly explain the general approach of bounded synthesis for both monolithic systems and distributed architectures. Afterwards we will look at an input format for architectures. We will compare results of three different SMT solvers: CVC4, Yices and Z3 and look at the difference between resulting transition systems in the mealy or moore format. We will also look at the differences between using consistency or weak symmetry constraints when solving a constraint system of a specification for a distributed architecture and look at results for different types of architectures.