Symbolic Finite- and Infinite-state Synthesis

Explore a 35-minute lecture on symbolic finite- and infinite-state synthesis presented by Nir Piterman from the University of Gothenberg. Delve into the challenges of reactive synthesis in large and infinite domains, and discover a novel iterative abstraction-refinement approach to LTL synthesis. Learn about the concept of liveness refinements for synthesis and how they identify concretely terminating loops in abstract counterstrategies. Examine the proof-of-concept prototype and its performance on standard LIA benchmarks. Gain insights into finite-state benchmarks and how the presented approach uniquely handles domain size independence. Understand the collaborative efforts behind this research, involving Shaun Azzopardi, Luca di Stefano, and Gerardo Schneider.