Jumping Automata for Uniform Strategies

The concept of uniform strategies has recently been proposed as a relevant notion in game theory for computer science. It relies on properties involving sets of plays in two-player turn-based arenas equipped with a binary relation between plays. Among the two notions of fully-uniform and strictly-uniform strategies, we focus on the latter, less explored. We present a language that extends CTL^* with a quantifier over all related plays, which enables to express a rich class of uniformity constraints on strategies. We show that the existence of a uniform strategy is equivalent to the language non-emptiness of a jumping tree automaton. While the existence of a uniform strategy is undecidable for rational binary relations, restricting to ecognizable relations yields a 2EXPTIME-complete complexity, and still captures a class of two-player imperfect-information games with epistemic temporal objectives. This result relies on a translation from jumping tree automata with recognizable relations to two-way tree automata.