History-deterministic (HD) automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter, so that if the overall input word has an accepting run, then the constructed run is also accepting. These automata have found important applications in reactive synthesis. In this talk I will discuss our work on a generalisation of HD automata called stochastically resolvable automata : the strategy for resolving non-determinism may randomise, and the input word only needs to be accepted with some threshold probability.

Not all NFAs are stochastically resolvable and a key challenge is to recognise such automata. It turns out that it is undecidable to check if a given NFA is stochastically resolvable with a given threshold. The problem however becomes decidable for the class of finitely-ambiguous automata. For the general question of stochastically resolving an automaton with any arbitrary positive threshold, the problem is decidable for automata over a unary alphabet, as well as for finitely-ambiguous automata. 

I will also discuss natural extensions of this concept to automata over infinite words and touch on some applications. I will conclude with several interesting open questions on this topic.

Amazigh Amrane gave a talk at GALOP 2025 on 19 July 2025.

From July 1 to August 29, 2025, Oscar Peyron is joining the team for a research internship. The objective of this internship is to develop efficient learning algorithms for concurrent systems and/or to implement existing ones in C++.

Two half-days dedicated to scientific presentations and discussions

The talk presents a conjectural characterisation of visibly pushdown languages (VPLs) in AC^0 obtained with Stefan Göller. The approach builds on recognisability by Ext-algebras, extending monoid morphism methods for regular languages. VPLs are classified into three categories: those in AC^0, those not in AC^0, and intermediate languages whose complexity remains unclear. The characterisation is complete up to the understanding of these intermediate languages.

Uli Fahrenberg gave a talk at DAAL 2025.

Alexandre Duret-Lutz has been invited as a keynote speaker at SPIN 2025.

This talk presents a formal approach to constructing reliable and efficient composite fog services in distributed IoT environments. It combines functional, non-functional, and transactional aspects, using heuristic and adaptive composition strategies. The approach also includes a correct-by-construction verification method, illustrated on a distributed e-health application.

Adrien Pommellet gave a talk at Paris ACTS

Active automata learning constructs models of software/hardware components from input/output observations. Timing information is crucial for many systems, motivating an extension of Mealy machine learning to machines with timers (MMTs). This algorithm generalizes the L# algorithm to timed settings using symbolic queries implemented via finitely many concrete queries.

Uli Fahrenberg has been invited as a speaker at the Estonian Winter School in Computer Science.

Uli Fahrenberg has been invited to the Colloquium for the 60th anniversary of Martin Fränzle in Oldenburg.

Adrien Pommellet gave a talk at the Workshop on Learning and Logic (LeaLog@CSL).

Amazigh Amrane was invited on January 23 to the Theoretical Computer Science Seminar at the University of Rouen.

Spot 2.12.2 was released.

Didier Verna has been invited to join the program committee of DocEng (ACM SIGWEB Symposium on Document Engineering) this year.

We show how to efficiently solve problems involving a quantitative measure, here called energy, as well as a qualitative acceptance condition, expressed as a Büchi or Parity objective, in finite weighted automata and in one-clock weighted timed automata. Solving the former problem and extracting the corresponding witness is our main contribution and is handled by a modified version of the Bellman-Ford algorithm interleaved with Couvreur’s algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source platforms TChecker and Spot.