Tree games with regular objectives

Marcin Przybyłko
(University of New Caledonia, University of Warsaw)

We study tree games developed recently by Matteo Mio as a game interpretation of the probabilistic μ-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.

In Adriano Peron and Carla Piazza: Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2014), Verona, Italy, 10th - 12th September 2014, Electronic Proceedings in Theoretical Computer Science 161, pp. 231–244.
Published: 24th August 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.161.20 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org