Practical synthesis of reactive systems from LTL specifications via parity games
From MaRDI portal
Publication:2303871
Abstract: The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.
Recommendations
Cites work
- Antichains and compositional algorithms for LTL synthesis
- Automata, logics, and infinite games. A guide to current research
- Bounded synthesis of reactive programs
- From LTL and limit-deterministic Büchi automata to deterministic parity automata
- Graph Games and Reactive Synthesis
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 1973991 (Why is no real title available?)
- scientific article; zbMATH DE number 7311251 (Why is no real title available?)
- Limit-deterministic Büchi automata for linear temporal logic
- LTL to deterministic Emerson-Lei automata
- One theorem to rule them all: a unified translation of LTL into -automata
- Owl: a library for \(\omega \)-words, automata, and LTL
- Safraless Compositional Synthesis
- Symbolic bounded synthesis
- Towards efficient parameterized synthesis
- Two local strategy iteration schemes for parity game solving
- Unbeast: Symbolic Bounded Synthesis
Cited in
(27)- \(\mathsf{GR}(1)\) is equivalent to \(\mathsf{R}(1)\)
- Back to the future: a fresh look at linear temporal logic
- Incorporating monitors in reactive synthesis without paying the price
- Reactive synthesis with maximum realizability of linear temporal logic specifications
- Synthesis of Reactive(1) designs
- Strix
- Flexible FOND Planning with Explicit Fairness Assumptions
- A Hybrid Algorithm for LTL Games
- Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis
- Universal algorithms for parity games and nested fixpoints
- OmegaThreads
- Dissecting \texttt{ltlsynt}
- Tableaux for realizability of safety specifications
- Justifications and a reconstruction of parity game solving algorithms
- Research Challenges in Orchestration Synthesis
- Practical applications of the alternating cycle decomposition
- Guessing winning policies in LTL synthesis by semantic learning
- Taming large bounds in synthesis from bounded-liveness specifications
- LTL reactive synthesis with a few hints
- From Muller to parity and Rabin qutomata: optimal transformations preserving (history) determinism
- Advancing orchestration synthesis for contract automata
- Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
- Faster and smaller solutions of obliging games
- The complexity of simplifying -automata through the alternating cycle decomposition
- Optimal transformations of games and automata using Muller conditions
- Linear temporal constraints for sketch-based synthesizers
- Synthesising reward machines for cooperative multi-agent reinforcement learning
This page was built for publication: Practical synthesis of reactive systems from LTL specifications via parity games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2303871)
