SMT-based synthesis of distributed systems
Bernd Finkbeiner, Sven Schewe · 2007
We apply SMT solving to synthesize distributed systems from specifications in linear-time temporal logic (LTL). The LTL formula is translated into an equivalent universal co-Büchi tree automaton. The existence of a finite transition system in the language of the automaton is then specified as a quantified formula in the theory (N,<) of the ordered natural numbers with uninterpreted function symbols. While our experimental results indicate that the resulting satisfiability problem is generally out of reach for the currently available SMT solvers, the problem immediately becomes tractable if we fix an upper bound on the number of states in the distributed system. After replacing each universal quantifier by an explicit conjunction, the SMT solver Yices solves simple single-process synthesis problems within a few seconds, and distributed synthesis problems, such as a twoprocess distributed arbiter, within one minute.