------------- updated Wed Nov 14 11:16:55 CET 2007 -------------- @String{ sp = {Springer}} @String{ lncs = {Lecture Notes in Computer Science}} @misc{cw07report, author = {Thierry Cachat and Igor Walukiewicz}, title = {The Complexity of Games on Higher Order Pushdown Automata}, year = {2007}, month = may, howpublished = {available at \url{http://hal.archives-ouvertes.fr/hal-00144226} and \url{http://fr.arxiv.org/abs/0705.0262}}, abstract = {We prove an $n$-{\sc exptime} lower bound for the problem of deciding the winner in a reachability game on Higher Order Pushdown Automata (HPDA) of level $n$. This bound matches the known upper bound for parity games on HPDA. As a consequence the $\mu$-calculus model checking over graphs given by $n$-HPDA is $n$-{\sc exptime} complete.} } @InProceedings{acstl07AB, author = {Eugene Asarin and Thierry Cachat and Alexander Seliverstov and Tayssir Touili and Vassily Lyubetsky}, title = {Attenuation Regulation as a Term Rewriting System}, booktitle = {Second International Conference on Algebraic Biology, AB'07}, year = {2007}, series = lncs, publisher = sp, pages = {81-94}, abstract = {The classical attenuation regulation of gene expression in bacteria is considered. We propose to represent the secondary RNA structure in the leader region of a gene or an operon by a term, and we give a probabilistic term rewriting system modeling the whole process of such a regulation. } } @InProceedings{ca06bFSTTCS, author = {Cachat, Thierry}, title = {Tree Automata Make Ordinal Theory Easy}, booktitle = {Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'06}, year = {2006}, series = lncs, publisher = sp, pages = {285--296}, volume = {4337}, abstract = {We give a new simple proof of the decidability of the First Order Theory of $(\w^{\w^i},+)$ and the Monadic Second Order Theory of $(\w^i,<)$, improving the complexity in both cases. Our algorithm is based on tree automata and a new representation of (sets of) ordinals by (infinite) trees. } } @inproceedings{ca06aATVA, author = {Thierry Cachat}, title = {Controller Synthesis and Ordinal Automata.}, booktitle = {Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis, ATVA'06}, year = {2006}, series = lncs, publisher = sp, pages = {215-228}, volume = {4218}, ee = {http://dx.doi.org/10.1007/11901914_18}, abstract = {Ordinal automata are used to model physical systems with Zeno behavior. Using automata and games techniques we solve a control problem formulated and left open by Demri and Nowak in 2005. It involves partial observability and a new synchronization between the controller and the environment. } } @inproceedings{abccg05aMSR, author = {Altisen, Karine and Bouyer, Patricia and Cachat, Thierry and Cassez, Franck and Gardey, Guillaume}, booktitle = {{A}ctes du 5{\`e}me {C}olloque sur la {M}od{\'e}lisation des {S}yst{\`e}mes {R}{\'e}actifs ({MSR}'05)}, address = {Autrans, France}, editor = {Alla, Hassane and Rutten, {\'E}ric}, month = oct, pages = {367-380}, publisher = {Herm{\`e}s}, title = {Introduction au contr{\^o}le des syst{\`e}mes temps-r{\'e}el}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MSR05-control.pdf}, year = {2005}, abstract = {In this paper we give a quick overview of the area of control of real-time systems.} } @PhDThesis{ca03bPhD, author = {Cachat, T.}, school = {RWTH Aachen}, title = {Games on Pushdown Graphs and Extensions}, year = {2003}, abstract = {Two player games are a standard model of reactive computation, where e.g. one player is the controller and the other is the environment. A game is won by a player if she has a winning strategy, i.e., if she can win every play. Given a finite description of the game, our aim is to compute the winner and a winning strategy. For finite graphs these problems have been solved for a long time, although some complexity questions remain open. We consider several classes of infinite graphs, from transition graphs of pushdown automata up to graphs of the Caucal hierarchy, and we investigate different winning conditions: reachability, recurrence (Büchi), parity, and a Sigma_3-condition. Two kinds of techniques are developed: a symbolic approach based on finite automata recognizing infinite sets of configurations and a game simulation which reduces a given game into a simpler one and solves it. Different kinds of strategies are also constructed: either positional or based on pushdown stack memories. } } @InProceedings{ca03aICALP, 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 (ICALP'03)}, 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{ca02dDag, author = {Cachat, T.}, title = {Two-Way Tree Automata Solving Pushdown Games}, booktitle = {Automata, Logics, and Infinite Games}, editor = {E. Gr{\"a}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{cdt02bCSL, 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'02)}, 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{ca02cINFINI, 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 (Infinity'02)}, 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{ca02aICALP, author = {Cachat, T.}, title = {Symbolic Strategy Synthesis for Games on Pushdown Graphs}, booktitle = {Proceedings of the 29th International Colloquium on Automata, Languages, and Programming (ICALP'02)}, 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{ca01bDLT, author = {Cachat, T.}, title = {The Power of One-Letter Rational Languages}, booktitle = {Proceedings of the 5th international conference Developments in Language Theory (DLT'01)}, 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.} }