Rackoff’s small witness property for the coverability problem is the standard means to prove tight upper bounds in vector addition systems (VAS) and many extensions. We show how to derive the same bounds directly on the computations of the VAS instantiation of the generic backward coverability algorithm. This relies on a dual view of the algorithm using ideal decompositions of downwards-closed sets, which exhibits a key structural invariant in the VAS case. The same reasoning readily generalises to several VAS extensions.

Joint work with Sylvain Schmitz presented at RP ’15; see https://hal.inria.fr/hal-01176755/.

The purpose of this seminar is to introduce the notion of ideals of well-quasi-orders. These irreducible downwards-closed sets of elements were first invented in the 1970’s but rediscovered in recent years in the theory of well-structured transition systems, notably by Finkel and Goubault-Larrecq. Ideals provide indeed finite effective representations of downwards-closed sets, in the same way as bases of minimal elements provide representations of upwards-closed sets.

After defining ideals and establishing some of their properties, I will illustrate their use in a concrete setting. I will present some recent results by Czerwiński, Martens, van Rooijen, and Zeitoun (FCT’15) on the decidability of piecewise-testable separability in the light of ideals. This seminar is also a warm-up for the next seminar on reachability in vector addition systems.

Descriptive complexity measure a problem in terms of the difficulty to express it. At first look this seems to have nothing to do with computational measures such as time and space. However it does have intimate links with classical computational complexity.

The most celebrated one is Fagin’s theorem linking the complexity class NP with the expressive power of existential second-order logic.

In this lecture we will study the Abiteboul-Vianu theorem saying that the separation of PTime and PSpace can be rephrased in terms of expressive powers of partial fixpoints versus least fixpoints.

The limitedness is a question of boundedness: given a function from words to integers described by some suitable model of finite state machines (distance automata, B-automata, …), determine whether the function it computes is bounded. It happens that for distance automata [Hashiguchi81, Leung82, Simon84] and B-automata [Kirsten05, Bojańczyk&C.06, C.09], this problem turns out to be decidable. This deep result is used in many situations, and in particular for solving the famous star-height problem [Hashiguchi88, Kirsten05]. (This problems asks, given a regular language L and a non-negative integer k, whether it is possible to describe L by means of a regular expression with nesting of Kleene stars bounded by k).

In his recent LICS15 paper, Bojańczyk gave a much shorter and self-contained proof of the decidability of limitedness (and in fact also star-height). It relies on a reduction to finite games of infinite duration, and involves arguments of positionality of stragegies in quantitative games [C.&Löding08]. The topic of this talk is the presentation of this elegant proof.

The decidability of limitedness was already presented in the LAAG seminar (using the algebraic approach of stabilization monoids), but the proof here is entirely different.

These two talks will continue the study of the equivalence problem of deterministic pushdown automata (DPDA).

The main focus of these talks will be on the computational complexity of this problem. We will give a proof of Stirling’s result that DPDA equivalence is primitive recursive.

More precisely, we will present a recent paper by Jancar that shows that in case two DPDAs are inequivalent they can be distinguished by a word whose length is bounded by a tower of exponentials of elementary height.

As in Arnaud’s talk we will view DPDA equivalence in terms of trace equivalence of deterministic first-order grammars.

This talk aims at going hand-in-hand with Arnaud’s talk but is intended to be self-contained as well.

These talks will be completely self-contained and require no background knowledge.

These two talks will continue the study of the equivalence problem of deterministic pushdown automata (DPDA).

The main focus of these talks will be on the computational complexity of this problem. We will give a proof of Stirling’s result that DPDA equivalence is primitive recursive.

More precisely, we will present a recent paper by Jancar that shows that in case two DPDAs are inequivalent they can be distinguished by a word whose length is bounded by a tower of exponentials of elementary height.

As in Arnaud’s talk we will view DPDA equivalence in terms of trace equivalence of deterministic first-order grammars.

This talk aims at going hand-in-hand with Arnaud’s talk but is intended to be self-contained as well.

These talks will be completely self-contained and require no background knowledge.

In this series of talks, we will present a proof of the decidability of the equivalence problem for deterministic pushdown automata. Namely given two deterministic pushdown automata, it is decidable if they accept the same language. This result was first proved by Géraud Sénizergues in 1997. His proof consists in two semi-decision procedures and hence while establishing decidability does not give an upper-bound on the complexity of the problem. In 2002, Colin Stirling gave a primitive recursive algorithm to decide the problem.

