The Complexity of Synthesizing Uniform Strategies

TL;DR

This paper introduces a formal language for specifying uniformity properties of strategies in two-player games, analyzing the complexity of synthesizing strategies under these constraints, which is non-elementary complete.

Contribution

It proposes a new formal framework for uniformity properties in strategic synthesis and establishes the non-elementary complexity of the synthesis problem.

Findings

The framework captures various existing uniformity concepts.

Synthesizing strategies with these constraints is non-elementary complete.

The approach generalizes multiple scenarios from the literature.

Abstract

We investigate uniformity properties of strategies. These properties involve sets of plays in order to express useful constraints on strategies that are not \mu-calculus definable. Typically, we can state that a strategy is observation-based. We propose a formal language to specify uniformity properties, interpreted over two-player turn-based arenas equipped with a binary relation between plays. This way, we capture e.g. games with winning conditions expressible in epistemic temporal logic, whose underlying equivalence relation between plays reflects the observational capabilities of agents (for example, synchronous perfect recall). Our framework naturally generalizes many other situations from the literature. We establish that the problem of synthesizing strategies under uniformity constraints based on regular binary relations between plays is non-elementary complete.