Symbolic Infinite-State LTL Synthesis

Recently interest has increased in applying reactive synthesis to more practical richer-than-Boolean domains. One of the major challenges in this area is to establish when certain repeating behaviour terminates in a desired state when the number of steps is unbounded. This isolated problem, by itself, is already undecidable, and forms part of the overall difficulty of this kind of synthesis tasks. Relatively successful approaches exist for deterministic games with at most B{\"u}chi conditions. Our contribution goes beyond, being the first effective approach for solving symbolic synthesis problems with full LTL objectives, based on novel liveness refinements guided by the underlying game. Our CEGAR-based approach relies on a sound boolean abstraction of the problem, spuriousness checking of abstract counterstrategies through invariant checking, and extracting fresh safety or liveness properties of the concrete game from counterexamples. The latter are used to refine the abstraction, which is used to re-attempt synthesis. Our discrete synthesis tool outperforms the state-of-the-art on LIA benchmarks from literature. We also introduce benchmarks that are out of scope for all other approaches.