Uniform Strategies

TL;DR

This paper introduces a formal language for specifying uniformity properties of strategies in turn-based game arenas, enabling the synthesis of strategies under complex constraints, extending existing temporal logic approaches.

Contribution

It proposes a novel formal language for uniformity properties, incorporates an additional modality for strategy correlation, and provides a generic synthesis procedure for relations definable by finite state transducers.

Findings

Rephrases known problems using the new formal language.

Develops an automated strategy synthesis procedure.

Extends existing results with a non-elementary complexity procedure.

Abstract

We consider turn-based game arenas for which we investigate uniformity properties of strategies. These properties involve bundles of plays, that arise from some semantical motive. Typically, we can represent constraints on allowed strategies, such as being observation-based. We propose a formal language to specify uniformity properties and demonstrate its relevance by rephrasing various known problems from the literature. Note that the ability to correlate different plays cannot be achieved by any branching-time logic if not equipped with an additional modality, so-called R in this contribution. We also study an automated procedure to synthesize strategies subject to a uniformity property, which strictly extends existing results based on, say standard temporal logics. We exhibit a generic solution for the synthesis problem provided the bundles of plays rely on any binary relation definable by a finite state transducer. This solution yields a non-elementary procedure.