The seminar of the research group AAAutomata and Applications is held every 23 weeks, usually online. It is open to the public.
The languages of the seminar are French and English. Talks may be given, and questions asked, in any of the two languages. If you want to participate in the seminar, or if you want to propose a talk, send an email to daniel.stan@epita.fr or philipp.schlehuber@epita.fr !
Upcoming Talk

Tuesday 10 October, 10:00am at ?? and online at ??

Speaker: Francesco Parolini

Title: Inclusion Testing of Büchi Automata Based on WellQuasiorders

In this seminar we present an algorithmic framework to decide whether inclusion holds between languages of infinite words over a finite alphabet. Our approach falls within the class of Ramseybased methods and relies on a least fixpoint characterization of ωlanguages leveraging ultimately periodic infinite words of type uv^ω, with u a finite prefix and v a finite period of an infinite word. We put forward an inclusion checking algorithm between Büchi automata, called BAInc, designed as a complete abstract interpretation using a pair of wellquasiorders on finite words. We implemented BAInc in a tool called BAIT that we experimentally evaluated against the stateoftheart. Our experimental results show that BAIT advances the stateoftheart on an overwhelming majority of these benchmarks.

Previous Talks

Friday 7 July, 14:00 at KB 404 and on zoom

Speaker: Shufang Zhu

Title: On the Power of LTLf in Assured Autonomy

Assured Autonomy is a novel area that merges Artificial Intelligence (AI) and Formal Methods (FM), concerning building AI agents that autonomously deliberate how to act in a changing, incompletely known, unpredictable environment under formal guarantees. A popular specification language for describing formal guarantees is Linear Temporal Logic (LTL) from FM. However, LTL is interpreted over infinite traces (relating to nonterminating systems). Since AI agents are not dedicated to a single task in their complete life cycle, but are supposed to accomplish one task after another, AI applications often employ a finitetrace variant of LTL, denoted as LTLf. In particular, the study of LTLf synthesis brings the intellectual merit of achieving Assured Autonomy by allowing agents to automatically construct programs with guarantees to meet their tasks specified in LTLf. In this presentation, I will review an evolving journey toward Assured Autonomy through LTLf synthesis. Starting from an attempt to devise a symbolic backward LTLf synthesis framework, which has demonstrated its significant efficiency in various applicable scenarios, the journey evolves into a forward LTLf synthesis technique that highlights several interesting avenues of future work in the context of Markovian Decision Process.

About the speaker: Shufang Zhu is a Postdoctoral researcher at the Department of Computer Science, University of Oxford, working with Prof. Giuseppe De Giacomo on his Advanced ERC project WhiteMech. Her research concerns interdisciplinary knowledge across artificial intelligence (AI) and formal methods (FM), focusing on automated reasoning, planning, and synthesis. She received her Ph.D. in March 2020, at East China Normal University (ECNU), Shanghai, China, under the supervision of Prof. Geguang Pu. During her Ph.D., she received a scholarship from the Chinese Scholarship Council (CSC) and studied as a visiting Ph.D. student (August 2016 to Feb 2018) at Rice University under the supervision of Prof. Moshe Y. Vardi.


Tuesday 11 April 15:30:

Speaker: Martin Pépin

Title: Directed Ordered Acyclic Graphs, asymptotic analysis and efficient random sampling

Directed Acyclic Graphs (DAGs) are directed graphs in which there is no path from a vertex to itself. They are an omnipresent data structure in computer science and the problem of counting the DAGs of given number of vertices has been solved in the 70’s by Robinson. In this talk, I will introduce a new class of DAGs (DOAGs for Directed Ordered Acyclic Graphs), endowed with an independent ordering of the children of each vertex. They offer a new modelling tool for objects arising from the compaction of treelike structures. For this class I will describe a recursive decomposition scheme that is amenable to effective random sampling with control over the number of edges. I will also present an optimised uniform sampler, for the case when the number of edges is free, whose design follows naturally from our asymptotic enumeration results.

At KB000 and online on jitsi


Friday 17 March 10:00:

Speaker: Daniel Stan

Title: Concurrent Stochastic Lossy Channel Games

