Benedikt Brütsch: “Synthesizing Structured Reactive Programs: How Much Memory Do They Need?”.
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 omega-regular specification without synthesizing a transition system first. The complexity of his algorithm is doubly exponential in the number of Boolean variables that can be used by the program.
In this talk, I will show a superpolynomial 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.