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.