Bounded Synthesis

Abstract. The bounded synthesis problem is to construct an implementation that satisfies a given temporal specification and a given bound on the number of states. We present a solution to the bounded synthesis problem for linear-time temporal logic (LTL), based on a novel emptiness-preserving translation from LTL to safety tree automata. For distributed architectures, where standard unbounded synthesis is in general undecidable, we show that bounded synthesis can be reduced to a SAT problem. As a result, we obtain an effective algorithm for the bounded synthesis from LTL specifications in arbitrary architectures. By iteratively increasing the bound, our construction can also be used as a semi-decision procedure for the unbounded synthesis problem.

• Type: Conference
• Year: 2007
• Where: ATVA
• Authors: Sven Schewe, Bernd Finkbeiner
• Keywords: ATVA 2007, Standard Unbounded Synthesis, Synthesis Problem, Unbounded Synthesis