Bounded synthesis

A fundamental challenge in the synthesis of reactive systems is the size of the search space: the number of candidate implementations of a temporal specification is typically superexponential or even, for distributed system architectures, infinite. In this article, we introduce the bounded synthesis approach, which makes it possible to traverse this immense search space in a structured manner. We fix a bound on a system parameter, such as the number of states, and limit the search to those implementations that fall below the bound. By incrementally expanding the search to larger bounds, we maintain completeness, while orienting the search towards the simplest (and often most useful) solutions. The technical backbone of this solution is a novel translation from formulas of linear-time temporal logic to sequences of safety tree automata, which are guaranteed to underapproximate the specification and to eventually become emptiness-equivalent. Bounded synthesis is applicable to the entire range of synthesis problems, from individual processes to synchronous and asynchronous distributed systems, to systems with additional design constraints, such as symmetry. We include experimental results from a SMT-based implementation, which demonstrate that bounded synthesis solves many synthesis problems that were previously considered intractable. © 2012 Springer-Verlag.