Paris Automata and Concurrency Theory Seminar

29 January 2025

Venue: IRIF, Université Paris Cité

Speaker 1: (present) Laetitia Laversa, IRIF, Université Paris Cité, France

Title: TBA

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.

10 October 2024

Venue: LRE, EPITA Paris

Speaker 1: (present) Uli Fahrenberg, EPITA

Title: Introduction to Paris ACTS

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

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, Université Paris Cité, France

Title: Expressivity of First Order and Temporal Logics for Pomset Languages

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

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.