Lossy channel systems is a classical model of infinite state space systems for representing proccesses communicating through unbounded FIFO channels. In this formalism, we assume the channels not to be reliable, that is to say, there is always a small fixed probability for a message to be dropped before being read. This assumption is crucial to regain decidability for simple problems as checking reachability of a configuration/state, through the use of wellquasiordering and backward reachability techniques. After a recall of these techniques, we introduce an extension where two players −with antagonistic objectives− control the transitions and operations on the channels, concurrently. We first revisit algorithms for solving 2player zerosum stochastic qualitative reachability games on a finite state space, then show how these can be extended to the lossy channel case. We further discuss decidability of more complex objectives as almostsure Büchi/coBüchi objectives, as well as conjunctions of qualitative objectives. Joint work with Parosh Aziz Abdullah, Anthony W. Lin and Muhammad Najib.

At KB001 and https://meet.jit.si/seminarAA


Monday 20 February 14:00:

Speaker: Vincent Botbol

Title: Static analysis of Michelson smartcontracts using abstract interpretation

In this talk, we briefly introduce the Toss blockchain and Michelson, its statically typed stackedbased smartcontract language. Then, we present a static analysis for Michelson smartcontracts using abstract interpretation. Our tool automatically infers (numerical) invariants allowing us to verify numerical safety properties along with more blockchainspecific functional properties, e.g., validating user authentication patterns, analyzing the evolution of contract’s storage, determining an upperbound gas usage of a smartcontract,… This ongoing work is integrated as an addition to the MOPSA platform which already provides abstract interpretationbased analysis of C and Python programs.


Thursday 2 February 10:00:

Speaker: Uli Fahrenberg

Title: A Generic Approach to Quantitative Verification

This talk is concerned with quantitative verification, that is, the verification of quantitative properties of quantitative systems. These systems are found in numerous applications, and their quantitative verification is important, but also rather challenging. In particular, given that most systems found in applications are rather big, compositionality and incrementality of verification methods are essential. In order to ensure robustness of verification, we replace the Boolean yesno answers of standard verification with distances. Depending on the application context, many different types of distances are being employed in quantitative verification. Consequently, there is a need for a general theory of system distances which abstracts away from the concrete distances and develops quantitative verification at a level independent of the distance. It is our view that in a theory of quantitative verification, the quantitative aspects should be treated just as much as input to a verification problem as the qualitative aspects are. In this work we develop such a general theory of quantitative verification. We assume as input a distance between traces, or executions, and then employ the theory of games with quantitative objectives to define distances between quantitative systems. Different versions of the quantitative bisimulation game give rise to different types of distances, viz.~bisimulation distance, simulation distance, trace equivalence distance, etc., enabling us to construct a quantitative generalization of van Glabbeek’s lineartime–branchingtime spectrum. We also extend our general theory of quantitative verification to a theory of quantitative specifications. For this we use modal transition systems, and we develop the quantitative properties of the usual operators for behavioral specification theories.


Tuesday 13 December 10:00:

Speaker: Vijay Ganesh

Title: SAT Solver + Computer Algebra Attack on the Minimum KochenSpecker Problem (conjoint with LIP6)

