Every language recognized by a non-deterministic finite automaton can be recognized by a deterministic automaton, at the cost of a potential increase of the number of states, which in the worst case can go from $n$ states to $2^n$ states. In this article, we investigate this classical result in a probabilistic setting where we take a deterministic automaton with $n$ states uniformly at random and add just one random transition. These automata are almost deterministic in the sense that only one state has a non-deterministic choice when reading an input letter. In our model, each state has a fixed probability to be final. We prove that for any $d\geq 1$, with non-negligible probability the minimal (deterministic) automaton of the language recognized by such an automaton has more than $n^d$ states; as a byproduct, the expected size of its minimal automaton grows faster than any polynomial. Our result also holds when each state is final with some probability that depends on $n$, as long as it is not too close to $0$ and $1$, at distance at least $\Omega(\frac1{\sqrt{n}})$ to be precise, therefore allowing models with a sublinear number of final states in expectation.

Every language recognized by a non-deterministic finite automaton can be recognized by a deterministic automaton, at the cost of a potential increase of the number of states, which in the worst case can go from n states to 2ⁿ states. In this article, we investigate this classical result in a probabilistic setting where we take a deterministic automaton with n states uniformly at random and add just one random transition. These automata are almost deterministic in the sense that only one state has a non-deterministic choice when reading an input letter. In our model each state has a fixed probability to be final. We prove that for any d ≥ 1, with non-negligible probability the minimal (deterministic) automaton of the language recognized by such an automaton has more than n^d states; as a byproduct, the expected size of its minimal automaton grows faster than any polynomial. Our result also holds when each state is final with some probability that depends on n, as long as it is not too close to 0 and 1, at distance at least Ω(1/√n) to be precise, therefore allowing models with a sublinear number of final states in expectation.

This article studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely, those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.

This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

We investigate the connection between properties of formal languages and properties of their generating series, with a focus on the class of holonomic power series. We first prove a strong version of a conjecture by Castiglione and Massazza: weakly-unambiguous Parikh automata are equivalent to unambiguous two-way reversal bounded counter machines, and their multivariate generating series are holonomic. We then show that the converse is not true: we construct a language whose generating series is algebraic (thus holonomic), but which is inherently weakly-ambiguous as a Parikh automata language. Finally, we prove an effective decidability result for the inclusion problem for weakly-unambiguous Parikh automata, and provide an upper-bound on its complexity.

An algorithm for computing optimal strategies in pushdown reachability games was given by Cachat. We show that the information tracked by this algorithm is too coarse and the strategies constructed are not necessarily optimal. We then show that the algorithm can be refined to recover optimality. Through a further non-trivial argument the refined algorithm can be run in 2EXPTIME by bounding the play-lengths tracked to those that are at most doubly exponential. This is optimal in the sense that there exists a game for which the optimal strategy requires a doubly exponential number of moves to reach a target configuration.

We consider imperfect information stochastic games where we require the players to use pure ( i.e. non randomised) strategies. We consider reachability, safety, Büchi and co-Büchi objectives, and investigate the existence of almost-sure/positively winning strategies for the first player when the second player is perfectly informed or more informed than the first player. We obtain decidability results for positive reachability and almost-sure Büchi with optimal algorithms to decide existence of a pure winning strategy and to compute one if it exists. We complete the picture by showing that positive safety is undecidable when restricting to pure strategies even if the second player is perfectly informed.

A pattern is encountered in a word if some infix of the word is the image of the pattern under some non-erasing morphism. A pattern p is unavoidable if, over every finite alphabet, every sufficiently long word encounters p. A theorem by Zimin and independently by Bean, Ehrenfeucht and McNulty states that a pattern over n distinct variables is unavoidable if, and only if, p itself is encountered in the n-th Zimin pattern. Given an alphabet size k, we study the minimal length f(n,k) such that every word of length f(n,k) encounters the n-th Zimin pattern. It is known that f is upper-bounded by a tower of exponentials. Our main result states that f(n,k) is lower-bounded by a tower of n-3 exponentials, even for k=2. To the best of our knowledge, this improves upon a previously best-known doubly-exponential lower bound. As a further result, we prove a doubly-exponential upper bound for encountering Zimin patterns in the abelian sense.

