Past Seminars
10 October 2024
Venue: LRE, EPITA Paris
Speaker 1: (present) Uli Fahrenberg, LRE
Title: Introduction to Paris ACTS
► Abstract:
I will give an introduction to the purpose of the Paris ACTS seminar series and to the intersection between
automata and concurrency theory at which it is situated. I will finish by introducing a notion of specification theories that we developed some years
ago and which is related to the refinement calculus of the second speaker.
Speaker 2: (online) Ian Hayes, University of Queensland, Brisbane, Australia
Title: Concurrent Refinement Algebra
► Abstract:
Our goal is to develop a refinement calculus for shared-memory concurrent programs that
supports Jones-style rely/guarantee developments. Our semantics is based on Aczel traces,
which explicitly include environment transitions as well as program transitions, and were
originally proposed as a basis for showing the rely/guarantee rules of Jones are sound.
Our approach has been to develop a hierarchy of algebraic theories that provide a foundation
for concurrent program refinement. Our algebraic theory is based on a lattice of commands
that includes a sub-lattice of test commands (similar to Kozen's Kleene Algebra with Tests)
and a sub-algebra of atomic commands (similar to Milner's SCCS but with a richer structure
that supports Aczel's program and environment transitions). Rely and guarantee conditions
are encoded as commands within the theory, and refinement laws for deriving concurrent
programs from rely/guarantee specifications can be proven within the theory.
26 November 2024
Venue: LIX, École polytechnique
Speaker 1: (present) Enzo Erlich, IRIF
Title: Expressivity of First Order and Temporal Logics for Pomset Languages
► Abstract:
We introduce a temporal logic for pomset languages, which we call Sparse-based Pomset Temporal Logic (SPTL). SPTL draws significant inspiration from Linear Temporal Logic (LTL). We show that, under a reasonable hypothesis, SPTL is as expressive as a First Order (FO) logic for pomset languages that we introduce. This extends Kamp's theorem, which states that LTL has the same expressive power as FO logic over words. To do this, we apply Kamp's theorem to ST-sequences, which are representations of pomsets over words, and provide successive translations over different logics.
Speaker 2: (online) Masaki Waga, Kyoto University, Japan
Title: Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
► Abstract:
We present an algorithm to learn a deterministic timed automaton (DTA)
via membership and equivalence queries. Our algorithm is an extension of
the L* algorithm with a Myhill-Nerode style characterization of
recognizable timed languages, which is the class of timed languages
recognizable by DTAs. We first characterize the recognizable timed
languages with a Nerode-style congruence. Using it, we give an algorithm
with a smart teacher answering symbolic membership queries in addition
to membership and equivalence queries. With a symbolic membership query,
one can ask the membership of a certain set of timed words at one
time. We prove that for any recognizable timed language, our learning
algorithm returns a DTA recognizing it. We show how to answer a symbolic
membership query with finitely many membership queries. We also show
that our learning algorithm requires a polynomial number of queries with
a smart teacher and an exponential number of queries with a normal
teacher. We applied our algorithm to various benchmarks and confirmed
its effectiveness with a normal teacher.
29 January 2025
Venue: IRIF, Université Paris Cité
Speaker 1: (present) Laetitia Laversa, IRIF
Title: About the k-synchronizability of communicating automata
► Abstract:
Distributed systems are ubiquitous and their implementation is complex and error-prone. In order to check for errors, they can be modeled as systems of communicating automata, where each automaton represents the behavior of an element of the system. Verification problems such as reachability are undecidable in such a model. Indeed, a system of communicating automata is Turing-equivalent. For that, the use of approximations is necessary. k-synchronizability is one of these techniques. A system is k-synchronizable if, for all executions, there is an equivalent execution that can be divided into phases containing k messages. These phases are called k-exchanges. In this presentation, we will discuss the different results that make this class so interesting.
Speaker 2: (present) Glynn Winskel, Queen Mary University of London, UK
Title: From Concurrent Games to Gödel's Dialectica Interpretation
► Abstract:
Computation today is highly distributed and interactive. Event structures represent computation in terms of causal dependency and conflict relations on events; the relations make precise the sense in which events can occur concurrently (independently, in parallel). By redeveloping games in sufficient generality, as event structures, interactive computation becomes a strategy and its type a game. Then the dichotomy between a system and its environment is caught in the distinction between Player and Opponent moves. A functional approach has to handle the dichotomy much more ingeniously, through its blunter distinction between input and output. This has led to a variety of functional approaches, specialised to particular interactive demands. A surprise in the development of concurrent games has been that several, seemingly disparate, historical approaches in logic and computation reappear as special cases. They include stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation; lenses and optics; and their extensions to containers in dependent lenses and optics.
20 March 2025
Venue: LRE, EPITA Paris
Speaker 1: (present) Adrien Pommellet, LRE
Title: Active Learning Techniques for Pomset Recognizers
► Abstract:
Pomsets are a promising
formalism for concurrent programs based on partially
ordered sets. Among this class, series-parallel pomsets
admit a convenient linear representation and can be
recognized by simple algebraic structures known as
pomset recognizers. Active learning consists in
inferring a formal model of a recognizable language by
asking membership and equivalence queries to a minimally
adequate teacher (MAT). We improve existing learning
algorithms for pomset recognizers by (1) introducing a
new counter-example analysis procedure that is in the
best case scenario exponentially more efficient than
existing methods; (2) adapting the state-of-the-art
Lλ algorithm to minimize the impact of
exceedingly verbose counter-examples and remove
redundant queries; (3) designing a suitable finite test
suite that ensures equivalence between two pomset
recognizers provided their sizes are close enough by
extending the well-known W-method.
Speaker 2: (online) Rajeev Alur, University of Pennsylvania, US
Title: Automata over Series-Parallel Graphs
► Abstract:
Motivated by distributed data processing applications, we introduce a class of labeled directed acyclic graphs constructed using sequential and parallel composition operations, and study automata and logics over them. We show that deterministic and non-deterministic acceptors over such graphs have the same expressive power, which can be equivalently characterized by Monadic Second-Order logic and the graded μ-calculus. We establish closure under composition operations and decision procedures for membership, emptiness, and inclusion.
A key feature of our graphs, called synchronized series-parallel graphs (SSPG), is that parallel composition introduces a synchronization edge from the newly introduced source vertex to the sink. The transfer of information enabled by such edges is crucial to the determinization construction, which would not be possible for the traditional definition of series-parallel graphs. SSPGs allow both ordered ranked parallelism and unordered unranked parallelism. The latter feature means that in the corresponding automata, the transition function needs to account for an arbitrary number of predecessors by counting each type of state only up to a specified constant, thus leading to a notion of counting complexity that is distinct from the classical notion of state complexity. The determinization construction translates a nondeterministic automaton with n states and k counting complexity to a deterministic automaton with 2n2 states and kn counting complexity, and both these bounds are shown to be tight. Furthermore, for nondeterministic automata a bound of 2 on counting complexity suffices without loss of expressiveness.
14 May 2025: Joint session with GT DAAL
Venue: LIGM, Marne-la-Vallée
9:30 Barbara König (online): Graph Automata and Automaton Functors
Abstract:
We generalize Courcelle's recognizable graph languages and results on monadic second-order logic to more general structures.
We give a category-theoretical characterization of recognizability. A recognizable subset of arrows in a category is defined via a functor into the category of relations on finite sets. This can be seen as a straightforward generalization of finite automata and we show how to obtain graph automata - accepting recognizable graph languages - by applying the theory to the category of cospans of graphs.
We also introduce a simple logic that allows to quantify over the subobjects of a categorical object and we show that, for the category of graphs, this logic is equally expressive as monadic second-order graph logic (MSOGL). Furthermore, we explain that in the more general setting of hereditary pushout categories, a class of categories closely related to adhesive categories, we can recover Courcelle's result that every MSOGL-expressible property is recognizable.
The talk concludes by reviewing a practical implementation of graph automata with applications to the verification of graph transformation systems.
10:30 Break
11:00 Denis Kuperberg (present): Explorable Automata
Abstract:
We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs instead of just one.
We show that recognizing HD parity automata of fixed index among explorable ones is in PTIME, thereby giving a strong link between the two notions. We then show that recognizing explorable automata is EXPTIME-complete, in the case of finite words or parity automata up to index [0,2]. Additionally, we define the notion of ω-explorable automata on infinite words, where countably many runs can be used to resolve the non-deterministic choices. We show EXPTIME-completeness for ω-explorability of automata on infinite words for the safety and co-Büchi acceptance conditions.
We finally characterize the expressivity of (ω-)explorable automata with respect to the parity index hierarchy.
We leave open the decidability of explorability for [1,3]-automata and ω- explorability for Büchi automata, both equivalent to the general case of arbitrary acceptance conditions.
This is joint work with Emile Hazard and Olivier Idir (short version CSL 2023, long version submitted to LMCS).