Simons Institute | Symbolic Finite- and Infinite-state Synthesis @SimonsInstituteTOC | Uploaded 2 months ago | Updated 2 hours ago
Nir Piterman (University of Gothenberg)
https://simons.berkeley.edu/talks/nir-piterman-university-gothenberg-2024-07-18
Games and Equilibria in System Design and Analysis
Reactive synthesis can automatically craft programs that satisfy a given specification. However, it fails to scale to large domains and becomes undecidable in infinite settings. Scalability is mainly affected by the need to enumerate, which can quickly explode the state space and is not viable in the infinite setting. We believe abstraction-refinement techniques can tackle these problems, but existing approaches mainly exploit safety refinements, which do not significantly aid scalability.
In this work we introduce a novel iterative abstraction-refinement approach to LTL synthesis, starting from a succinct symbolic representation of problems, and exploiting invariant checking to identify correctness of abstract counterstrategies. We introduce the notion of liveness refinements for synthesis, based on identifying concretely terminating loops in abstract counterstrategies. Other approaches exist that identify and add liveness constraints for infinite-state synthesis, however they either do not ensure progress or only apply them in a localised manner. We also present a proof-of-concept prototype, contribute further benchmarks, and show how our approach goes very significantly beyond the state-of-the-art on our and standard LIA benchmarks. We also contribute a set of finite-state benchmarks, and identify a subset whose solution does not depend on the size of the finite domain, and show that our approach’s runtime uniquely does not exhibit dependence on the domain size.
Joint work with Shaun Azzopardi, Luca di Stefano, and Gerardo Schneider.
Nir Piterman (University of Gothenberg)
https://simons.berkeley.edu/talks/nir-piterman-university-gothenberg-2024-07-18
Games and Equilibria in System Design and Analysis
Reactive synthesis can automatically craft programs that satisfy a given specification. However, it fails to scale to large domains and becomes undecidable in infinite settings. Scalability is mainly affected by the need to enumerate, which can quickly explode the state space and is not viable in the infinite setting. We believe abstraction-refinement techniques can tackle these problems, but existing approaches mainly exploit safety refinements, which do not significantly aid scalability.
In this work we introduce a novel iterative abstraction-refinement approach to LTL synthesis, starting from a succinct symbolic representation of problems, and exploiting invariant checking to identify correctness of abstract counterstrategies. We introduce the notion of liveness refinements for synthesis, based on identifying concretely terminating loops in abstract counterstrategies. Other approaches exist that identify and add liveness constraints for infinite-state synthesis, however they either do not ensure progress or only apply them in a localised manner. We also present a proof-of-concept prototype, contribute further benchmarks, and show how our approach goes very significantly beyond the state-of-the-art on our and standard LIA benchmarks. We also contribute a set of finite-state benchmarks, and identify a subset whose solution does not depend on the size of the finite domain, and show that our approach’s runtime uniquely does not exhibit dependence on the domain size.
Joint work with Shaun Azzopardi, Luca di Stefano, and Gerardo Schneider.
