Property-directed synthesis of reactive systems from safety specifications

Reactive system synthesis from safety specifications is a promising approach to the correct-by-construction methodology. The synthesis process is often divided into two separate steps: First, check specification realizability by computing the winning region of states under a game-theoretic interpretation; second, synthesize the implementation circuit based on the computed winning region if the specification is realizable. Moreover, recent results suggest that methods based on satisfiability (SAT) solving outperform those based on Binary Decision Diagrams (BDDs) especially on large benchmark instances. In this paper, we focus on the the winning region computation and propose a SAT-based algorithm. By adopting the concepts from the state-of-the-art model checking algorithm property directed reachability (PDR, a.k.a. IC3), we aim at devising an efficient computation method for automatic controller synthesis. Experimental results on the benchmarks from the synthesis competition (SyntComp 2014) show that our proposed algorithm outperforms the existing SAT-based and QBF-based methods by some margin.