摘要：We give a formalization of Pratt's intuitive sculpting process forhigher-dimensional automata (HDA). Intuitively, an HDA is a sculpture if it canbe 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 besculpted, exemplified through several natural acyclic HDA, one being the famous"broken box" example of van Glabbeek. Moreover, we show that even the naturaloperation of unfolding is completely unrelated to sculpting, e.g., there aresculptures whose unfoldings cannot be sculpted. We investigate theexpressiveness of sculptures, as a proper subclass of HDA, by showing them tobe equivalent to regular ST-structures (an event-based counterpart of HDA) andto (regular) Chu spaces over 3 (in their concurrent interpretation given byPratt). We believe that our results shed new light on the intuitions behindsculpting as a method of modeling concurrent behavior, showing the precisereaches of its expressiveness. Besides expressiveness, we also develop analgorithm to decide whether an HDA can be sculpted. More importantly, we showthat sculptures are equivalent to Euclidean cubical complexes (being thegeometrical counterpart of our combinatorial definition), which include thepopular PV models used for deadlock detection. This exposes a close connectionbetween geometric and combinatorial models for concurrency which may be of usefor both areas.