International audience

This article is inspired by two works from the early 90s. The first one is by Bogaert and Tison who considered a model of automata on finite ranked trees where one can check equality and disequality constraints between direct subtrees: they proved that this class of automata is closed under Boolean operations and that both the emptiness and the finiteness problem of the accepted language are decidable. The second one is by Niwinski who showed that one can compute the cardinality of any ω-regular language of infinite trees.

We consider games with two antagonistic players -- Éloïse (modelling a program) and Abelard (modelling a byzantine environment) -- and a third, unpredictable and uncontrollable player, that we call Nature. Motivated by the fact that the usual probabilistic semantics very quickly leads to undecidability when considering either infinite game graphs or imperfect information, we propose two alternative semantics that leads to decidability where the probabilistic one fails: one based on counting and one based on topology.

No abstract available.

We study finite automata running over infinite binary trees. A run of such an automaton over an input tree is a tree labeled by control states of the automaton: the labeling is built in a top-down fashion and should be consistent with the transitions of the automaton. A branch in a run is accepting if the ω-word obtained by reading the states along the branch satisfies some acceptance condition (typically an ω-regular condition such as a Büchi or a parity condition). Finally, a tree is accepted by the automaton if there exists a run over this tree in which every branch is accepting. In this article, we consider two relaxations of this definition, introducing a qualitative aspect. First, we relax the notion of accepting run by allowing a negligible set (in the sense of measure theory) of nonaccepting branches. In this qualitative setting, a tree is accepted by the automaton if there exists a run over this tree in which almost every branch is accepting. This leads to a new class of tree languages, qualitative tree languages . This class enjoys many good properties: closure under union and intersection (but not under complement), and emptiness is decidable in polynomial time. A dual class, positive tree languages , is defined by requiring that an accepting run contains a non-negligeable set of branches. The second relaxation is to replace the existential quantification (a tree is accepted if there exists some accepting run over the input tree) with a probabilistic quantification (a tree is accepted if almost every run over the input tree is accepting). For the run, we may use either classical acceptance or qualitative acceptance. In particular, for the latter, we exhibit a tight connection with partial observation Markov decision processes. Moreover, if we additionally restrict operation to the Büchi condition, we show that it leads to a class of probabilistic automata on infinite trees enjoying a decidable emptiness problem. To our knowledge, this is the first positive result for a class of probabilistic automaton over infinite trees.

Higher-order recursion schemes (HORS) have recently received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. This paper contributes to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspective. We introduce the first practical model-checking algorithm that acts on a generalisation of pushdown automata equi-expressive with HORS called collapsible pushdown systems (CPDS). At its core is a substantial modification of a recently studied saturation algorithm for CPDS. In particular it is able to use information gathered from an approximate forward reachability analysis to guide its backward search. Moreover, we introduce an algorithm that prunes the CPDS prior to model-checking and a method for extracting counter-examples in negative instances. We compare our tool with the state-of-the-art verification tools for HORS and obtain encouraging results. In contrast to some of the main competition tackling the same problem, our algorithm is fixed-parameter tractable, and we also offer significantly improved performance over the only previously published tool of which we are aware that also enjoys this property. The tool and additional material are available from http://cshore.cs.rhul.ac.uk.

Higher-order recursion schemes are rewriting systems for simply typed terms and they are known to be equi-expressive with collapsible pushdown automata (CPDA) for generating trees. We argue that CPDA are an essential model when working with recursion schemes. First, we give a new proof of the translation of schemes into CPDA that does not appeal to game semantics. Second, we show that this translation permits to revisit the safety constraint and allows CPDA to be seen as Krivine machines. Finally, we show that CPDA permit one to prove the effective MSO selection property for schemes, subsuming all known decidability results for MSO on schemes.

