We will recall a generic technique for proving lower bounds for bisimulation equivalence checking (for which there was not enough time in my last LAAG talk) . First, we will introduce bisimulation equivalence and recall Jancar’s and Srba’s Defender’s Forcing lower bound technique. Then, we will apply this technique to different classes of infinite state systems for showing the following hardness results : (1) undecidability for prefix-recognizable graphs, (2) undecidability for vector addition systems, (3) nonelementary hardness for pushdown graphs, and (4) Ackermann hardness for equational graphs of finite out-degree.

In this third part, we will introduce stabilization monoids and cost functions, and show ho this constitutes a good framework in which the results of the previous talks can be unified.

This talk constitutes the continuation of the previous one, in which the star-height problem was reduced to a boundedness question.

In this second part, we will establish the decidability of this second problem, following the ideas of Leung, Simon, and Kirsten.

This talk is the first in a series of lecture intended to describe the main ideas and the use of automata limitedness and related questions.

The goal of the first session is to present the famous (restricted) star-height problem, and show the first steps toward its resolution. The question is the following: given a regular language L and a non-negative integer k, can we decide whether L can bee represented as a regular expression of star-height (i.e., nesting of Kleene stars) at most k. This problem has been open for 25 years unit Hashiguchi provided a proof in a series of four paper, between 81 and 88. This proof is notoriously difficult, and the presentation here will be based on the ideas in the more modern, and much simpler, proof of Kirsten (2005).

The idea behind both these proofs is to reduce the original problem to a question of existence of bounds for a function computed by some specific forms of automata (distance automata, nested-distance desert automata, B-automata, …). This idea goes much beyond the scope of the star-height problem, and I will try to convey this idea through several examples.

Les graphes expandeurs sont des graphes creux mais fortement connexes. Ils peuvent se substituer aux graphes denses ou même aux graphes complets dans beaucoup d’applications, et ainsi permettre une réduction de complexité de calcul ou d’aléa. Ils jouent un rôle clé dans plusieurs domaines de l’informatique fondamentale, notamment dans la dérandomisation et le pseudo-aléa.

Dans cet exposé nous présenterons les graphes expandeurs, leur(s) définition(s), quelques lemmes structurels fondamentaux, et quelques exemples de leur utilisation dans la dérandomisation. Nous esquisserons également la construction basée sur le produit zigzag.

Weak monadic second-order logic (WMSO) over the infinite binary tree has the same syntax as MSO, but second-order quantification is interpreted only over finite sets. It captures a strict subclass of the regular languages of infinite trees, but is expressive enough to subsume temporal logics like CTL.

In this talk, I will sketch the proofs showing the equivalence of WMSO and a form of automata called weak alternating automata. I will also prove Rabin’s characterization of WMSO: a language is weakly definable iff the language and its complement are recognizable by nondeterministic Büchi automata.

I will conclude by describing connections with recent work (joint with Thomas Colcombet, Denis Kuperberg, and Christof Löding) showing that given a Büchi automaton as input, it is decidable whether the language is definable in WMSO.

In 1969, Michael O. Rabin established that the class of regular tree languages (i.e. languages of infinite node-labelled complete binary trees accepted by non-deterministic tree automata) form a Boolean algebra. The goal of this talk is to present the underlying objects of this statement as well as a complete proof of it.

Hence, the structure of the talk will be as follows:

1. Main definitions and examples : infinite trees, parity tree automata and regular tree languages
2. Basic recalls on positional determinacy of two-player parity games on graphs (see previous LAAG seminar by Nathanaël Fijalkow)
3. Acceptance game and emptiness game/test for parity tree automata
4. Complementation of parity tree automata relying on positional determinacy and determinisation of automata on infinite words (see previous LAAG seminar).

I will assume no specific knowledge on automata nor games for that talk.

Last week, Thomas Colcombet presented a proof of Positional Determinacy for Parity Games, following a forward approach. In this second part, I will present a completely different proof of the same result based on ideas by Muller and Schupp, following a backward approach.

I will highlight the differences between the two approaches, and the applications of both techniques. In particular, I will explain why backward approaches naturally induce determinization procedures for automata over infinite words.

The talk will be self-contained, and in particular I will quickly recall all required definitions at the beginning.

In this sequence of two seminars, we will recall the basic definitions of games and parity games. We will give several proofs and applications of the most famous result in this context: the memoryless determinacy theorem. We will also see how some of these techniques naturally provide determinization procedures over infinite words.

This is in preparation to the seminars after the holidays, that will aim at presenting the results on the monadic theory of the infinite binary tree.