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.

翻译：我们提出一种面向局部、基于过去时的命题动态逻辑片段，用于推理建模为Mazurkiewicz迹的并发场景，并证明其在正则迹语言上具有表达完备性。由于局部性，该逻辑中的规范可高效转化为异步自动机，且转化方式反映公式结构。特别地，我们得到Zielonka基本定理的新证明，并证明任何正则迹语言均可由局部化异步自动机的级联积实现——这些自动机本质上仅在单一进程上运行。这些结果改进了Adsul等人此前的研究，其工作涉及更大范围过去时命题动态逻辑片段，并使用了Mukund与Sohoni的闲聊自动机。我们的新结果无需使用该自动机或Zielonka时间戳机制，并特别展示了如何将闲聊自动机实现为级联积。