20th Conference on Computer Science Logic (CSL), Bergen, Norway, 2011, pages 428-442
Used by the Cassting project
Current theoretical solutions to the classical Church’s synthesis problem are focussed on synthesizing transition systems and not programs. Programs are compact and often the true aim in many synthesis problems, while the transition systems that correspond to them are often large and not very useful as synthesized artefacts. Consequently, current practical techniques first synthesize a transition system, and then extract a more compact representation from it. In this paper, the synthesis of reactive systems is formulated directly in terms of program synthesis. The problem of synthesizing programs over a fixed set of Boolean variables in a simple imperative programming language is proven decidable for regular specifications.