Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fully Generalized Reactivity(1) Synthesis

Rüdiger Ehlers, Ayrat Khalimov

TL;DR

The paper tackles the bottleneck of reactive synthesis for full LTL by introducing a unified COCOA-based framework that preserves GR(1) efficiency while gracefully handling omega-regular specifications beyond GR(1). It builds on chains of good-for-games co-Büchi automata to obtain canonical, minimal representations of omega-regular languages and derives fixpoint equations that can be efficiently evaluated on symbolic game graphs. The COCOA-based fixpoint formulation generalizes GR(1) fixpoints and performs favorably against parity-based and LTL-specific solvers, often by one to two orders of magnitude in practice. This approach bridges GR(1) and LTL synthesis, enabling scalable synthesis for specifications slightly beyond GR(1) and providing a practical first application of COCOA in reactive synthesis with promising directions for future optimizations and implementations.

Abstract

Generalized Reactivity(1) (GR(1)) synthesis is a reactive synthesis approach in which the specification is split into two parts: a symbolic game graph, describing the safe transitions of a system, a liveness specification in a subset of Linear Temporal Logic (LTL) on top of it. Many specifications can naturally be written in this restricted form, and the restriction gives rise to a scalable synthesis procedure -- the reasons for the high popularity of the approach. For specifications even slightly beyond GR(1), however, the approach is inapplicable. This necessitates a transition to synthesizers for full LTL specifications, introducing a huge efficiency drop. This paper proposes a synthesis approach that smoothly bridges the efficiency gap from GR(1) to LTL by unifying synthesis for both classes of specifications. The approach leverages a recently introduced canonical representation of omega-regular languages based on a chain of good-for-games co-Büchi automata (COCOA). By constructing COCOA for the liveness part of a specification, we can then build a fixpoint formula that can be efficiently evaluated on the symbolic game graph. The COCOA-based synthesis approach outperforms standard approaches and retains the efficiency of GR(1) synthesis for specifications in GR(1) form and those with few non-GR(1) specification parts.

Fully Generalized Reactivity(1) Synthesis

TL;DR

The paper tackles the bottleneck of reactive synthesis for full LTL by introducing a unified COCOA-based framework that preserves GR(1) efficiency while gracefully handling omega-regular specifications beyond GR(1). It builds on chains of good-for-games co-Büchi automata to obtain canonical, minimal representations of omega-regular languages and derives fixpoint equations that can be efficiently evaluated on symbolic game graphs. The COCOA-based fixpoint formulation generalizes GR(1) fixpoints and performs favorably against parity-based and LTL-specific solvers, often by one to two orders of magnitude in practice. This approach bridges GR(1) and LTL synthesis, enabling scalable synthesis for specifications slightly beyond GR(1) and providing a practical first application of COCOA in reactive synthesis with promising directions for future optimizations and implementations.

Abstract

Generalized Reactivity(1) (GR(1)) synthesis is a reactive synthesis approach in which the specification is split into two parts: a symbolic game graph, describing the safe transitions of a system, a liveness specification in a subset of Linear Temporal Logic (LTL) on top of it. Many specifications can naturally be written in this restricted form, and the restriction gives rise to a scalable synthesis procedure -- the reasons for the high popularity of the approach. For specifications even slightly beyond GR(1), however, the approach is inapplicable. This necessitates a transition to synthesizers for full LTL specifications, introducing a huge efficiency drop. This paper proposes a synthesis approach that smoothly bridges the efficiency gap from GR(1) to LTL by unifying synthesis for both classes of specifications. The approach leverages a recently introduced canonical representation of omega-regular languages based on a chain of good-for-games co-Büchi automata (COCOA). By constructing COCOA for the liveness part of a specification, we can then build a fixpoint formula that can be efficiently evaluated on the symbolic game graph. The COCOA-based synthesis approach outperforms standard approaches and retains the efficiency of GR(1) synthesis for specifications in GR(1) form and those with few non-GR(1) specification parts.
Paper Structure (24 sections, 6 theorems, 20 equations, 5 figures)

This paper contains 24 sections, 6 theorems, 20 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. LTL.
  4. Games.
  5. Symbolic games with LTL objectives.
  6. Mu-calculus fixpoint formulas.
  7. Example.
  8. Chains of Good-for-Games co-Büchi Automata
  9. GFGness strategies $f^l$.
  10. Restrictions $g^l$.
  11. Get-back strategies $f^l_\star$.
  12. Alternating automata.
  13. COCOA product.
  14. Example.
  15. Solving LTL Games Using Chain of co-Büchi Automata
  16. ...and 9 more sections

Key Result

lemma thmcounterlemma

Fix a canonical GFG co-Büchi automaton $\cal A$ computed by DBLP:journals/lmcs/RadiK22. For every state $q$ and letter $x$, either there is

Figures (5)

  • Figure 1: Parity automaton for $\mathsf{GF} u \to (\mathsf{GF} x \land \mathsf{GF} y)$. Transitions are labeled by the proposition valuations for which they can be taken as well as the color of the transition.
  • Figure 2: Example of a deterministic co-Büchi automaton (on the left) and an equivalent canonical good-for-games co-Büchi automaton for the same language. Both automata have minimal numbers of states. Rejecting transitions are dashed. GFG co-Büchi automata are exponentially more succinct than deterministic ones DBLP:conf/icalp/KuperbergS15.
  • Figure 3: COCOA for the language $\mathsf{GF} u \to (\mathsf{GF} x \land \mathsf{GF} y)$. Rejecting transitions are dashed.
  • Figure 4: Optimized COCOA product for $\mathsf{GF} u \to (\mathsf{GF} x \land \mathsf{GF} y)$. It has only two nondeterministic transitions, connecting $(q_0,p_0)$ and $(q_1,p_1)$, controlled by the rejector. For instance, $\delta((q_0, p_0),x) = (\{(q_0,p_0),(q_1,p_1)\},0,\mathit{rej})$.
  • Figure 5: From left to right: (G1) Cactus plot comparing our approaches with LTL synthesizer $\tt strix$meyer2018strix; (G2a) Comparing COCOA-based approach with GR(1) synthesizer $\tt slugs$DBLP:conf/nfm/Ehlers11; (G2b) The same but excluding LTL-to-parity translation time; (G3) Comparing COCOA and parity approaches (excluding LTL-to-parity translation time).

Theorems & Definitions (10)

  • definition thmcounterdefinition
  • lemma thmcounterlemma: DBLP:journals/lmcs/RadiK22
  • corollary thmcountercorollary: DBLP:journals/lmcs/RadiK22
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • theorem thmcountertheorem