The aim of the talk is to present what seems to be the simplest self-contained proof of this result. We will present a proof based on the recent work of Petr Jancar which uses first-order grammars instead of deterministic pushdown automata. To keep the proof as simple as possible, we will present the proof giving two semi-decision procedures.

In this series of talks, we will present a proof of the decidability of the equivalence problem for deterministic pushdown automata. Namely given two deterministic pushdown automata, it is decidable if they accept the same language. This result was first proved by Géraud Sénizergues in 1997. His proof consists in two semi-decision procedures and hence while establishing decidability does not give an upper-bound on the complexity of the problem. In 2002, Colin Stirling gave a primitive recursive algorithm to decide the problem.

The aim of the talk is to present what seems to be the simplest self-contained proof of this result. We will present a proof based on the recent work of Petr Jancar which uses first-order grammars instead of deterministic pushdown automata. To keep the proof as simple as possible, we will present the proof giving two semi-decision procedures.

This talk is a continuation of the talk from two weeks ago, but it will be independent, so please consider coming even if you didn’t attend the first part.

The plan for this second session is:

1. explain how to obtain a universally non-regular automaton (by adding one state to last time’s example),
2. explain how to encode Minsky machines using bounded-error probabilistic automata, with two-way and one-way variants,
3. explain how to encode probabilistic automata using only one random probabilistic transition,

show the decidability of two problems: the equivalence and the finiteness problem. Both proofs rely on one observation: the reals with the addition and the multiplication form a field, and some linear algebra.

This talk is about probabilistic automata over finite words: such machines, when reading a letter, flip a coin to determine which transition to follow. Although quite simple, this computational model is quite powerful, and many natural problems are undecidable.

In this talk, I will review some of the most important undecidability results, with new simplified constructions.

This talk will be a continuation of my talk from 11th February. I will not assume knowledge of any material presented then except for basic notions of topology. During this talk I will move to the case of regular languages of infinite trees. Since there are known examples of such languages that are not Borel I will introduce the projective hierarchy. This hierarchy allows to study complexity of sets defined using big quantifiers (i.e. ranging over sets of naturals). I will focus on correspondence between topological complexity and automata-theoretic complexity measured by the Rabin-Mostowski index. My aim will be to prove certain results of strict containment using purely topological methods. At the end I hope to present some recent results about extensions of MSO.

The interplay between topology and automata theory has a form of synergy: descriptive set theory motivates new problems and methods in automata theory but on the other hand, automata theory introduces natural examples for classical topological concepts.

During this talk I will introduce basic notions of topology and descriptive set theory focusing on the case of infinite words. I’ll say what is the Borel hierarchy and the Wadge order. Then I’ll show how these tools are related to automata theory. I’ll try to argue that even from purely automata theoretic point of view, it is possible to obtain new results and new proofs by referring to topological concepts.

Non-determinism and walking mechanisms were considered already at the very beginning of automata theory. I will survey a few results connecting models of automata and transducers enhanced with non-determinism and two-wayness.

A classical result by Rabin and Scott shows that deterministic finite state automata are as expressive as their non-deterministic and two-way counterparts. The translation from two-way automata to one-way automata is easily seen to imply an exponential blowup in the worst case, even when one maps deterministic two-way models to non-deterministic one-way models. The converse translation, which is based on the subset construction and maps non-deterministic one-way automata to deterministic ones, also implies an exponential blowup. This latter translation, however, is not known to be optimal when one aims at removing non-determinism by possibly introducing two-wayness. In particular, the question of whether the exponential blowup is unavoidable in transforming non-determinism to two-wayness is open.

When one turns to models of transducers, some translations are not anymore possible. For example, one-way transducers (even those that exploit functional non-determinism) are easily seen to be less powerful than two-way transducers (even input-deterministic ones). A natural problem thus arises that amounts at characterizing the two-way transductions that can be implemented by one-way functional transducers. The latter problem was solved in recent paper by Filiot, Gauwin, Reynier, and Servais – however, some questions related to complexity remains open. Another interesting, but older, result by Hopcroft shows that functional non-determinism can be removed from two-way transducers, at the cost of an exponential blow-up. A similar transformation can be used to prove that two-way transducers are closed under functional composition.