Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages

TL;DR

This paper introduces a local, past-oriented fragment of propositional dynamic logic for reasoning about concurrent systems modeled as Mazurkiewicz traces, demonstrating its expressiveness and efficient automata translation, and providing new proofs and constructions for regular trace languages.

Contribution

It presents a new, localized fragment of propositional dynamic logic that is expressively complete for regular trace languages and offers a novel cascade automata decomposition approach.

Findings

Logic is efficiently translatable into asynchronous automata.

Provides a new proof of Zielonka's theorem.

Shows how to implement gossip automata as cascade products.

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 asynchronous automata, in a way that reflects the structure of formulas. In particular, we obtain a new proof of Zielonka's fundamental theorem and we prove that any regular trace language can be implemented by a cascade product of localized asynchronous automata, which essentially operate on a single process. These results refine earlier results by Adsul et al. which involved a larger fragment of past propositional dynamic logic and used Mukund and Sohoni's gossip automaton. Our new results avoid using this automaton, or Zielonka's timestamping mechanism and, in particular, they show how to implement a gossip automaton as a cascade product.