Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages
<|reference_start|>Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages: 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.<|reference_end|>
@article{adsul2024propositional,
    title={Propositional dynamic logic and asynchronous cascade decompositions for
  regular trace languages},
    author={Bharat Adsul, Paul Gastin, Shantanu Kulkarni, Pascal Weil},
    journal={In LICS'24: Proceedings of the 39th Annual ACM/IEEE Symposium on
  Logic in Computer Science, ACM, 2024, Article No.: 2, Pages 1-13},
    year={2024},
    doi={10.1145/3661814.3662110},
    archivePrefix={arXiv},
    eprint={2405.11308},
    primaryClass={cs.FL cs.LO}
}