FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Strix: Explicit Reactive Synthesis Strikes Back!

Authors: Philipp J. Meyer, Salomon Sickert and Michael Luttenberger

Paper Information

Title:Strix: Explicit Reactive Synthesis Strikes Back!
Authors:Philipp J. Meyer, Salomon Sickert and Michael Luttenberger
Proceedings:CAV All Papers
Editors: Georg Weissenbacher, Hana Chockler and Igor Konnov
Keywords:Reactive Synthesis, Linear Temporal Logic, AMBA AHB, Deterministic Parity Automaton, Parity Game
Abstract:

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) translates these on-the-fly into DPAs based on the queries of the parity game solver, (3) composes the DPAs into a parity game, and at the same time already solves the intermediate games using strategy iteration, and (4) finally translates the wining strategy, if it exists, into a Mealy automaton or an AIGER cicuit with optional minimization using external tools. We experimentally demonstrate the applicability of our approach by a comparison with Party, BoSy and ltlsynt using the SYNTCOMP2017 benchmarks. In these experiments, our prototype can compete with BoSy and ltlsynt with only Party performing slightly better. In particular, our prototype successfully synthesizes the full and unmodified LTL specification of the AMBA protocol for n = 2 masters.

Pages:9
Talk:Jul 15 14:15 (Session 105A: Tools)
Paper: