一句话：提出异步圈积与异步级联分解，将Krohn-Rhodes理论推广到Mazurkiewicz迹与异步自动机。
论文为以 Mazurkiewicz 迹语言和异步自动机建模的并发行为发展代数工具，反映事件的因果与并发。作者引入异步圈积运算及其原则，给出相应迹语言的刻画，并提出类似 Krohn-Rhodes 的分解结果，在无环架构下证明。随后定义局部级联积与全局级联序列：前者直接实现异步圈积，后者借助 gossip 自动机给出更复杂实现。应用上，一阶逻辑可定义的迹语言可由 gossip 自动机与 2 状态异步重置自动机的受限局部级联积接受，也可由 2 状态异步重置自动机的全局级联序列接受；在异步 Krohn-Rhodes 定理成立的字母表上，局部级联积已足够，并导出表达完备的简单时序逻辑。
We develop new algebraic tools to reason about concurrent behaviours modelled as languages of Mazurkiewicz traces and asynchronous automata. These tools reflect the distributed nature of traces and the underlying causality and concurrency between events, and can be said to support true concurrency. They generalize the tools that have been so efficient in understanding, classifying and reasoning about word languages. In particular, we introduce an asynchronous version of the wreath product operation and we describe the trace languages recognized by such products (the so-called asynchronous wreath product principle). We then propose a decomposition result for recognizable trace languages, analogous to the Krohn-Rhodes theorem, and we prove this decomposition result in the special case of acyclic architectures. Finally, we introduce and analyze two distributed automata-theoretic operations. One, the local cascade product, is a direct implementation of the asynchronous wreath product operation. The other, global cascade sequences, although conceptually and operationally similar to the local cascade product, translates to a more complex asynchronous implementation which uses the gossip automaton of Mukund and Sohoni. This leads to interesting applications to the characterization of trace languages definable in first-order logic: they are accepted by a restricted local cascade product of the gossip automaton and 2-state asynchronous reset automata, and also by a global cascade sequence of 2-state asynchronous reset automata. Over distributed alphabets for which the asynchronous Krohn-Rhodes theorem holds, a local cascade product of such automata is sufficient and this, in turn, leads to the identification of a simple temporal logic which is expressively complete for such alphabets.
@article{paperbot1688,
title = {Asynchronous wreath product and cascade decompositions for concurrent behaviours},
author = {Bharat Adsul and Paul Gastin and Saptarshi Sarkar and Pascal Weil},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:22)2022}
}