Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Full LTL Synthesis over Infinite-state Arenas

Shaun Azzopardi, Luca Di Stefano, Nir Piterman, Gerardo Schneider

TL;DR

This paper tackles the challenge of synthesising controllers for full LTL specifications over infinite-state arenas, where the environment can delay progress and variables range over infinite domains. It introduces a CEGAR-inspired framework that combines predicate abstraction, invariant-based concretisability checks, and novel refinements (safety and two forms of liveness refinements) to handle termination of repeated behaviours. A key technical contribution is an efficient binary encoding of predicates that reduces abstraction and synthesis complexity and supports acceleration via well-founded progress and fairness constraints. Empirical results on a broad set of linear integer arithmetic benchmarks show state-of-the-art performance in synthesis and reveal the approach’s ability to handle richer objectives than prior work, including benchmarks with strong fairness. The work also contributes new benchmarks and discusses how its methods relate to and extend existing frameworks like TSL and RPG, outlining promising directions for further integration with symbolic and decision-procedure techniques.

Abstract

Recently, interest has increased in applying reactive synthesis to richer-than-Boolean domains. A major (undecidable) challenge in this area is to establish when certain repeating behaviour terminates in a desired state when the number of steps is unbounded. Existing approaches struggle with this problem, or can handle at most deterministic games with Büchi goals. This work goes beyond by contributing the first effectual approach to synthesis with full LTL objectives, based on Boolean abstractions that encode both safety and liveness properties of the underlying infinite arena. We take a CEGAR approach: attempting synthesis on the Boolean abstraction, checking spuriousness of abstract counterstrategies through invariant checking, and refining the abstraction based on counterexamples. We reduce the complexity, when restricted to predicates, of abstracting and synthesising by an exponential through an efficient binary encoding. This also allows us to eagerly identify useful fairness properties. Our discrete synthesis tool outperforms the state-of-the-art on linear integer arithmetic (LIA) benchmarks from literature, solving almost double as many syntesis problems as the current state-of-the-art. It also solves slightly more problems than the second-best realisability checker, in one-third of the time. We also introduce benchmarks with richer objectives that other approaches cannot handle, and evaluate our tool on them.

Full LTL Synthesis over Infinite-state Arenas

TL;DR

This paper tackles the challenge of synthesising controllers for full LTL specifications over infinite-state arenas, where the environment can delay progress and variables range over infinite domains. It introduces a CEGAR-inspired framework that combines predicate abstraction, invariant-based concretisability checks, and novel refinements (safety and two forms of liveness refinements) to handle termination of repeated behaviours. A key technical contribution is an efficient binary encoding of predicates that reduces abstraction and synthesis complexity and supports acceleration via well-founded progress and fairness constraints. Empirical results on a broad set of linear integer arithmetic benchmarks show state-of-the-art performance in synthesis and reveal the approach’s ability to handle richer objectives than prior work, including benchmarks with strong fairness. The work also contributes new benchmarks and discusses how its methods relate to and extend existing frameworks like TSL and RPG, outlining promising directions for further integration with symbolic and decision-procedure techniques.

Abstract

Recently, interest has increased in applying reactive synthesis to richer-than-Boolean domains. A major (undecidable) challenge in this area is to establish when certain repeating behaviour terminates in a desired state when the number of steps is unbounded. Existing approaches struggle with this problem, or can handle at most deterministic games with Büchi goals. This work goes beyond by contributing the first effectual approach to synthesis with full LTL objectives, based on Boolean abstractions that encode both safety and liveness properties of the underlying infinite arena. We take a CEGAR approach: attempting synthesis on the Boolean abstraction, checking spuriousness of abstract counterstrategies through invariant checking, and refining the abstraction based on counterexamples. We reduce the complexity, when restricted to predicates, of abstracting and synthesising by an exponential through an efficient binary encoding. This also allows us to eagerly identify useful fairness properties. Our discrete synthesis tool outperforms the state-of-the-art on linear integer arithmetic (LIA) benchmarks from literature, solving almost double as many syntesis problems as the current state-of-the-art. It also solves slightly more problems than the second-best realisability checker, in one-third of the time. We also introduce benchmarks with richer objectives that other approaches cannot handle, and evaluate our tool on them.
Paper Structure (18 sections, 3 theorems, 6 equations, 7 figures, 3 tables, 1 algorithm)

This paper contains 18 sections, 3 theorems, 6 equations, 7 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Informal Overview
  4. Synthesis Setting
  5. Abstract to Concrete Synthesis
  6. Predicate Abstraction
  7. Refinement
  8. Safety Refinement
  9. Liveness Refinement
  10. Efficient Encoding and Acceleration
  11. Evaluation
  12. Description of New Benchmarks
  13. Further Details on Experimental Evaluation
  14. Related Work
  15. Realisability modulo arenas vs. TSL and RPG
  16. ...and 3 more sections

Key Result

theorem thmcountertheorem

For a sequence of formulas $f_0,\ldots, f_k$, such that $\bigwedge_{i=0}^k f_i$ is unsatisfiable and for every $i,j$ either $|i-j|\leq 1$ or $f_i$ and $f_j$ do not share variables, then there is a set of sequence interpolants$I_0,\ldots, I_{k-1}$, where $f_0 \Longrightarrow I_0$, $\forall 1\leq i <

Figures (7)

  • Figure 1: Workflow of our approach.
  • Figure 2: Elevator example.
  • Figure 3: $ce$ loop.
  • Figure 4: Partitions for binary encoding.
  • Figure 5: Time comparison.
  • ...and 2 more figures

Theorems & Definitions (29)

  • definition thmcounterdefinition: LTL Synthesis
  • definition thmcounterdefinition: Arena
  • definition thmcounterdefinition: Abstract Words and Concretisability
  • definition thmcounterdefinition: Realisability modulo an Arena
  • definition thmcounterdefinition: Abstraction
  • proof
  • definition thmcounterdefinition: Counterstrategy Concretisability
  • proof
  • proof
  • proof
  • ...and 19 more