# Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages

arXiv: https://arxiv.org/abs/2405.11308 · HTML: https://mlsanity.com/paper/2405.11308/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 May 2024.

## Built on by (most cited first, 1 of 1)

- [Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows](https://mlsanity.com/paper/2605.20923/) (2026)

## Abstract (arXiv)

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.