We study the distribution of the number of accessible states in deterministic and complete automata with n states over a k-letters alphabet. We show that as n tends to infinity and for a fixed alphabet size, the distribution converges in law toward a Gaussian centered around vk n and of standard deviation equivalent to sk n^(1/2), for some explicit constants vk and sk. Using this characterization, we give a simple algorithm for random uniform generation of accessible deterministic and complete automata of size n of expected complexity O(n^(3/2)), which matches the best methods known so far. Moreover, if we allow a variation around n in the size of the output automaton, our algorithm is the first solution of linear expected complexity. Finally we show how this work can be used to study accessible automata (which are difficult to apprehend from a combinatorial point of view) through the prism of the simpler deterministic and complete automata. As an example, we show how the average complexity in O(n log log n) for Moore's minimization algorithm obtained by David for deterministic and complete automata can be extended to accessible automata.

We study finite automata running over infinite binary trees and we relax the notion of accepting run by allowing a negligible set (in the sense of measure theory) of non-accepting branches. In this qualitative setting, a tree is accepted by the automaton if there exists a run over this tree in which almost every branch is accepting. This leads to a new class of tree languages, called the qualitative tree languages that enjoys many properties. Then, we replace the existential quantification -- a tree is accepted if there exists some accepting run over the input tree -- by a probabilistic quantification -- a tree is accepted if almost every run over the input tree is accepting. Together with the qualitative acceptance and the Büchi condition, we obtain a class of probabilistic tree automata with a decidable emptiness problem. To our knowledge, this is the first positive result for a class of probabilistic automaton over infinite trees.

Let R be a class of generators of node-labelled infinite trees, and Lbe a logical language for describing correctness properties of the setrees. Given r in R and phi in L, we say that r_phi is aphi-reflection of r just if (i) r and r_phi generate the same underlying tree, and (ii) suppose a node u of the tree t(r) generated by r has label f, then the label of the node u of t(r_phi) is f* if uin t(r) satisfies phi; it is f otherwise. Thus if t(r) is the computation tree of a program r, we may regard r_phi as a transform of R that can internally observe its behaviour against a specification phi. We say that R is (constructively) reflective w.r.t. L just if there is an algorithm that transforms a given pair (r,phi) to r_phi. In this paper, we prove that higher-order recursion schemes are reflective w.r.t. both modal mu-calculus and monadic second order(MSO) logic. To obtain this result, we give the first characterisation of the winning regions of parity games over the transition graphs of collapsible pushdown automata (CPDA): they are regular sets defined by a new class of automata. (Order-n recursion schemes are equi-expressive with order-n CPDA for generating trees.) As a corollary, we show that these schemes are closed under the operation of MSO-interpretation followed by tree unfolding a la Caucal.

In this paper we consider parity games defined by higher-order pushdown automata. These automata generalise pushdown automata by the use of higher-order stacks, which are nested "stack of stacks" structures. Representing higher-order stacks as well-bracketed words in the usual way, we show that the winning regions of these games are regular sets of words. Moreover a finite automaton recognising this region can be effectively computed.A novelty of our work are abstract pushdown processes which can be seen as (ordinary) pushdown automata but with an infinite stack alphabet. We use the device to give a uniform presentation of our results.From our main result on winning regions of parity games we derive a solution to the Modal Mu-Calculus Global Model-Checking Problem for higher-order pushdown graphs as well as for ranked trees generated by higher-order safe recursion schemes.

We investigate families of infinite automata for context-sensitive languages. An infinite automaton is an infinite labeled graph with two sets of initial and final vertices. Its language is the set of all words labelling a path from an initial vertex to a final vertex. In 2001, Morvan and Stirling proved that rational graphs accept the context-sensitive languages between rational sets of initial and final vertices. This result was later extended to sub-families of rational graphs defined by more restricted classes of transducers. languages. Our contribution is to provide syntactical and self-contained proofs of the above results, when earlier constructions relied on a non-trivial normal form of context-sensitive grammars defined by Penttonen in the 1970's. These new proof techniques enable us to summarize and refine these results by considering several sub-families defined by restrictions on the type of transducers, the degree of the graph or the size of the set of initial vertices.