Encodings of Bounded Synthesis of Distributed Systems
Jan Baumeister
Reactive synthesis is one approach to get correct programs from a formal specification, e.g. given in linear-time temporal logic (LTL). This approach constructs correct-by-design implementations directly from those specifications and frees the programmer from writing an implementation. To cope with the drawback of the high complexity, bounded synthesis was introduced by Finkbeiner and Schewe in 2012. This approach bounds the size of the implementation, for example in the number of states. The original implementation constructs an SMT query that is satisfiable iff a realizing implementation of that size exists. Later Faymonville et al. proposed different encodings to (quantified) propositional logics. In this thesis we explain the bounded synthesis approach for single process and distributed synthesis. Based on the encodings introduced by Faymonville et al. we define three new encodings to solve the distributed bounded synthesis problem and proof their functional correctness. We conclude by comparing the different encodings in an experimental evaluation section.
Bachelor Thesis.