Synthesizing structured reactive programs via deterministic tree automata

Existing approaches to the synthesis of controllers in reactive systems typically involve the construction of transition systems such as Mealy automata. In 2011, Madhusudan proposed structured programs over a finite set of Boolean variables as a more succinct formalism to represent the controller. He provided an algorithm to construct such a program from a given ω-regular specification without synthesizing a transition system first. His procedure is based on two-way alternating ω-automata on finite trees that recognize the set of “correct” programs.We present a more elementary and direct approach using only deterministic bottom-up tree automata and extend Madhusudan's results to the wider class of programs with bounded delay, which may read several input symbols before producing an output symbol (or vice versa). In addition, we show a lower bound for the size of these tree automata. Finally, we prove a lower bound for the number of Boolean variables that are required for a structured program to satisfy a given LTL specification, almost matching the known upper bound.