并发中的雕塑
摘要：高维自动机的直观雕塑过程。直观地说，如果高维自动机可以嵌入（即由）单个高维单元（超立方体）雕塑出来，那么它就是一个雕塑。本文的一个重要结果是，并非所有的高维自动机都可以被雕塑，其中几个自然无环的高维自动机可以作为例子，其中一个例子是著名的“破碎盒子”例子。此外，我们还展示了展开操作与雕塑完全无关，例如，有些雕塑的展开无法进行雕塑。我们通过将雕塑作为高维自动机的适当子类，并展示它们与规则ST结构（高维自动机的事件对应物）以及Pratt给出的3个（规则）Chu空间（在并发解释中）等价。我们认为我们的结果揭示了作为建模并发行为方法的雕塑背后的直觉，展示了其表达能力的准确范围。除了表达能力之外，我们还开发了一个算法来判断一个高维自动机是否可以进行雕塑。更重要的是，我们展示了雕塑与欧几里得立方体复合物等价（它是我们组合定义的几何对应物），其中包括用于死锁检测的流行的PV模型。这揭示了几何模型与组合模型之间的密切联系，这对于两个领域都可能有用。
作者：Uli Fahrenberg, Christian Johansen, Christopher A. Trotter, Krzysztof Ziemia''nski
论文ID：1812.02008
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22