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.