Faster and Smaller Solutions of Obliging Games
Daniel Hausmann, Nir Piterman
TL;DR
This work addresses reactive-synthesis obligations by reframing obliging games as large-step, long-term commitments rather than single-step reductions. It introduces witnesses and certificates to capture feasible long-run behaviors, proves determinacy under this framework, and reduces ω-regular obliging games to finite certificate games. By applying a lazy LAR parity transform and DAG-attraction techniques, it achieves significantly smaller winning strategies and faster solution times in many cases, with tight linear and polynomial dependencies on the weak objective size $|W|$. The approach unifies a rigorous determinacy theory with practical algorithms, offering substantial improvements over prior methods and highlighting open questions about canonical certificates and direct non-LAR solutions.
Abstract
Obliging games have been introduced in the context of the game perspective on reactive synthesis in order to enforce a degree of cooperation between the to-be-synthesized system and the environment. Previous approaches to the analysis of obliging games have been small-step in the sense that they have been based on a reduction to standard (non-obliging) games in which single moves correspond to single moves in the original (obliging) game. Here, we propose a novel, large-step view on obliging games, reducing them to standard games in which single moves encode long-term behaviors in the original game. This not only allows us to give a meaningful definition of the environment winning in obliging games, but also leads to significantly improved bounds on both strategy sizes and the solution runtime for obliging games.