一句话：提出 Mazurkiewicz 迹上局部过去命题动态逻辑，证明其相对正则迹语言表达完备，并构造异步自动机级联积。
针对并发场景可建模为 Mazurkiewicz 迹，本文提出一种局部、面向过去的命题动态逻辑片段，并证明它相对于正则迹语言是表达完备的。由于公式具有局部性，可将逻辑规格按公式结构高效翻译为异步自动机。由此作者给出 Zielonka 基本定理的新证明，并证明任意正则迹语言都可由局部化异步自动机的级联积实现；这些局部化自动机基本只作用于单个进程。该结果改进了 Adsul 等人此前依赖更大过去命题动态逻辑片段和 gossip 自动机的工作，避免使用 gossip 自动机或 Zielonka 时间戳机制，并展示如何把 gossip 自动机实现为级联积。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{AdsulGKW24,
title = {An expressively complete local past propositional dynamic logic over Mazurkiewicz traces and its applications},
author = {Bharat Adsul and Paul Gastin and Shantanu Kulkarni and Pascal Weil},
booktitle = {LICS},
year = {2024},
doi = {10.1145/3661814.3662110}
}