Bounded Synthesis of Reactive Programs
Carsten Gerstacker
Bounded Synthesis is the construction of an implementation that satisfies a given temporal specification and a bound on the size of the implementation. The approach presented by Schewe and Finkbeiner introduces Bounded Synthesis of transition systems such as Mealy machines which improves on classic synthesis in that the reduced search space only contains implementations of the specified size. However, transitions systems are often derived as synthesis artifacts which are too large and structurally complex to be considered comprehensible and therefore motivate the synthesis of more succinct representations of implementations. Programs that are compact and naturally comprehensible are such a desirable representation. Additionally, systems are usually designed by means of high-level representations such as programs. In this thesis we revisit the bounded synthesis approach and a solution to program synthesis. We then introduce a solution for the bounded synthesis problem for reactive programs based on the revisited approaches.
Bachelor Thesis.