Extending finite-memory determinacy by Boolean combination of winning conditions

TL;DR

This paper investigates conditions under which finite-memory strategies are sufficient for optimal play in complex multi-objective games on finite graphs, providing a unified framework that broadens understanding of FM determinacy.

Contribution

It introduces a general criterion for finite-memory determinacy applicable to a wide range of game classes, unifying and extending existing results.

Findings

Framework encompasses key classes of games from literature

Provides a criterion for FM determinacy in multi-objective games

Enhances understanding of core principles behind FM strategies

Abstract

We study finite-memory (FM) determinacy in games on finite graphs, a central question for applications in controller synthesis, as FM strategies correspond to implementable controllers. We establish general conditions under which FM strategies suffice to play optimally, even in a broad multi-objective setting. We show that our framework encompasses important classes of games from the literature, and permits to go further, using a unified approach. While such an approach cannot match ad-hoc proofs with regard to tightness of memory bounds, it has two advantages: first, it gives a widely-applicable criterion for FM determinacy; second, it helps to understand the cornerstones of FM determinacy, which are often hidden but common in proofs for specific (combinations of) winning conditions.