Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913497667862528 |
|---|---|
| author | Adsul, Bharat Gastin, Paul Kulkarni, Shantanu Weil, Pascal |
| author_facet | Adsul, Bharat Gastin, Paul Kulkarni, Shantanu Weil, Pascal |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_11308 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages Adsul, Bharat Gastin, Paul Kulkarni, Shantanu Weil, Pascal Formal Languages and Automata Theory Logic in Computer Science 68Q10, 68Q45, 68Q70 F.1.1; F.4.1; F.4.3 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. |
| title | Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages |
| topic | Formal Languages and Automata Theory Logic in Computer Science 68Q10, 68Q45, 68Q70 F.1.1; F.4.1; F.4.3 |
| url | https://arxiv.org/abs/2405.11308 |