Our paper “Full LTL Synthesis over Infinite-state Arenas” has been accepted to CAV 2025.

A previous version of the paper is available on ArXiv. We are working hard on the final version! A repository of Dockerfiles to try out our synthesis tool is on GitHub.

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 ap- proaches 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 exponen- tial 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 thrice as many problems as the current state-of-the-art and roughly 1.5 times as many as the second-best realisability checker. We also introduce benchmarks with richer objectives than other approaches can handle, and evaluate our tool on them.