In this talk I will first introduce finite automata on infinite trees as well as connections with logic and games. In a second part of the talk I will discuss several variants of the model and present challenges and recent results on these new classes.

In this talk I will give a brief overview over learning techniques for automata and its applications in verification. In particular, I will consider active automata inference techniques and survey some recent developments on inference of finite-state automata and its extensions (alternating automata, Büchi automata, predicate automata, register automata, etc.).

In the last years, we have been developing a theory for measuring the size of timed regular languages. More precisely, we generalize a classical approach introduced by Chomsky and Miller for finite automata: count words having n symbols and compute the exponential growth rate of their number (i.e.entropy). For timed automata, we replace cardinalities by volumes and define (volumetric) entropy similarly.

We described several techniques for approximating this number for a given automaton. One is based on the discretization of the behaviors, reducing the problem to that of finite automata. Other techniques depend on the spectral analysis of the functional operator associated to the execution of one discrete transition of the automaton. In a special case, entropy is even characterized symbolically, as the problem reduces to some ODE.

Various interpretations exist for this entropy, one of them information- theoretic : it answers the question how much information can be transmitted by letting a given timed automaton run for a given amount of transitions, knowing that its executions will be observed up to some precision. Some practical applications may however require knowing how much information can be encoded given some precision and given some time bound (without constraining the number of transitions). This variant, although it seems dual to the first question, opens new interesting challenges, which we are only starting to address.

…

Parametrized verification consists in analyzing the behavior of a model with some parameters to be instantiated. This framework is especially well-suited to model concurrent algorithms where the number of involved processes can be seen as a parameter. In this talk, I will introduce some parametrized models related to distributed systems together with the properties one might want to check on such models. I will then present some techniques to perform verification in this context. Finally I will give some new research directions linked to the analysis of distributed algorithms.

In this talk I will present the axis “automaton groups and semigroups” of the “automata” thematic team, and the classical decision and combinatorial questions we are interested in. Finally I will describe some of the results we have already obtained in that domain.

We present a decision procedure for checking entailment in a fragment of separation logic with inductive predicates. The inductive predicates specify data structures corresponding to finite nesting of various kinds of singly linked lists: acyclic or cyclic, nested lists, skip lists, etc. The decision procedure reduces the problem of checking entailment between two arbitrary formulas to the problem of checking entailment between a formula and an atom. Subsequently, in case the atom is a predicate, we reduce the entailment to testing membership of a tree derived from the formula in the language of a tree automaton derived from the predicate.

We describe the numbers with eventually periodic and purely periodic expansions in non-standard numeration systems such as beta-expansions (with Pisot numbers beta) and (variants of) continued fractions. This involves fractal sets such as Rauzy fractals.

…

Modern computer software is typically built with specialized concurrent or distributed objects, which encapsulate shared-memory accesses into higher-level abstract data types. These objects are designed to behave according to certain consistency criteria like linearizability, eventual or causal consistency. In this talk, we address the issue of verifying automatically whether the executions of an object satisfy a given consistency criterion. More precisely, we consider two problems: (1) checking whether one single execution is consistent, which is relevant for developing testing and bug finding algorithms, and (2) verifying whether all the executions of an implementation are consistent. In general, the first problem is NP-complete while the second is undecidable. We discuss relevant cases where these negative results can be circumvented, thus obtaining polynomial-time algorithms for deciding consistency of a single execution and decision procedures for checking whether a finite-state implementation is consistent. The latter type of results are usually proved using a reduction to standard reachability problems.