SMT-Based Synthesis of Distributed Systems
Bernd Finkbeiner and Sven Schewe
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-Buchi 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 two-process distributed arbiter, within one minute.
Second Workshop on Automated Formal Methods (AFM 2007) (AFM 2007).