AA/Seminar

From LRDE

Seminar "Automata and Applications"

The seminar of the research group 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 the organizer.

Upcoming Talks

  • Monday 21 November 11:00: Souheib Baarir: 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.
    • At KB in salle Apprentissage 2 and online at https://meet.lrde.epita.fr/seminar-aa-20221121

Previous Seminars

  • Wednesday 26 October 15:00: Gaëtan Staquet: 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: Guillermo Perez: 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: Sarah Berkemer: 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: Florian Renkin: 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: Alexandre Duret-Lutz: À 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.