Computer Science Seminar
Date: Friday, 09 February 2024
Time: 2:00 - 3:00 PM
Venue: Lecture Hall 5
Cascade Decomposition of Asynchronous Automata
Paul Gastin
LMF, CNRS & ENS Paris-Saclay.
09-02-24

---

Abstract

We propose a local, past-oriented fragment of propositional dynamic logic to reason about concurrent scenarios modelled as Mazurkiewicz traces, and prove it to be expressively complete with respect to regular trace languages.

Because of locality, specifications in this logic are efficiently translated into a cascade product of localized asynchronous automata, in a way that reflects the structure of formulas. An asynchronous automaton is local when only one process is acting non-trivially, all other processes have a single state. Hence, local asynchronous automata are in some sense the simplest ones wrt to the distributed system.

In particular, we obtain a new proof of Zielonka's fundamental theorem and a new implementation for the gossip problem as a cascade product of localized asynchronous automata.

The talk only assumes basic knowledge in ToC, mainly automata and logic. We first consider the sequential case. We revisit Krohn-Rhodes decomposition theorem in terms of cascade of relabelling transducers and sketch a proof for aperiodic languages based on Kamp’s theorem. Then, we introduce Mazurkiewicz traces and Zielonka asynchronous automata. Finally we present our local-past-PDL for traces.

Based on joint works with Bharat Adsul, Shantanu Kulkarni, Saptarshi Sarkar, and Pascal Weil. Papers: Concur’20, Concur’22, LMCS’22, and one submitted.