Paris Automata and Concurrency Theory Seminar

26 November 2024

Venue: LIX, École polytechnique

Speaker 1: Enzo Erlich, IRIF, Université Paris Cité, France

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

Speaker 2: 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.

10 October 2024

Venue: LRE, EPITA Paris

Speaker 1: 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: 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.