Strix: Explicit Reactive Synthesis Strikes Back!

ABSTRACT. Strix is a new tool for reactive LTL synthesis combining a direct translation of LTL formulas into deterministic parity automata (DPA) and an efficient, multi-threaded explicit state solver for parity games. In brief, Strix (1) decomposes the given formula into simpler formulas, (2) identifies isomorphic formulas and groups them into equivalence classes, (3) translates one formula for each class on-the-fly into DPAs based on the queries of the parity game solver, (4) composes the DPAs into a parity game, and at the same time already solves the intermediate games using strategy iteration, (5) finally translates the winning strategy, if it exists, into a Mealy machine or an AIGER circuit, and (6) optionally minimizes the resulting Mealy machine or AIGER circuit. We experimentally demonstrate the applicability of our approach by a comparison with Party, BoSy, and ltlsynt using the SYNTCOMP 2017 benchmarks. In these experiments, our tool can compete with all other approaches, solving more instances for realizability and often producing smaller solutions. In particular, our tool successfully synthesizes the full and unmodified LTL specification of the AMBA protocol for n=2 masters. We will also report on the results of SYNTCOMP 2018 for which we entered with Strix this year. This is joint work with Salomon Sickert and Michael Luttenberger. It has been accepted at CAV 2018 as a tool paper. This work was partially funded and supported by the German Research Foundation (DFG) projects "Game-based Synthesis for Industrial Automation" (253384115) and "Verified Model Checkers" (317422601).

Authors

• Philipp J. Meyer

Keywords

No keywords are indexed for this paper.