Journées de rentrée ASV 2017

Lundi 27 novembre · Salle 3052, Bâtiment Sophie Germain

9h30-10h Olivier Serre Tree Automata and variants

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.

10h-10h30 Peter Habermehl Automata theory meets verification: (Machine) Learning

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.).

10h30 – 11h Pause café

11h-11h30 Aldric Degorre Entropy of timed regular languages: current framework and new challenges

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.

11h30-12h Amélie Gheerbrant Querying databases: are you certain you want me to answer?

12h-12h30 Arnaud Sangnier From parametrized verification to analysis of distributed algorithms

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.

12h30 – 14h Repas

14h-14h30 Ines Klimann A brief introduction to automaton groups and semigroups

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.

14h30-15h Mihaela Sighireanu Tree automata for verification of data structures

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.

15h-15h30 Wolfgang Steiner Periodic beta-expansions and continued fractions

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.

15h30 – 16h Pause café

16h-16h30 Jean-Éric Pin Difference hierarchies

16h30-17h Constantin Enea Checking Consistency Properties: Tractable Reductions to Reachability

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.