Extending finite-memory determinacy by boolean combination of winning conditions

This talk considers turn-based, infinite duration, two-player, win/lose games played on finite graphs. In the literature, who wins a play is defined via winning conditions such as Muller, energy, reachability, mean-payoff, etc. The usual winning conditions guarantee the existence of winning strategies that are simple enough to be implemented via finite automata. This guarantee is called finite-memory determinacy. Advanced modeling may involve combinations of the usual winning conditions mentioned above. Finite-memory determinacy may or may not be preserved by such combinations. I will describe a criterion for boolean combinations of winning conditions to preserve this determinacy. The criterion is general enough to imply finite-memory determinacy of energy Muller games, multi-dimensional bounded energy games, etc.

Authors

• Stephane Le Roux
• Arno Pauly

Keywords

No keywords are indexed for this paper.