One of the most fundamental results in the foundations of quantum mechanics is the Kochen–Specker (KS) theorem, a `nogo’ theorem which states that contextuality is an essential feature of any hiddenvariable theory. The theorem hinges on the existence of a mathematical object called a KS vector system. Although the existence of a KS vector system was first established by Kochen and Specker, the problem of the minimum size of such a system has stubbornly remained open for over 50 years. In this paper, we present a new method based on a combination of a SAT solver and a computer algebra system (CAS) to address this problem. We improve the lower bound on the minimum number of vectors in a KS system from 22 to 23 and improve the efficiency of the search by a factor of over 1000 when compared to the most recent computational methods. Finding a minimum KS system would simplify experimental tests of the KS theorem and have direct applications in quantum information processing, specifically in the security of quantum cryptographic protocols based on complementarity, zeroerror classical communication, and dimension witnessing.


Monday 21 November 11:00

Speaker: Souheib Baarir

Title: Contributions to Boolean satisfiability solving and its application to the analysis of discrete systems

Despite its NPCompleteness, propositional (Boolean) satisfiability (SAT) covers a broad spectrum of applications. Nowadays, it is an active research area finding its applications in many contexts: planning decision, cryptology, computational biology, hardware and software analysis, etc. Hence, the development of approaches that could handle increasingly challenging SAT problems has become a focus. During these last 8 years, SAT solving has been the main subject of my research work, and in this talk I will present some of the main results we obtained in the field.


Wednesday 26 October 15:00

Speaker: Gaëtan Staquet

Title: Learning Realtime OneCounter Automata

We present a new learning algorithm for realtime onecounter automata. Our algorithm uses membership and equivalence queries as in Angluin’s L* algorithm, as well as counter value queries and partial equivalence queries. In a partial equivalence query, we ask the teacher whether the language of a given finitestate automaton coincides with a counterbounded subset of the target language. We evaluate an implementation of our algorithm on a number of random benchmarks and on a use case regarding efficient JSONstream validation.

Recording: https://peertube.lre.epita.fr/w/toVh61JXaxNUdxBViUpRvD


Wednesday 26 October 13:30

Speaker: Guillermo Perez

Title: The Geometry of Reachability in Continuous Vector Addition Systems with States

We study the geometry of reachability sets of continuous vector addition systems with states (VASS). In particular we establish that they are almost Minkowski sums of convex cones and zonotopes generated by the vectors labelling the transitions of the VASS. We use the latter to prove that short socalled linear path schemes suffice as witnesses of reachability in continuous VASS of fixed dimension. Then, we give new polynomialtime algorithms for the reachability problem for linear path schemes. Finally, we also establish that enriching the model with zero tests makes the reachability problem intractable already for linear path schemes of dimension two.

Recording: https://peertube.lre.epita.fr/w/nQVdcT73vYzBfgQqZDwKJ4


Friday 14 October 14:00

Speaker: Sarah Berkemer

Title: Compositional properties of alignments

Alignments, i.e., positionwise comparisons of two or more strings or ordered lists are of utmost practical importance in computational biology and a host of other fields, including historical linguistics and emerging areas of research in the Digital Humanities. The problem is wellknown to be computationally hard as soon as the number of input strings is not bounded. Due to its practical importance, a huge number of heuristics have been devised, which have proved very successful in a wide range of applications. Alignments nevertheless have received hardly any attention as formal, mathematical structures. Here, we focus on the compositional aspects of alignments, which underlie most algorithmic approaches to computing alignments. We also show that the concepts naturally generalize to finite partially ordered sets and partial maps between them that in some sense preserve the partial orders. As a consequence of this discussion we observe that alignments of even more general structure, in particular graphs, are essentially characterized by the fact that the restriction of alignments to a row must coincide with the corresponding input graphs. Pairwise alignments of graphs are therefore determined completely by common induced subgraphs. In this setting alignments of alignments are welldefined, and alignments can be decomposed recursively into subalignments. This provides a general framework within which different classes of alignment algorithms can be explored for objects very different from sequences and other totally ordered data structures.


Friday 30 September 14:00

Speaker: Florian Renkin

Title: Transformations d’ωautomates pour la synthèse de systèmes réactifs

La synthèse vise à produire un système correct à partir de spécifications. Une approche pour résoudre ce problème consiste à traduire la spécification en un jeu de parité dont la stratégie gagnante encode le système. Dans cet exposé nous verrons deux méthodes permettant de produire des automates de parité. La première s’appuie sur l’amélioration et la combinaison de procédures nouvelles ou existantes. La seconde est un algorithme de Casares et al. apportant une garantie d’optimalité du résultat. Dans un deuxième temps, nous verrons comment nous réduisons le système obtenu. Deux types de réductions seront abordées. La première permet d’obtenir un résultat optimal mais pas la seconde qui privilégie le temps de traitement.


Friday 9 September 14:00

Speaker: Alexandre DuretLutz

Title: À l’arrache : Spot

Présentation informelle de Spot, bibliothèque C++ de manipulation d’ωautomates et de formules de logique temporelle linéaire, fournissant des bindings Python et plusieurs outils.
