Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis

Watch this 19-minute conference talk from POPL 2025 where Philippe Heim and Rayna Dimitrova from CISPA Helmholtz Center for Information Security present their innovative approach to infinite-state reactive synthesis. Learn about a novel technique that constructs monitors incorporating first-order and temporal reasoning at the formula level, enriching constructed games with semantic information for more efficient solving. The presentation addresses a significant gap in current methods, which typically lose the semantic structure of temporal and first-order constraints when translating temporal logics into symbolic games. Discover how this new approach outperforms state-of-the-art techniques across various benchmarks, offering a more efficient solution for infinite-state reactive synthesis problems. The talk includes discussion of their reusable artifacts, which are available via Zenodo. This research was presented at the ACM SIGPLAN POPL conference in January 2025.