Stochastic games and their complexities

W pracy badamy klasę gier zwanych grami rozgałęziającymi. Gry rozgałęziające zostały wprowadzone przez Mio w celu uchwycenia semantyki probabilistycznego rachunku mu. Stanowią one podklasę stochastycznych dwuosobowych gier turowych o sumie zerowej i nieskończonym czasie rozgrywki. Gry rozgałęziające rozszerzają gry Gale'a-Stewarta poprzez to, że pozwalają podzielić rozgrywkę, tworząc nowe podgry, które są rozgrywane równolegle i niezależnie. Z tego powodu rozgrywka gry rozgałęziającej ma strukturę drzewiastą, w przeciwieństwie do liniowej struktury rozgrywek w grach Gale'a-Stewarta. W niniejszej rozprawie doktorskiej skupiamy się na regularnych grach rozgałęziających. Są to te gry rozgałęziające, w których funkcja wypłaty jest funkcją charakterystyczną regularnego zbioru nieskończonych drzew, to jest zbioru nieskończonych drzew, który jest rozpoznawany przez skończony automat na drzewach. W pracy skupiamy się głównie na problemie determinacji, na obliczalności wartości gier oraz na powiązanym z grami problemie obliczania miary regularnych zbiorów drzew. Determinacja jest to własność gry, która gwarantuje, że żaden z graczy nie zyska ani nie straci przewagi poprzez ujawnienie swojej strategii na początku gry. Pokazujemy, że gry rozgałęziające nie muszą być zdeterminowane: ani gdy zbiory wygrywające są topologicznie proste, ani w przypadku, gdy dopuścimy strategie mieszane. Z drugiej strony, pokazujemy, że regularne gry rozgałęziające z otwartymi zbiorami wygrywającymi są zdeterminowane w strategiach mieszanych. Co więcej, pokazujemy, że te gry są zdeterminowane w strategiach czystych, jeśli zbiory wygrywające są rozpoznawalne przez automaty growe. Dla obu rezultatów konstruujemy przykłady pokazujące granice użytych technik. Rozwiązujemy także problem obliczalności wartości gier pokazując, że mieszane wartości niestochastycznych gier rozgałęziających nie są obliczalne oraz, że czyste wartości gier stochastycznych także nie są obliczalne. Z drugiej strony, opisujemy algorytm, który wylicza czyste wartości niestochastycznych gier rozgałęziających. Częściowo rozwiązujemy problem obliczania miar regularnych zbiorów drzew. Przedstawiamy algorytm, który oblicza miarę zbioru drzew, względem jednorodnej miary na drzewach, w dwu przypadkach: kiedy zbiór jest zdefiniowany poprzez formułę pierwszego rzędu nie używającą relacji potomka oraz gdy zbiór jest zdefiniowany poprzez boolowską kombinację zapytań koniunkcyjnych. Wreszcie, pokazujemy w jaki sposób możemy zastosować bogate techniki teorii gier w praktyce. Proponujemy procedurę, która na podstawie szeregu czasowego tworzy reaktywny model pozwalający przewidzieć ewolucję modelowanego systemu i tworzyć strategie pozwalające zrealizować uprzednio zdefiniowane cele, jeśli takie strategie istnieją. Używamy wyżej wymienionej procedury, by stworzyć grę bazującą na procesach decyzyjnych Markowa, która pozwala przewidzieć i kontrolować poziomy obecności szkodników w tropikalnym sadzie owocowym.

We study a class of games introduced by Mio to capture the probabilistic μ-calculi called branching games. They are a subclass of stochastic two-player zero-sum turn-based infinite-time games of imperfect information. Branching games extend Gale-Stewart games by allowing players to split the execution of a play into new concurrent sub-games that continue their execution independently. In consequence, the play of a branching game has a tree-like structure, as opposed to linearly structured plays of Gale-Stewart games. In this thesis, we focus our attention on regular branching games. Those are the branching games whose pay-off functions are the indicator functions of regular sets of infinite trees, i.e. the sets recognisable by finite tree automata. We study the problems of determinacy, game value computability, and the related problem of computing a measure of a regular set of infinite trees. Determinacy is a property of a game that guarantees that none of the players gains or loses an advantage by revealing their strategy at the start of the game. In general, branching games are not determined: not even under mixed strategies nor when the winning sets are topologically simple. On the positive side, we show that regular branching games with open winning sets are determined under mixed strategies. Moreover, we show that game automata definable winning sets guarantee a stronger version of determinacy – the determinacy under pure strategies. Both results are accompanied by examples showing the limits of used techniques. We give an answer to the problem of computing a value of a regular branching game. We show that a mixed value of a non-stochastic branching game is uncomputable and that a pure value of a stochastic branching game is also uncomputable. On the other hand, we provide an algorithm that computes all pure values of a given non-stochastic regular branching game. We partially solve the problem of computing measures of regular sets of trees. We provide an algorithm that computes the uniform measure of a regular winning set in two cases. Either when it is defined by a first-order formula with no descendant relation or when it is defined by a Boolean combination of conjunctive queries. Finally, we use real-life data to show how to incorporate game-theoretic techniques in practice. We propose a general procedure that given a time series of data extracts a reactive model that can be used to predict the evolution of the system and advise on the strategies to achieve predefined goals. We use the procedure to create a game based on Markov decision processes that is used to predict and control level of pest in a tropical fruit farm.