by Véronique Bruyère, Olivier Carton and Géraud Sénizergues
Dans cet article, on résout le problème de l'équivalence de ces automates restreints aux ordres dispersés et dénombrables. Plus généralement, on montre que le problème de l'inclusion est décidable. Notre approche pour résoudre le problème de l'inclusion utilise de le théorème de Rabin. L'idée est la suivante. Les chemins acceptants sont décrits par une formule du second ordre monadique avec deux fonctions successeur. De cette façon, le problème de l'inclusion pour les automates sur les ordres dispersés est réduit au problème de l'inclusion pour les automates d'arbres. Ceci établit en outre un lien intéressant entre les automates d'arbres et les automates sur les ordres.
In this paper, we solve the equivalence problem for these automata on scattered and countable linear orderings. More generally, we show that the inclusion problem is decidable. Our approach to solve the inclusion problem uses the Rabin tree theorem. The idea is the following. Accepting paths in an automaton are described by a monadic second-order formula using two successor functions. In this way, the inclusion problem for automata on scattered linear orderings is reduced to the inclusion problem for tree automata. This establishes an interesting link between tree automata and automata on linear orderings.