一句话：形式化 Pratt 的高维自动机雕塑过程，刻画可雕塑 HDA 的表示能力并给出判定算法。
本文形式化 Pratt 关于高维自动机（HDA）的雕塑过程：若 HDA 能嵌入单个超立方体，则称其为雕塑。作者证明并非所有 HDA 可雕塑，给出若干自然无环反例，包括 van Glabbeek 的“破箱”；并发现展开与可雕塑性无关。为刻画表达力，他们证明雕塑这一 HDA 真子类等价于正则 ST 结构和 3 上正则 Chu 空间，也等价于欧几里得立方复形，涵盖用于死锁检测的 PV 模型。文末给出判定 HDA 是否可雕塑的算法，从而连接并发的几何模型与组合模型。
We give a formalization of Pratt's intuitive sculpting process for higher-dimensional automata (HDA). Intuitively, an HDA is a sculpture if it can be embedded in (i.e., sculpted from) a single higher dimensional cell (hypercube). A first important result of this paper is that not all HDA can be sculpted, exemplified through several natural acyclic HDA, one being the famous "broken box" example of van Glabbeek. Moreover, we show that even the natural operation of unfolding is completely unrelated to sculpting, e.g., there are sculptures whose unfoldings cannot be sculpted. We investigate the expressiveness of sculptures, as a proper subclass of HDA, by showing them to be equivalent to regular ST-structures (an event-based counterpart of HDA) and to (regular) Chu spaces over 3 (in their concurrent interpretation given by Pratt). We believe that our results shed new light on the intuitions behind sculpting as a method of modeling concurrent behavior, showing the precise reaches of its expressiveness. Besides expressiveness, we also develop an algorithm to decide whether an HDA can be sculpted. More importantly, we show that sculptures are equivalent to Euclidean cubical complexes (being the geometrical counterpart of our combinatorial definition), which include the popular PV models used for deadlock detection. This exposes a close connection between geometric and combinatorial models for concurrency which may be of use for both areas.
@article{paperbot1323,
title = {Sculptures in Concurrency},
author = {Uli Fahrenberg and Christian Johansen and Christopher A. Trotter and Krzysztof Ziemiański},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 2},
year = {2021},
doi = {10.23638/lmcs-17(2:5)2021}
}