Benedikt Brütsch: “Synthesizing Structured Reactive Programs: How Much Memory Do They Need?”.
Abstract:
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.