@InProceedings{ca03a, author = {Cachat, T.}, title = {Higher Order Pushdown Automata, the {C}aucal Hierarchy of Graphs and Parity Games}, booktitle = {Proceedings of the 30th International Colloquium on Automata, Languages, and Programming }, year = {2003}, series = lncs, publisher = sp, copyright = {\copyright \url{http://www.springer.de/comp/lncs/index.html}{Springer}}, pages = {556--569}, volume = {2719}, ps = {../../download/papers/cachat/ca03aICALP.ps }, pdf = {../../download/papers/cachat/ca03aICALP.pdf }, abstract = {We consider two-player parity games played on transition graphs of higher order pushdown automata. They are ``game-equivalent'' to a kind of model-checking game played on graphs of the infinite hierarchy introduced recently by Caucal. Then in this hierarchy we show how to reduce a game to a graph of lower level. This leads to an effective solution and a construction of the winning strategies. } } @InCollection{ca02d, author = {Cachat, T.}, title = {Two-Way Tree Automata Solving Pushdown Games}, booktitle = {Automata, Logics, and Infinite Games}, editor = {E. Gr\"{ĉ}del and W. Thomas and T. Wilke}, series = lncs, publisher = sp, copyright = {\copyright \url{http://www.springer.de/comp/lncs/index.html}{Springer}}, year = {2002}, pages = {303--317}, volume = {2500}, ps = {../../download/papers/cachat/ca02dDag.ps }, pdf = {../../download/papers/cachat/ca02dDag.pdf }, abstract = {The transition graph of the pushdown automaton defines the arena: the graph of the play and the partition of the vertex set needed to specify the parity winning condition. We know that such games are determined and that each of both players has a memoryless winning strategy on his winning region. The aim of this paper is to show how to compute effectively the winning region of Player 0 and a memoryless winning strategy. The idea is to simulate the pushdown system in the full W-tree, where W is a finite set of directions, and to use the expressive power of alternating two-way tree automata to answer these questions. Finally it is necessary to translate the 2-way tree automaton into an equivalent nondeterministic one-way tree automaton. } } @InProceedings{caduth02a, author = {Cachat, T. and Duparc, J. and Thomas, W.}, title = {Solving Pushdown Games with a Sigma-3 Winning Condition}, booktitle = {Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002}, pages = {322--336}, year = {2002}, volume = {2471}, series = lncs, publisher = sp, copyright = {\copyright \url{http://www.springer.de/comp/lncs/index.html}{Springer}}, ps = {../../download/papers/cachat/cdt02bCSL.ps }, pdf = {../../download/papers/cachat/cdt02bCSL.pdf }, abstract = {We study infinite two-player games over pushdown graphs with a winning condition that refers explicitly to the infinity of the game graph: A play is won by player 0 if some vertex is visited infinity often during the play. We show that the set of winning plays is a proper Sigma-3-set in the Borel hierarchy, thus transcending the Boolean closure of Sigma-2-sets which arises with the standard automata theoretic winning conditions (such as the Muller, Rabin, or parity condition). We also show that this Sigma-3-game over pushdown graphs can be solved effectively (by a computation of the winning region of player 0 and his memoryless winning strategy). This seems to be a first example of an effectively solvable game beyond the second level of the Borel hierarchy. } } @InProceedings{ca02c, author = {Cachat, T.}, title = {Uniform Solution of Parity Games on Prefix-Recognizable Graphs}, booktitle = {Proceedings of the 4th International Workshop on Verification of Infinite-State Systems }, series = {Electronic Notes in Theoretical Computer Science}, volume = {68}, issue = {6}, publisher = {Elsevier Science Publishers}, editor = {Antonin Kucera and Richard Mayr}, year = {2002}, copyright = {\copyright \url{http://www.elsevier.nl/locate/entcs/volume68.html}{Elsevier Science}}, ps = {../../download/papers/cachat/ca02cINFINI.ps }, pdf = {../../download/papers/cachat/ca02cINFINI.pdf }, abstract = {Walukiewicz gave in 1996 a solution for parity games on pushdown graphs: he proved the existence of pushdown strategies and determined the winner with an EXPTIME procedure. We give a new presentation and a new algorithmic proof of these results, obtain a uniform solution for parity games (independent of their initial configuration), and extend the results to prefix-recognizable graphs. The winning regions of the players are proved to be effectively regular, and winning strategies are computed. } } @InProceedings{ca02a, author = {Cachat, T.}, title = {Symbolic Strategy Synthesis for Games on Pushdown Graphs}, booktitle = {Proceedings of the 29th International Colloquium on Automata, Languages, and Programming }, pages = {704--715}, year = {2002}, volume = {2380}, series = lncs, publisher = sp, copyright = {\copyright \url{http://www.springer.de/comp/lncs/index.html}{Springer}}, ps = {../../download/papers/cachat/ca02aICALP.ps }, pdf = {../../download/papers/cachat/ca02aICALP.pdf }, abstract = {We consider infinite two-player games on pushdown graphs, the reachability game where the first player must reach a given set of vertices to win, and the Büchi game where he must reach this set infinitely often. We provide an automata theoretic approach to compute uniformly the winning region of a player and corresponding winning strategies, if the goal set is regular. Two kinds of strategies are computed: positional ones which however require linear execution time in each step, and strategies with pushdown memory where a step can be executed in constant time. } } @InProceedings{ca01b, author = {Cachat, T.}, title = {The Power of One-Letter Rational Languages}, booktitle = {Proceedings of the 5th international conference Developments in Language Theory}, pages = {145--154}, year = {2002}, volume = {2295}, series = lncs, publisher = sp, copyright = {\copyright \url{http://www.springer.de/comp/lncs/index.html}{Springer}}, ps = {../../download/papers/cachat/ca01bDLT.ps}, pdf = {../../download/papers/cachat/ca01bDLT.pdf}, abstract = {For any language $L$, let $\pow(L)=\{u^j\ |\ j\pgd 0,\ u\in L\}$ be the set of powers of elements of $L$. Given a rational language $L$ (over a finite alphabet), we study the question, posed in \cite{ths}, whether $\pow(L)$ {\em is rational or not.} While leaving open the problem in general, we provide an algorithmic solution for the case of one-letter alphabets. This case is still non trivial; our solution is based on Dirichlet's result that for two relatively prime numbers, their associated arithmetic progression contains infinitely many primes.} }