Paris ACTS has been created to reinforce the links between different research groups in the Paris area which are working on the connections between automata theory and concurrency theory, and in order to advance this research on a national and international level,
The seminar takes place for an afternoon every six-eight weeks, moving between LIX (École Polytechnique), LRE (EPITA Paris), and IRIF (Université Paris Cité). It is held in hybrid mode and is an evolution of the (i)Po(m)set Project Online Seminar (PPOS).
Paris ACTS is inspired by the MeFoSyLoMa seminar, with which it has a slight thematic overlap, but includes a hybrid component.
The program for each afternoon is roughly as follows:
| 14:00--14:45 | In-person talk |
| 14:45--15:30 | Virtual talk |
| 15:30--16:00 | Coffee break |
| 16:00--17:00 | Discussion |
Venue: LRE, EPITA Paris, salle KB404
Speaker 1: Uli Fahrenberg, LRE, EPITA
Title: Introduction
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: 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.