Tree games with regular objectives

TL;DR

This paper investigates the determinacy of non-stochastic tree games with regular objectives, providing conditions under which they are determined and an algorithm to decide this for given game objectives.

Contribution

It establishes that non-stochastic tree games with objectives recognized by game automata are determined under finite memory strategies, and introduces an algorithm to decide determinacy.

Findings

Non-stochastic tree games with automata-recognizable objectives are determined.

An elementary algorithm can decide determinacy for any regular language and tree game.

Determinacy under deterministic strategies depends on the recognizability of objectives by game automata.

Abstract

We study tree games developed recently by Matteo Mio as a game interpretation of the probabilistic $\mu$-calculus. With expressive power comes complexity. Mio showed that tree games are able to encode Blackwell games and, consequently, are not determined under deterministic strategies. We show that non-stochastic tree games with objectives recognisable by so-called game automata are determined under deterministic, finite memory strategies. Moreover, we give an elementary algorithmic procedure which, for an arbitrary regular language L and a finite non-stochastic tree game with a winning objective L decides if the game is determined under deterministic strategies.