Seminars of the Automata and applications group

The seminar of the research group AA|Automata and Applications is held every 2-3 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

Previous Talks

  • Thursday 24 October 2024, 15:00

    • Title: “Synchronous Product of Time Petri Nets and its Applications to Fault-Diagnosis”
    • Speaker: Eric Lubat
    • We study the behavior of Discrete Event Systems (DES) subject to strong temporal constraints. We are more particularly interested in the formal verification of properties on the timed languages associated with their executions. In this context, we focus on DESmodelled using Time Petri Nets (TPN), an extension of classicalPetri nets in which we can constrain the time during which transitions stay enabled.Our goal is to use and extend techniques borrowed from model-checking in order to check properties related to the diagnosability of a system. To this end, we study properties on the intersection of the timed languages of systems. Our approach is based on the definition of a new composition operator,that we call a synchronous product, that constrains different transitions to fire at the same time. This allows us to analyse the product of systems more directly, without the need to compute the intersection of their language at the level of their state spaces.Our main contribution is the definition of a new formal model, called Product TPN (PTPN), that includes our notion of synchronous product in its syntax. We show how to extend the notion ofState Class Graphs to PTPN and use this construction to check the diagnosability of single faults on TPN. We also study the diagnosability of more complex behaviors, expressed using patterns of events, and explore a restricted case of timed pattern. A software called TWINA was created in the context of this thesis. Twina is a tool for analyzing the “product” of two Time Petri Nets (TPN), with possibly inhibitor and read arcs. Its main objective is to compute a usable representation of the intersection of two net languages; meaning the intersection of the (timed) languages obtained from the executions of two TPN, in which transitions with the same labels are fired at the same date. The tool is based on a new extension of the State Class Graph construction, the method used in the TINA (TIme petri Net Analyzer) toolbox. Like for TINA, this tool is maintained by the Verification of Time Critical Systems (VERTICS) group, which develops new verification methods and tools for checking properties of critical systems having strong temporal and timing requirements. TWINA is mainly used to conduct experiments on our new model, the PTPN.

  • Wednesday 6 November, 14:00

    • Title: Closable and uniquely closable skeletons of untyped lambda terms, formally.
    • Speaker: Nicolas Magaud
    • In 2017, Olivier Bodini and Paul Tarau introduced closable and uniquely closable Motzkin trees as “skeletons” to describe the structure of closed untyped lambda terms. They defined efficient Prolog generators for these skeletons and studied their statistical properties. We present a formalization of these different notions in the Coq proof assistant, with formal proofs of equivalence between several definitions that underlie the generators designed by Bodini and Tarau. We also present random generators to be used with QuickChick, and extend the discourse to open λ-terms. To facilitate this work and generalize the approach, we propose generic tools to help setting up the correspondence between two isomorphic types more easily. We hope such a methodology could be reused to deal with other families of objects, having different and isomorphic representations.

  • Monday 26 February, 15:00 at EPITA KB 204 and online

    • Speaker: Jérémy Dubut-Kross, National Institute of Advanced Science and Technology, Tokyo

    • Title: Fixed-Point Theorems for Non-Transitive Relations

    • We develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden. Joint work with Akihisa Yamada.

  • Tuesday 10 October, 10:00am at EPITA KB and online

    • Speaker: Francesco Parolini

    • Title: Inclusion Testing of Büchi Automata Based on Well-Quasiorders

    • 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 Ramsey-based 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 well-quasiorders on finite words. We implemented BAInc in a tool called BAIT that we experimentally evaluated against the state-of-the-art. Our experimental results show that BAIT advances the state-of-the-art on an overwhelming majority of these benchmarks.

  • 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 non-terminating 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 finite-trace 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 tree-like 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 well-quasi-ordering 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 2-player zero-sum 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 almost-sure Büchi/co-Bü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/seminar-AA

  • Monday 20 February 14:00:

    • Speaker: Vincent Botbol

    • Title: Static analysis of Michelson smart-contracts using abstract interpretation

    • In this talk, we briefly introduce the Toss blockchain and Michelson, its statically typed stacked-based smart-contract language. Then, we present a static analysis for Michelson smart-contracts using abstract interpretation. Our tool automatically infers (numerical) invariants allowing us to verify numerical safety properties along with more blockchain-specific functional properties, e.g., validating user authentication patterns, analyzing the evolution of contract’s storage, determining an upper-bound gas usage of a smart-contract,… This ongoing work is integrated as an addition to the MOPSA platform which already provides abstract interpretation-based 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 yes-no 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 linear-time–branching-time 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 Kochen-Specker Problem (conjoint with LIP6)

    • One of the most fundamental results in the foundations of quantum mechanics is the Kochen–Specker (KS) theorem, a `no-go’ theorem which states that contextuality is an essential feature of any hidden-variable 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, zero-error 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 NP-Completeness, 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 One-Counter Automata

    • We present a new learning algorithm for realtime one-counter 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 finite-state automaton coincides with a counter-bounded 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 JSON-stream 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 so-called linear path schemes suffice as witnesses of reachability in continuous VASS of fixed dimension. Then, we give new polynomial-time 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., position-wise 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 well-known 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 well-defined, 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 Duret-Lutz

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