Abstract:
The work at hand deals with infinite games played on finite graphs. Such games are widely used in automatic verification, model checking, automata and formal logics. In particular, we are interested in perfect information games that are played between two players, called Player 0 and Player 1, over a finite bipartite directed graphs. Each play starts from a node in the underlying graph. The players play the game by moving the token alternatively along the edges. If a play satisfies the winning condition of the game, then we say Player 0 wins the play otherwise Player 1 wins. We are interested in to investigate algorithmic questions about games. The emphasis is placed on the following three interrelated algorithmic problems. 1. Given a game, we want to solve the game. This means that we want to design an algorithm that finds all the winning nodes for Player 0 and all the winning nodes for Player 1 in the game. 2. Given a game, we want to extract finite state winning strategies. This means that we want to design an algorithm that, for the given game, builds finite state automata that realize winning strategies. 3. We want to investigate the above two problems in dynamically changing games. This means that we want to design algorithms, for the above two problems, for games played over the finite bipartite directed graphs that undergo a series of updates. These updates include insertions and deletions of edges and nodes.