Faster and Smaller Solutions of Obliging Games

TL;DR

This paper introduces a novel large-step approach to analyzing obliging games, enabling more efficient solutions by encoding long-term behaviors, which improves strategy sizes and runtime bounds compared to previous small-step methods.

Contribution

It proposes a new large-step reduction method for obliging games, enhancing efficiency and providing better bounds on strategies and solution runtime.

Findings

Significantly improved bounds on strategy sizes.

Reduced solution runtime for obliging games.

New meaningful definition of environment winning in obliging games.

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.