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 recognizable relations yields a 2EχpτiME-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.
展开▼
