Sculptures in Concurrency

TL;DR

This paper formalizes the concept of sculpting in higher-dimensional automata, explores its limitations and expressiveness, and establishes connections with geometric models, providing a new perspective on modeling concurrent systems.

Contribution

It introduces a formal definition of sculpting for HDA, analyzes its expressiveness, and links it to Euclidean cubical complexes and PV models, with an algorithm for sculptability decision.

Findings

Not all HDA can be sculpted, including the 'broken box' example.

Sculptures are equivalent to regular ST-structures and Chu spaces over 3.

Sculptures correspond to Euclidean cubical complexes, including PV models.

Abstract

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.

Equations

$${\alpha }_{k,n-1}{\beta }_{\ell ,n}={\beta }_{\ell -1,n-1}{\alpha }_{k,n}(k<\ell )$$

$$q_{n-1}\stackrel{s_i}{\to }{q}_n\text{ with }{s}_i(q_n)=q_{n-1}\text{ or }{q}_n\stackrel{t_i}{\to }{q}_{n-1}\text{ with }{t}_i(q_n)=q_{n-1}.$$

$$Q\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\{(\lambda (s_2(q)),\lambda (s_1(q)))\mid q\in Q_2\}.$$

$${\lambda }_i(q)=\lambda (s_1(s_2(\dots (s_{i-1}(s_{i+1}(\dots (s_n(q))\dots )).$$

$$\lambda ({\alpha }_i(q))=({\lambda }_1(q),\dots ,{\lambda }_{i-1}(q),{\lambda }_{i+1}(q),\dots ,{\lambda }_n(q)).$$

$$\begin{gathered} {\lambda }_i({\alpha }_j(q))=\lambda (s_1{s}_2\dots s_{i-1}{s}_{i+1}\dots s_{n-2}{s}_{n-1}{\alpha }_j(q))=\lambda (s_1{s}_2\dots s_{i-1}{s}_{i+1}\dots s_{n-2}{\alpha }_j{s}_n(q)) \\ =\lambda (s_1{s}_2\dots s_{i-1}{s}_{i+1}\dots {\alpha }_j{s}_{n-1}{s}_n(q))=\cdots =\lambda (s_1{s}_2\dots s_{i-1}{s}_{i+1}\dots s_{j-1}{\alpha }_j{s}_{j+1}\dots s_{n-1}{s}_n(q)) \\ =\lambda (s_1{s}_2\dots s_{i-1}{s}_{i+1}\dots s_{j-1}{s}_j{s}_{j+1}\dots s_{n-1}{s}_n(q))={\lambda }_i(q) \end{gathered}$$

$$\begin{gathered} {\lambda }_i({\alpha }_j(q))=\lambda (s_1{s}_2\dots s_{i-1}{s}_{i+1}\dots s_{n-2}{s}_{n-1}{\alpha }_j(q))=\cdots =\lambda (s_1{s}_2\dots s_{i-1}{\alpha }_j{s}_{i+2}\dots s_{n-1}{s}_n(q)) \\ =\lambda (s_1{s}_2\dots {\alpha }_j{s}_i{s}_{i+2}\dots s_{n-1}{s}_n(q))=\cdots =\lambda (s_1{s}_2\dots s_{j-1}{\alpha }_j{s}_{j+1}\dots s_i{s}_{i+2}\dots s_{n-1}{s}_n(q)) \\ =\lambda (s_1{s}_2\dots s_i{s}_{i+2}\dots s_{n-1}{s}_n(q))={\lambda }_{i+1}(q). \end{gathered}$$

$${\lambda }_1(q)=\lambda (s_2(q))=\lambda (s_1(q))={\lambda }_2(q).$$

$$\begin{gathered} \lambda (s_2(s_1\dots s_{i-1}{s}_{i+1}\dots s_{j-1}{s}_{j+1}\dots s_n(q)))=\lambda (s_1\dots s_{j-1}{s}_{j+1}\dots s_n(q))={\lambda }_j(q) \\ ={\lambda }_i(q)=\lambda (s_1\dots s_{i-1}{s}_{i+1}\dots s_n(q))=\lambda (s_1(s_1\dots s_{i-1}{s}_{i+1}\dots s_{j-1}{s}_{j+1}\dots s_n(q))). \end{gathered}$$

$$\pi \stackrel{△}{=}(S,T)\stackrel{e}{\to }(S^{\prime },T^{\prime })\stackrel{e^{\prime }}{\to }(S^{\prime \prime },T^{\prime \prime })\dots$$

$$\mathbf{B}^{d}_{n}=\big{\{}(x_{1},\dotsc,x_{d})\in\{0,\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}},1\}^{d}\mathrel{\big{|}}|\{i\mid x_{i}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\}|=n\big{\}}$$

$$x_i=\{\begin{array}{ll}0& \text{if }i\notin S,\\ \text{leavevmode}to7.29pt\text{vbox}to4.71pt\text{pgfpicture}\text{makeatletter}\text{lower}-0.2ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt0.0pt\text{pgfsys@lineto}3.44443pt0.0pt\text{pgfsys@lineto}3.44443pt4.30554pt\text{pgfsys@lineto}6.88885pt4.30554pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}& \text{if }i\in S\setminus T,\\ 1& \text{if }i\in T,\end{array}$$

$$u_i=\{\begin{array}{ll}{t}_j& \text{if }i=b(j),\\ 0& \text{if }i\notin \mathrm{im}(b).\end{array}$$

$$(t_1,\dots ,t_{j-1},\text{leavevmode}to7.29pt\text{vbox}to4.71pt\text{pgfpicture}\text{makeatletter}\text{lower}-0.2ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt0.0pt\text{pgfsys@lineto}3.44443pt0.0pt\text{pgfsys@lineto}3.44443pt4.30554pt\text{pgfsys@lineto}6.88885pt4.30554pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture},t_{j+1},\dots ,t_d)$$

$$Q\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$UE(Q)\stackrel{UE(\text{em})}{\to }UE({\mathbf{B}}^d)\simeq \{1<2<\cdots <d\}.$$

$$\text{@ensuremath}\mathsf{H}({\mathsf{ST}}_1)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$v_0\stackrel{s}{\to }{e}_1\stackrel{t}{\to }{v}_1\stackrel{s}{\to }{e}_2\stackrel{t}{\to }{v}_2\stackrel{s}{\to }\cdots \stackrel{s}{\to }{e}_n\stackrel{t}{\to }{v}_n$$

$${\mathsf{ST}}_{\pi }(Q)=\bigcup _{\pi \in \mathrm{Path}(Q{)}_{\ast }}{\mathsf{ST}}_{\pi }(\pi )$$

$$S_{\pi }=T_{\pi }=\{\lambda (e_1),\dots ,\lambda (e_n)\}.$$

$$\pi =\sigma \stackrel{{\alpha }_i}{\to }q\stackrel{{\beta }_j}{\to }r,\varrho =\sigma \stackrel{{\beta }_k}{\to }{q}^{\prime }\stackrel{{\alpha }_l}{\to }r,$$

$$S_{\pi }$$

$$S_{\varrho }$$

$$S_{\pi }$$

$$T_{\pi }$$

$$s_i(s_j(r))\stackrel{s_i}{\to }{s}_j(r)\stackrel{s_j}{\to }r\stackrel{t_l}{\to }{t}_l(r).$$

$$T_{\pi }=T_{{\pi }^{\prime }}\cup \{{\lambda }_i(q)\}\stackrel{L.\text{ref}lem:HomotopicPaths}{=}{T}_{{\varrho }^{\prime }}\cup \{{\lambda }_i(q)\}=T_{{\varrho }^{\prime \prime }}\cup \{{\lambda }_i(q)\}\stackrel{ind}{\subseteq }{S}_{{\varrho }^{\prime \prime }}\cup \{{\lambda }_i(q)\}=S_{{\varrho }^{\prime }}=S_{\pi }.$$

$$S_{\pi }\stackrel{def}{=}{S}_{{\pi }^{\prime }}\stackrel{ind}{=}{T}_{{\pi }^{\prime }}\cup \{\lambda (en({\pi }^{\prime }))\}\stackrel{def}{=}{T}_{\pi }.$$

$$\lambda (s_1\dots s_{i-1}{s}_{i+1}\dots s_n(q))={\lambda }_i(q)$$

$$e={\lambda }_i(q)\in \lambda (q)=S_{\pi }\setminus T_{\pi },$$

Full text

1. Introduction

In approaches to non-interleaving concurrency, more than one event may happen simultaneously. There is a plethora of formalisms for modeling and analyzing such concurrent systems, e.g. Petri nets [Pet62], event structures [NPW81], configuration structures [vGP09, vGP95], or more recent variations such as dynamic event structures [AKPN15] or ST-structures [Joh16, Pri12]. They all share the idea of differentiating between concurrent and interleaving executions; i.e., in CCS notation [Mil89], $a\,|\,b$ is not the same as $a.b+b.a$.

In [vG06a], van Glabbeek shows that (up to history-preserving bisimilarity) higher-dimensional automata (HDA), introduced by Pratt and van Glabbeek in [Pra91, vG91], encompass all other commonly used models for concurrency. However, their generality make HDA quite difficult to work with, and so the quest for useful and general models for concurrency continues.

In [Pra00], Pratt introduces sculpting as a process to manage the complexity of HDA. Intuitively, sculpting takes one single hypercube, having enough concurrency (i.e., enough events), and removes cells until the desired concurrent behavior is obtained. This is orthogonal to composition, where a system is built by putting together smaller systems, which in HDA is done by gluing cubes. Pratt finishes the introduction of [Pra00] saying that “sculpture on its own suffices […] for the abstract modeling of concurrent behavior.”

In this paper we make precise the intuition of Pratt [Pra00] and give a definition of sculptures. We show that there is a close correspondence between sculptures, Chu spaces over $\boldsymbol{3}$ [Pra95], and ST-structures. We develop an algorithm to decide whether an HDA can be sculpted and show in Theorem 32 several natural examples of acyclic HDA that cannot be sculpted. We will carefully introduce these concepts later, but spend some time here to motivate our developments.

Combinatorial sculpting as described above is not to be confused with geometric sculpting, which consists of taking a geometric cube of some dimension and chiseling away hypercubes which one does not want to be part of the structure. Figure 1 shows a geometric sculpture; for a combinatorial sculpture see Figure 2.

Geometric sculpting has been used by Fajstrup et al. in [FRG06, FGR98] and other papers to model and analyze so-called PV programs: processes which interact by locking and releasing shared resources. In the simplest case of linear processes without choice or iteration this defines a hypercube with forbidden hyperrectangles, which cannot be accessed due to resources’ access limits. See Figure 3 for an example.

Technically, geometric sculptures are Euclidean cubical complexes; rewriting a proof in [Zie18] we show that such complexes are precisely (combinatorial) sculptures. In other words, an HDA is Euclidean iff it can be sculpted, so that the geometric models for concurrency [FRG06, FGR98] are closely related to the combinatorial ones [Pra91, vG91], through the notion of sculptures. Much work has been done in the geometric analysis of Euclidean HDA [FRGH04, GH07, FGR98, MR17, RZ14, Zie18]; through our equivalences these results are made available for the combinatorial models.

The notion of unfolding is commonly used to turn a complicated model into a simpler, but potentially infinite one. It may thus be expected that even if an HDA cannot be sculpted, then at least its unfolding can, as illustrated by the two examples in Figure 4.

However, this is not always the case, as witnessed by the example in Figure 5 which shows an HDA which cannot be sculpted and which is its own unfolding. This concurrent system, introduced in [Joh16], cannot be modeled as an ST-structure, but can be modeled as an ST-structure with cancellation [Joh16, Sec. 5].

Even more concerning is the fact that there are HDA which can be sculpted, but their unfoldings cannot; in fact, Figure 2 exposes one such example. This shows that for HDA, unfolding does not always return a simpler model.

In the geometric setting, this means that there are Euclidean cubical complexes whose unfoldings are not Euclidean. Since Goubault and Jensen’s seminal paper [GJ92], directed topology has been developed in order to analyze concurrent systems as geometric objects [Gra09, FRG06, FGH*+*16]. Directed topology has been developed largely in analogy to algebraic topology, but the analogy sometimes breaks. The mismatch we discover here, between Euclidean complexes and unfoldings, shows such a broken analogy. Unfoldings of HDA are directed analogues of universal covering spaces in algebraic topology [vG91, Fah05a, Fah05b]. There are several other problems with this notion, and finding better definitions of directed coverings is active ongoing research [Dub19, FL15].

Another motivation for Pratt’s [Pra00] is that HDA have no explicit notion of events. From the work in [Joh16] on ST-structures, introduced as event-based counterparts of HDA, we know that it is not always possible to identify the events in an HDA. The example in Figure 6 shows the (strong) asymmetric conflict from [vGP09, Pra03, Joh16], with two events $a$, $b$ such that occurrence of $a$ disables $b$. This can be modeled as a general event structure, but not as a pure event structure, hence also not as a configuration structure [vGP09]. It can also be modeled as an ST-structure, but when using HDA, one faces the problem that HDA transition labels do not carry events. The right part of Figure 6 shows two different ways of sculpting the corresponding structure from an HDA, one in which the two $a$-labeled transitions denote the same event and one in which they do not; a priori there is no way to tell which HDA is the “right” model. This also shows that the same HDA may be sculpted in several different ways.

Structure of the paper

We start in Section 2 by recalling the definitions of HDA, ST-structures, and Chu spaces. In Section 3 we introduce sculptures and show that they are isomorphic to regular ST-structures. The triple equivalence

[TABLE]

embodies Pratt’s event-state duality [Pra92]. Regularity is a geometric closure condition introduced for ST-structures in [Joh16] which ensures that for any ST-configuration, also all its faces are part of the structure, and they are all distinct. If regularity is dropped, then one has to pass to partial HDA [FL15] on the geometric side, and then the above equivalence becomes one between ST-structures and sculptures from partial HDA. For clarity of exposition we do not pursue this here, but also in that case, there will be acyclic partial HDA which cannot be sculpted.

Section 4 contains our main contribution, an algorithm to decide whether a given HDA $Q$ can be sculpted. The algorithm essentially works by covering $Q$ with the ST-structure $\mathsf{ST}_{\pi}(Q)$ which is built out of all paths in $Q$, and then trying to find a quotient of $\mathsf{ST}_{\pi}(Q)$ which is isomorphic to $Q$. We show that such a quotient exists iff $Q$ can be sculpted.

Figure 7 shows a simple example: the empty square, a one-dimensional HDA with two interleaving transitions. The covering $\mathsf{ST}_{\pi}(H)$ splits the upper-right corner, and the algorithm finds an equivalence on the four events which recovers (an ST-structure isomorphic to) $H$: in this case we equate $q_{1}\sim q_{3}$ and $q_{2}\sim q_{4}$, which corresponds to the standard way of identifying events in HDA as opposite sides of a filled-in square when it exists.

Another example is shown in Figure 8. This one-dimensional acyclic HDA cannot be sculpted, and the algorithm detects this by noting that (1) all the $a$-labeled transitions indeed need to be the same event, but then (2) the two states connected with a dashed line need to be identified, so that the ST-structure covering cannot be isomorphic to the original HDA model.

In Section 5 we make the connection between the combinatorial and geometric models and show that HDA can be sculpted precisely if they are Euclidean. This necessitates a few notions from directed topology which can be found in appendix.

Figure 9 sums up the relations between the different models which we expose in this paper. (The dashed line indicates the common belief that Chu spaces over $\boldsymbol{3}$ and acyclic HDA are equivalent, which we prove not to be the case.)

2. HDA, ST-Structures, and Chu Spaces

HDA are automata in which independence of events is indicated by higher-dimensional structure. HDA consist of states, transitions, and cubes of different dimensions which represent events running concurrently.

Precubical sets

A precubical set is a graded set $Q=\bigcup_{n\in\mathbbm{N}}Q_{n}$, with $Q_{n}\cap Q_{m}=\emptyset$ for all $n\neq m$, together with mappings $s_{k,n},t_{k,n}:Q_{n}\to Q_{n-1}$, $k=1,\dots,n$, satisfying the following precubical identities, for $\alpha,\beta\in\{s,t\}$,

[TABLE]

Elements of $Q_{n}$ are called $n$-cells (or simply cells), and for $q\in Q_{n}$, $n=\dim q$ is its dimension. The mappings $s_{k,n}$ and $t_{k,n}$ are called face maps, and we will usually omit the extra subscript $n$ and simply write $s_{k}$ and $t_{k}$. Intuitively, each $n$-cell $q\in Q_{n}$ has $n$ lower faces $s_{1}q,\dotsc,s_{n}q$ and $n$ upper faces $t_{1}q,\dotsc,t_{n}q$, whereas the precubical identity expresses the fact that $(n-1)$-faces of an $n$-cell meet in common $(n-2)$-faces; see Figure 10 for an example.

Morphisms $f:Q\to R$ of precubical sets are graded functions $f=\{f_{n}:Q_{n}\to R_{n}\}_{n\in\mathbbm{N}}$ which commute with the face maps: $\alpha_{k}\circ f_{n}=f_{n-1}\circ\alpha_{k}$ for all $n\in\mathbbm{N}$, $k\in\{1,\dots,n\}$, and $\alpha\in\{s,t\}$. This defines a category $\mathbb{pCub}$ of precubical sets. A precubical morphism is an embedding if it is injective; in that case we write $f:Q\hookrightarrow R$. $Q$ and $R$ are isomorphic, denoted $Q\cong R$, if there is a bijective morphism $Q\to R$.

If two cells $q,q^{\prime}\in Q$ are in a face relation $q=\alpha^{1}_{i_{1}}\dotsm\alpha^{n}_{i_{n}}q^{\prime}$, for $\alpha^{1},\dotsc,\alpha^{n}\in\{s,t\}$, then this sequence can be rewritten in a unique way, using the precubical identities (1), so that the indices $i_{1}<\dotsm<i_{n}$, see [GM03]. $Q$ is said to be non-selflinked if up to this rewriting, there is at most one face relation between any of its cells, that is, it holds for all $q,q^{\prime}\in Q$ that there exists at most one index sequence $i_{1}<\dotsc<i_{n}$ such that $q=\alpha^{1}_{i_{1}}\dotsm\alpha^{n}_{i_{n}}q^{\prime}$ for $\alpha^{1},\dotsc,\alpha^{n}\in\{s,t\}$.

In other words, $Q$ is non-selflinked iff any $q\in Q$ is embedded in $Q$, hence iff all $q$’s iterated faces are genuinely different. This conveys a geometric intuition of regularity and is frequently assumed [Faj05, FRG06], also in algebraic topology [Bre93, Def. IV.21.1]. It means that for all cells in $Q$, each of their faces (and faces of faces etc.) are present in $Q$ as distinct cells.

Higher-dimensional automata

A precubical set $Q$ is finite if $Q$ is finite as a set. This means that $Q_{n}$ is finite for each $n\in\mathbbm{N}$ and that $Q$ is finite-dimensional: there exists $N\in\mathbbm{N}$ such that $Q_{n}=\emptyset$ for all $n>N$ (equivalently, $\dim q\leq N$ for all $q\in Q$). In that case, the smallest such $N$ is called the dimension of $Q$ and denoted $\dim Q=\max\{\dim q\mid q\in Q\}$. A higher-dimensional automaton (HDA) is a finite precubical set $Q$ with a designated initial cell $I\in Q_{0}$. Morphisms $f:Q\to Q^{\prime}$ of HDA are precubical morphisms that fix the initial cell, i.e., have $f(I)=I^{\prime}$. We often call cells from $Q_{0}$ and $Q_{1}$ respectively states and transitions.

Note that we only deal with unlabeled HDA here, i.e., HDA without labellings on transitions and/or higher cells. We are interested here in the events, not in their labeling.

A step in an HDA, with $q_{n}\in Q_{n}$, $q_{n-1}\in Q_{n-1}$, and $1\leq i\leq n$, is either

[TABLE]

A path $\pi\overset{\scriptscriptstyle\triangle}{=}q^{0}\xrightarrow{\alpha^{1}}q^{1}\xrightarrow{\alpha^{2}}q^{2}\xrightarrow{\alpha^{3}}\dots$ is a sequence of steps $q^{j-1}\xrightarrow{\alpha^{j}}q^{j}$, with $\alpha^{j}\in\{s,t\}$. The first cell is denoted $\mathit{st}(\pi)$ and the ending cell in a finite path is $\mathit{en}(\pi)$. The string $\alpha^{1}\dots\alpha^{n}$ consisting of letters $s$, $t$ is the type of the path $\pi$.

Two paths are elementary homotopic [vG06a], denoted $\pi\!\stackrel{{\scriptstyle\textup{hom}}}{{\longleftrightarrow}}\!\pi^{\prime}$, if one can be obtained from the other by replacing, for $q\in Q$ and $i<j$, either (1) a segment $\xrightarrow{s_{i}}q\xrightarrow{s_{j}}$ by $\xrightarrow{s_{j-1}}q^{\prime}\xrightarrow{s_{i}}$, (2) a segment $\xrightarrow{t_{j}}q\xrightarrow{t_{i}}$ by $\xrightarrow{t_{i}}q^{\prime}\xrightarrow{t_{j-1}}$, (3) a segment $\xrightarrow{s_{i}}q\xrightarrow{t_{j}}$ by $\xrightarrow{t_{j-1}}q^{\prime}\xrightarrow{s_{i}}$, or (4) a segment $\xrightarrow{s_{j}}q\xrightarrow{t_{i}}$ by $\xrightarrow{t_{i}}q^{\prime}\xrightarrow{s_{j-1}}$. Homotopy is the reflexive and transitive closure of the above and is denoted the same. Two homotopic paths thus share their respective start and end cells.

A cell $q^{\prime}$ in an HDA $Q$ is reachable from another cell $q$ if there exists a path $\pi$ with $\mathit{st}(\pi)=q$ and $\mathit{en}(\pi)=q^{\prime}$. $Q$ is said to be connected if any cell is reachable from the initial state $I$. $Q$ is acyclic if there are no two different cells $q,q^{\prime}$ in $Q$ such that $q^{\prime}$ is reachable from $q$ and $q$ is reachable from $q^{\prime}$.

If an HDA is not connected, then it contains cells which are not reachable during any computation. We will hence assume all HDA to be connected.

Universal event labeling

Let $Q$ be a precubical set and define $\overset{\textsf{ev}}{\sim}$ to be the equivalence relation on $Q_{1}$ spanned by $\{(s_{i}q,t_{i}q)\mid q\in Q_{2},i\in\{1,2\}\}$. Let $\mathit{UE}(Q)={Q_{1}}_{\!/\mathord{\mathord{\overset{\textsf{ev}}{\sim}}}}$ be the set of equivalence classes; this is called the set of universal labels of $Q$. The universal label of a transition $q_{1}$ will be denoted by $\lambda(q_{1})$.

For every precubical morphism $f:Q\to R$ and transitions $e,e^{\prime}\in Q_{1}$, $e\overset{\textsf{ev}}{\sim}e^{\prime}$ implies $f(e)\overset{\textsf{ev}}{\sim}f(e^{\prime})$. As a consequence, $f$ induces a map between the sets of universal labels fitting into the diagram:

[TABLE]

This makes $\mathit{UE}$ a functor from the category of precubical sets $\mathbb{pCub}$ into the category of sets.

$Q$ is said to be inherently self-concurrent if there is $q\in Q_{2}$ for which $s_{1}q\overset{\textsf{ev}}{\sim}s_{2}q$ or (equivalently) $t_{1}q\overset{\textsf{ev}}{\sim}t_{2}q$. In that case, $\mathit{UE}(Q)$ does not identify events, as there are cells in which more than one occurrence of an event is active. We say that $Q$ is consistent if it is not inherently self-concurrent.

{exa}

The examples (1) and (2) are not consistent, though the first one is selflinked, whereas the second one is non-selflinked. Example (3) is consistent and selflinked.

1. (1)

Consider the HDA with three cells $\{Q_{0}=\{q_{0}\},Q_{1}=\{q_{1}\},Q_{2}=\{q_{2}\}\}$ where all the four maps of the square point to the same transition $\alpha_{i}(q_{2})=q_{1}$, for $\alpha\in\{s,t\}$ and $i\in\{1,2\}$ and the two maps of the transition point to the same state $\alpha_{1}(q_{1})=q_{0}$, which is also the initial state. For visual help we draw states as circles, transitions as squares, and 2-cells as hexagons.

2. (2)

Consider the HDA formed of three squares $q_{2},q^{\prime}_{2},q^{\prime\prime}_{2}\in Q_{2}$ that are adjacent, i.e., $t_{1}(q_{2})=s_{1}(q^{\prime}_{2})$ and $t_{1}(q^{\prime}_{2})=s_{1}(q^{\prime\prime}_{2})$, but the first square shares with the third one a transition, namely $s_{1}(q_{2})=s_{2}(q^{\prime\prime}_{2})=e$.

3. (3)

Consider the HDA formed of a single 2-cell $q_{2}$ having two of its vertices identified, i.e., $t_{1}(s_{1}(q_{2}))=v=t_{1}(s_{2}(q_{2}))$.

Let ${\mathrel{\overset{\mathsf{ev}}{<}}}\subseteq\mathit{UE}(Q)\times\mathit{UE}(Q)$ be the transitive closure of the relation

[TABLE]

We say that $Q$ is ordered if for every $a,b\in\mathit{UE}(Q)$ the conditions $a\mathrel{\overset{\mathsf{ev}}{<}}b$ and $b\mathrel{\overset{\mathsf{ev}}{<}}a$ cannot hold simultaneously or, equivalently, $\mathrel{\overset{\mathsf{ev}}{<}}$ is antisymmetric and $a\not\mathrel{\overset{\mathsf{ev}}{<}}a$ for all $a\in\mathit{UE}(Q)$. For a precubical morphism $f:Q\to R$, the induced map $\mathit{UE}(f):\mathit{UE}(Q)\to\mathit{UE}(R)$ preserves the relation $\mathrel{\overset{\mathsf{ev}}{<}}$. This makes $\mathit{UE}$ a functor into the category of sets with a transitive relation and relation-preserving maps.

If $Q$ is not consistent, then it is not ordered. Indeed, if $a=\lambda(s_{1}(q))=\lambda(s_{2}(q))$ for some $q\in Q_{2}$, then $a\mathrel{\overset{\mathsf{ev}}{<}}a$, which excludes ordered.

For every square $q$ we can assign a pair of universal labels $(\lambda(\alpha_{2}(q)),\lambda(\beta_{1}(q)))$, which does not depend on the choice $\alpha,\beta\in\{s,t\}$. This generalizes for higher-dimensional cubes: for $q\in Q_{n}$ and $i\in\{1,\dotsc,n\}$ let

[TABLE]

Again, we can replace some of $s$’s with $t$’s and get the same result. Denote $\lambda(q)=(\lambda_{1}(q),\dotsc,\lambda_{n}(q))$.

Lemma 1**.**

Some properties:

1. (1)

For $q\in Q_{n}$, $\alpha\in\{s,t\}$,

[TABLE] 2. (2)

$\lambda_{1}(q)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{2}(q)\mathrel{\overset{\mathsf{ev}}{<}}\dots\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{n}(q)$. 3. (3)

$Q$* is consistent iff for every $n$ and $q\in Q_{n}$, all $\lambda_{i}(q)$ are different.* 4. (4)

If $Q$ is ordered, then $\lambda_{i}(q)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{j}(q)$ implies $i<j$.

Proof 2.1**.**

1. (1)

For $j\geq i$ we have

[TABLE]

For $j<i$,

[TABLE] 2. (2)

Fix $q\in Q_{n}$ and $i\in\{1,\dots,n-1\}$ and let $z=s_{1}s_{2}\dots s_{i-1}s_{i+2}\dots s_{n}(q)$. Using (1) we obtain that $\lambda_{1}(z)=\lambda_{i}(q)$, $\lambda_{2}(z)=\lambda_{i+1}(q)$; therefore, $\lambda_{i}(q)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{i+1}(q)$. 3. (3)

If $Q$ is not consistent, then there exists $q\in Q_{2}$ such that

[TABLE]

If $\lambda_{i}(q)=\lambda_{j}(q)$ for some $q\in Q_{n}$, $i<j$, then

[TABLE] 4. (4)

If $\lambda_{i}(q)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{j}(q)$ for $j\leq i$, then either $\lambda_{j}(q)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{i}(q)$ (if $j<i$) or $\lambda_{i}(q)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{i}(q)$ (if $i=j$). In both cases $Q$ cannot be ordered.

{exa}

The following HDA is not ordered (due to a “wrong” numbering of the face maps), but we can swap the directions of one of the squares to obtain an ordered HDA. Consider the following HDA $Q$:

• •

$Q_{2}=\{A,B,C\}$,

• •

$Q_{1}=\{a,b,c,d,e,f,g,h,i\}$

• •

$Q_{0}=\{0,1,2,3,4,5,6,7\}$, [math] being the initial state,

with the following face maps:

• •

$s_{2}(A)=s_{1}(B)=a$,

• •

$s_{2}(B)=s_{1}(C)=b$,

• •

$s_{2}(C)=s_{1}(A)=c$,

• •

$s_{1}(a)=s_{1}(b)=s_{1}(c)=0$

• •

the other face maps are not of importance for the example.

This is not ordered because antisymmetry is broken by the following: $\lambda(a)=\lambda_{1}(A)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{2}(A)=\lambda(c)$ and $\lambda(b)=\lambda_{1}(B)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{2}(B)=\lambda(a)$ and $\lambda(c)=\lambda_{1}(C)\mathrel{\overset{\mathsf{ev}}{<}}\lambda_{2}(C)=\lambda(b)$. Note that $Q$ is almost the union of the three start faces of a 3-cell, except that the face maps of $A$ are in the “wrong” order, i.e., in a cube we would have the following:

• •

$s_{1}(A)=s_{1}(B)=a$,

• •

$s_{2}(B)=s_{1}(C)=b$,

• •

$s_{2}(C)=s_{2}(A)=c$.

However, we can create a slightly different HDA (called symmetric variant) that would be ordered, by only changing the maps of one of the offending squares, i.e., take the HDA from above only with $A^{\prime}$ instead of $A$, such that $s_{1}(A^{\prime})=a$ and $s_{2}(A^{\prime})=c$. We could have, alternatively, reordered the maps of $B$ or $C$ to obtain other ordered symmetric variants.

In the rest of the paper we consider only ordered HDAs. As we show later, in Proposition 6, only ordered HDAs can be sculpted. The result below shows that this is not a restriction, as any consistent precubical set can be ordered by re-arranging its face maps.

Proposition 2**.**

For every consistent precubical set $Q$ there exists an ordered precubical set $Q^{\prime}$ that is a symmetric variant of $Q$.

By a “symmetric variant” we mean that $Q$ and $Q^{\prime}$ are isomorphic when regarded as symmetric precubical sets [GM03]. In particular, there is a bijection between the set of paths on $Q$ and the set of paths on $Q^{\prime}$ (see the proof details in Appendix A).

ST-structures

An ST-configuration over a finite set $E$ of events is a pair $(S,T)$ of sets $T\subseteq S\subseteq E$. An ST-structure is a pair $\mathsf{ST}=(E,\mathit{C})$ consisting of a finite set $E$ of events and a set $\mathit{C}$ of ST-configurations over $E$.

Intuitively, in an ST-configuration $(S,T)$ the set $S$ contains events which have started and $T$ contains events which have terminated. Hence the condition $T\subseteq S$: only events which have already started can terminate. The events in $S\setminus T$ are running concurrently, and we call $|S\setminus T|$ the concurrency degree of $(S,T)$.

The notion of having events which are currently running, i.e., started but not terminated, is a key aspect captured by ST-structures and also by HDA through their higher dimensional cells. Other event-based formalisms such as configuration structures [vGP95, vGP09] or event structures [NPW81, Win86] cannot express this.

A step between two ST-configurations is either

**s-step: **

$(S,T)\xrightarrow[s]{e}(S^{\prime},T^{\prime})$ with $T=T^{\prime}$, $e\notin S$ and $S^{\prime}=S\cup\{e\}$, or

**t-step: **

$(S,T)\xrightarrow[t]{e}(S^{\prime},T^{\prime})$ with $S=S^{\prime}$, $e\notin T$, and $T^{\prime}=T\cup\{e\}$.

When the type is unimportant we write $\smash{\xrightarrow{e}}$. A path of an ST-structure, denoted $\pi$, is a sequence of steps, where the end of one is the beginning of the next, i.e.,

[TABLE]

A path is rooted if it starts in $(\emptyset,\emptyset)$. An ST-structure $\mathsf{ST}=(E,\mathit{C})$ is said to be

1. (A)

rooted if $(\emptyset,\emptyset)\in\mathit{C}$; 2. (B)

connected if for any $(S,T)\in\mathit{C}$ there exists a rooted path ending in $(S,T)$; 3. (C)

closed under single events if, for all $(S,T)\in\mathit{C}$ and all $e\in S\setminus T$, also $(S,T\cup\{e\})\in\mathit{C}$ and $(S\setminus\{e\},T)\in\mathit{C}$.

$\mathsf{ST}$ is regular if it satisfies all three conditions above. Figure 6(center) shows a regular ST-structure.

ST-structures were introduced in [Joh16] as an event-based counterpart of HDA that are also a natural extension of configuration structures and event structures.

The notions of rootedness and connectedness for ST-structures are similar to connectedness for HDA. The notion of being closed under single events mirrors the fact that cells in HDA have all their faces, and (by non-selflinkedness) these are all distinct. Thus regularity is assumed in some of the results below.

A morphism of ST-structures $(E,\mathit{C})\to(E^{\prime},\mathit{C}^{\prime})$ is a partial function $f:E\rightharpoonup E^{\prime}$ of events which preserves ST-configurations (i.e., for all $(S,T)\in\mathit{C}$ we have $f(S,T):=(f(S),f(T))\in\mathit{C}^{\prime}$) and is locally total and injective (i.e., for all $(S,T)\in\mathit{C}$, the restriction $f_{\upharpoonleft S}:S\to E^{\prime}$ is a total and injective function). This defines a category $\mathbb{ST}$ of ST-structures. Two ST-structures are isomorphic, denoted $\mathsf{ST}\cong\mathsf{ST}^{\prime}$, if there exists a bijective morphism between them.

{defi}

Let $\mathsf{ST}=(E,\mathit{C})$ be an ST-structure and $\mathord{\sim}\subseteq E\times E$ an equivalence relation. The quotient of $\mathsf{ST}$ under $\sim$ is the ST-structure ${\mathsf{ST}}_{\!/\mathord{\sim}}=({E}_{\!/\mathord{\sim}},{\mathit{C}}_{\!/\mathord{\sim}})$, with ${\mathit{C}}_{\!/\mathord{\sim}}=\{({S}_{\!/\mathord{\sim}},{T}_{\!/\mathord{\sim}})\mid(S,T)\in\mathit{C}\}$.

It is clear that ${\mathsf{ST}}_{\!/\mathord{\sim}}$ is again an ST-structure. To ease notation we will sometimes denote $({S}_{\!/\mathord{\sim}},{T}_{\!/\mathord{\sim}})={(S,T)}_{\!/\mathord{\sim}}$. The quotient map $\gamma:\mathsf{ST}\to{\mathsf{ST}}_{\!/\mathord{\sim}}:e\mapsto[e]_{\sim}$ is generally not an ST-morphism, failing local injectivity.

{defi}

An equivalence relation $\mathord{\sim}\subseteq E\times E$ on an ST-structure $\mathsf{ST}=(E,\mathit{C})$ is collapsing if there is $(S,T)\in\mathit{C}$ and $e,e^{\prime}\in S$ with $e\neq e^{\prime}$ and $e\sim e^{\prime}$. Otherwise, $\sim$ is non-collapsing.

Lemma 3**.**

$\mathord{\sim}\subseteq E\times E$* is non-collapsing iff the quotient map $\gamma:\mathsf{ST}\to{\mathsf{ST}}_{\!/\mathord{\sim}}:e\mapsto[e]_{\sim}$ is an ST-morphism.*

Proof 2.2**.**

If $\sim$ is collapsing, then $\gamma$ is not locally injective. For the other direction, assume that $\gamma$ is not locally injective, then there is $(S,T)\in\mathit{C}$ and $e,e^{\prime}\in S$ with $e\neq e^{\prime}$ and $\gamma(e)=\gamma(e^{\prime})$, thus $e\sim e^{\prime}$: ergo $\sim$ is collapsing.

We want to compare sculptures and ST-structures. To this end, we introduce a small but important modification to ST-structures which consists in ordering the events.

Let $E$ be a totally ordered set of events with ordering $<$. An ordered ST-structure is an ST-structure on $E$, and morphisms $f:(E,\mathit{C})\to(E^{\prime},\mathit{C}^{\prime})$ of ordered ST-structures respect the ordering, i.e., if $f(e_{1})$ and $f(e_{2})$ are defined and $e_{1}<e_{2}$, then $f(e_{1})<f(e_{2})$. This defines a category of ordered ST-structures.

Chu spaces

The model of Chu spaces has been developed by Gupta and Pratt [Gup94, Pra95] in order to study the event-state duality [Pra92]. A Chu space over a finite set $K$ is a triple $\mathsf{Chu}=(E,r,X)$ with $E$ and $X$ sets and $r:E\times X\rightarrow K$ a function called the matrix of the Chu space.

Chu spaces can be viewed in various equivalent ways [Gup94, Chap. 5]. For our setting, we take the view of $E$ as the set of events and $X$ as the set of configurations. The structure $K$ is representing the possible values the events may take, e.g.: $K=\boldsymbol{2}=\{0,1\}$ is the classical case of an event being either not started ([math]) or terminated ($1$), hence Chu spaces over $\boldsymbol{2}$ correspond to configuration structures [vGP95, vGP09] where an order of $0<1$ is used to define the steps in the system, i.e., steps between states must respect the increasing order when lifted pointwise from $K$ to $X$.

ST-structures capture the “during” aspect in the event-based setting, extending configuration structures with this notion. Therefore we need another structure $K=\boldsymbol{3}=\{0,\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}},1\}$ with the order $0<\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}<1$, introducing the value  to stand for during, or in transition. Note that [Gup94] studies Chu spaces over $\boldsymbol{2}$, whereas Pratt proposed to study Chu spaces over $\boldsymbol{3}$ and other structures in [Pra03].

A Chu space is extensional [Gup94] if it holds for every $x\neq x^{\prime}$ that there exists $e\in E$ such that $r(e,x)\neq r(e,x^{\prime})$. We assume extensionality. Using currying, we can view a Chu space $(E,r,X)$ over $K$ as a structure $X\subseteq K^{E}$ (this needs extensionality). Consequently, we will often write $x(e)$ instead of $r(e,x)$ below. A Chu space is separable [Pra02] (called T0 in [Gup94]) if no two events are the same, that is, for all $e\neq e^{\prime}$ there is $x\in X$ such that $r(e,x)\neq r(e^{\prime},x)$.

{defi}

[translations between ST and Chu] For an ST-structure $\mathsf{ST}=(E,\mathit{C})$ construct $(E,X)^{\mathsf{ST}}$ the associated Chu space over $\boldsymbol{3}$ with $E$ the set of events from $\mathsf{ST}$, and $X\subseteq\boldsymbol{3}^{E}$ containing for each ST-configuration $(S,T)\in\mathit{C}$ the state $x^{(S,T)}\in X$ formed by assigning to each $e\in E$:

• •

$e\rightarrow 0$ if $e\not\in S$ and $e\not\in T$;

• •

$e\rightarrow\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ if $e\in S$ and $e\not\in T$;

• •

$e\rightarrow 1$ if $e\in S$ and $e\in T$.111The case $e\notin S\wedge e\in T$ is dismissed by the requirement $T\subseteq S$ of ST-configurations.

Call this mapping $\mathsf{ChuST}(S,T)$ when applied to an ST-configuration and $\mathsf{ChuST}(\mathsf{ST})$ when applied to an ST-structure. The other way, we translate an extensional Chu space $(E,X)$ into an ST-structure over $E$ with one ST-configuration $(S,T)^{x}$ for each state $x\in X$ using the inverse of the above mapping. We use $\mathsf{ST}\mathsf{Chu}(x)$ for the ST-configuration obtained from the event listing $x$.

{thmC}

[[Joh16, Sec. 3.4]]

For any ST-structure $\mathsf{ST}$, $\mathsf{ST}\mathsf{Chu}(\mathsf{ChuST}(\mathsf{ST}))\cong\mathsf{ST}$. For any (extensional) Chu space $\mathsf{Chu}$ over $\boldsymbol{3}$, $\mathsf{ChuST}(\mathsf{ST}\mathsf{Chu}(\mathsf{Chu})\cong\mathsf{Chu}$.

3. Sculptures

Inspired by the Chu notation for states, we define a bulk in two equivalent ways, both of which can be seen as the complete $\mathsf{Chu}$ over $\boldsymbol{3}$.

{defi}

Let $d\in\mathbbm{N}$. The $d$-dimensional bulk $\mathbf{B}^{d}$ is the precubical set defined as follows. For $n=0,\dotsc,d$, let

[TABLE]

be the set of tuples with precisely $n$ occurrences of . For $n=1,\dotsc,d$ and $k=1,\dotsc,n$, define face maps $s_{k},t_{k}:\mathbf{B}^{d}_{n}\to\mathbf{B}^{d}_{n-1}$ as follows: for $x=(x_{1},\dotsc,x_{d})\in\mathbf{B}^{d}_{n}$ with $x_{i_{1}}=\dotsm=x_{i_{n}}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$, let $s_{k}x=(x_{1},\dotsc,0_{i_{k}},\dotsc,x_{d})$ and $t_{k}x=(x_{1},\dotsc,1_{i_{k}},\dotsc,x_{d})$ be the tuples with the $k$-th occurrence of set to [math] or $1$, respectively.

The initial state $I_{\mathbf{B}^{d}}$ of the bulk $\mathbf{B}^{d}$ is the cell $(0,\dotsc,0)$. This turns bulks into HDA.

Let $\mathbf{S}^{d}=(\oldvec{E},\mathit{C})$ be the complete ordered ST-structure on $\oldvec{E}=(1,\dotsc,d)$, with $\mathit{C}=\{(S,T)\mid T\subseteq S\subseteq\oldvec{E}\}$. There is a bijection between $\mathbf{S}^{d}$ and the bulk $\mathbf{B}^{d}$ which maps a configuration $(S,T)$ to the cell $(x_{1},\dotsc,x_{d})$ given by

[TABLE]

cf. Def. 2, and using the inverse of the above when mapping the other way. This bijection induces face maps in $\mathbf{S}^{d}$ as follows: for $x=(x_{1},\dotsc,x_{d})\in\mathbf{B}^{d}_{n}$ with $x_{i_{1}}=\dotsm=x_{i_{n}}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ and $s_{k}x=(x_{1},\dotsc,0_{i_{k}},\dotsc,x_{d})$, i.e., with the $k$-th occurrence of set to [math], then for the respective ST-configuration $(S,T)^{x}$ the map is $s_{k}((S,T)^{x})=(S,T)^{(x_{1},\dotsc,0_{i_{k}},\dotsc,x_{d})}=(S^{x}\setminus\{i_{k}\},T^{x})$. Conversely, $\mathbf{S}^{d}$ can be equipped with face maps as $s_{k}((S,T))=(S\setminus\{i_{k}\},T)$ and $t_{k}((S,T))=(S,T\cup\{i_{k}\})$ with $i_{k}\in\oldvec{E}$ being the $k^{th}$ event in the subset listing $\oldvec{E}\!\!\upharpoonright_{S\setminus T}$. We will use these two notions of bulk interchangeably and denote this bijection as $\mathbf{S}^{d}\mathrel{\leftrightarrow}\mathbf{B}^{d}$.

Let $d\leq d^{\prime}$ and $b:\{1,\dotsc,d\}\to\{1,\dotsc,d^{\prime}\}$ a strictly increasing function. This defines an embedding, also denoted $b:\mathbf{B}^{d}\hookrightarrow\mathbf{B}^{d^{\prime}}$, mapping any cell $(t_{1},\dotsc,t_{d})$ to $(u_{1},\dotsc,u_{d^{\prime}})$ given by

[TABLE]

Every HDA morphism $\mathbf{B}^{d}\to\mathbf{B}^{d^{\prime}}$ is of this form (but not every precubical morphism because these do not need to preserve the initial state), and there are no morphisms $\mathbf{B}^{d}\to\mathbf{B}^{d^{\prime}}$ for $d>d^{\prime}$.

Lemma 4**.**

Fix a bulk $\mathbf{B}^{d}$ and take two transitions $(t_{1},\dots,t_{d})$ and $(u_{1},\dots,u_{d})$, and let $k$ be the unique index s.t. $t_{k}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$, and the same for $u_{l}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$. Then the two transitions represent the same event, i.e., $(t_{1},\dots,t_{d})\overset{\textsf{ev}}{\sim}(u_{1},\dots,u_{d})$, iff $k=l$. Therefore, the set of universal events is $\mathit{UE}(\mathbf{B}^{d})=\{1,\dots,d\}$. Moreover, the order $\mathrel{\overset{\mathsf{ev}}{<}}$ on $\mathit{UE}(\mathbf{B}^{d})$ agrees with the natural order on $\{1,\dots,d\}$.

Proof 3.1**.**

For a transition $t=(t_{1},\dots,t_{d})$ in $\mathbf{B}^{d}$ let $dir(t)$ be the unique index such that $t_{dir(t)}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$. Let $y=(y_{1},\dots,y_{d})$ be an arbitrary 2-cube and its two unique indices $k<l$ such that $y_{k}=y_{l}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$. We have $dir(s_{1}(y))=dir(t_{1}(y))=l$ and $dir(s_{2}(y))=dir(t_{2}(y))=k$. Therefore, $t\overset{\textsf{ev}}{\sim}u$ implies $dir(t)=dir(u)$.

We will show that $t\overset{\textsf{ev}}{\sim}u$ for any two transitions $t,u$ with $dir(t)=dir(u)=k$. Induction with respect to the number $m$ of indices $i$ such that $t_{i}\neq u_{i}$. If $m=0$, then $t=u$ and there is nothing to prove. If $m>0$, then choose any index $j$ such that $t_{j}\neq u_{j}$; the square

[TABLE]

assures that $t\overset{\textsf{ev}}{\sim}(t_{1},\dots,t_{j-1},u_{j},t_{j+1},\dots,t_{d})=t^{\prime}$, and $t^{\prime}\overset{\textsf{ev}}{\sim}u$ by the inductive hypothesis. As a consequence, $dir:\mathit{UE}(\mathbf{B}^{d})\to\{1,\dots,d\}$ is a bijection.

For a square $y$ with $y_{k}=y_{l}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$, $k<l$, we have $dir(s_{2}(y))=k<l=dir(s_{1}(y))$ and $\lambda(s_{2}(y))\mathrel{\overset{\mathsf{ev}}{<}}\lambda(s_{1}(y))$. Therefore, the order $\mathrel{\overset{\mathsf{ev}}{<}}$ on $\mathit{UE}(\mathbf{B}^{d})$ agrees with the order on $\{1,\dotsc,d\}$.

{defi}

A sculpture, denoted $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$, is an HDA $Q$ together with a bulk $\mathbf{B}^{d}$ and an HDA embedding $\textit{em}:Q\hookrightarrow\mathbf{B}^{d}$. A morphism of sculptures $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$, $Q^{\prime}\!\stackrel{{\scriptstyle\textit{em}^{\prime}}}{{\hookrightarrow}}\!\mathbf{B}^{d^{\prime}}$ is a pair of HDA morphisms $f:Q\to Q^{\prime}$, $b:\mathbf{B}^{d}\to\mathbf{B}^{d^{\prime}}$ such that the square

[TABLE]

commutes, i.e., $b\circ\textit{em}=\textit{em}^{\prime}\circ f$.

We say that an HDA $Q$ is sculptable if there exists a sculpture $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$.

For a morphism $(f,b)$ as above, we must have $d^{\prime}\geq d$ and $b$ injective, hence also $f$ is injective. Two sculptures are isomorphic, denoted $\cong$, when $f$ and $b$ are isomorphisms (implying $d=d^{\prime}$ and $b=\operatorname{id}$).

For the special case of $Q=Q^{\prime}$ above, we see that any sculpture $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$ can be over-embedded into a sculpture $Q\!\stackrel{{\scriptstyle b\circ\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d^{\prime}}$ for $d^{\prime}>d$. Conversely, any sculpture $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$ admits a minimal bulk $\mathbf{B}^{d_{\textup{min}}}$ for which $Q\!\stackrel{{\scriptstyle\textit{em}^{\prime}}}{{\hookrightarrow}}\!\mathbf{B}^{d_{\textup{min}}}\!\stackrel{{\scriptstyle b^{\prime}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$ with $b^{\prime}\circ\textit{em}^{\prime}=\textit{em}$, i.e., such that there is no factorization of the embedding of $Q$ through $\mathbf{B}^{d^{\prime}}$ for any $d^{\prime}<d_{\textup{min}}$. We call such a minimal embedding simplistic.

Remark 5**.**

One precubical set can be seen as sculpted from two different-dimensional bulks, in both cases being a simplistic sculpture, i.e., it all depends on the embedding morphism (cf. Figure 6). Because of this we cannot determine from an HDA alone in which sculpture it enters (if any).

Working with unfoldings is not particularly good either. The interleaving square from Figure 7 (left) can be sculpted from $\mathbf{B}^{2}$, but its unfolding may be sculpted simplistically from $\mathbf{B}^{3}$ or $\mathbf{B}^{4}$; we cannot decide which.

All the sculptures in Figs. 6 and 7 are simplistic.

Proposition 6**.**

If an HDA $Q$ is not ordered, then it is not sculptable.

Proof 3.2**.**

Any precubical morphism $\textit{em}:Q\to\mathbf{B}^{d}$ induces a map

[TABLE]

If $Q$ is not ordered, then there exists $a\in\mathit{UE}(Q)$ such that $a\mathrel{\overset{\mathsf{ev}}{<}}a$, which implies $\mathit{UE}(\textit{em})(a)\mathrel{\overset{\mathsf{ev}}{<}}\mathit{UE}(\textit{em})(a)$, which is a contradiction.

We show that sculptures and regular ordered ST-structures are in bijective correspondence while also respecting the computation steps. This result also resolves the open problem noticed in [Joh16, Sec. 3.3] that there is no adjunction between ST-structures and general HDA.

Recall that an ST-structure is regular if it is rooted, connected, and closed under single events. Through the observation from Section 2 the results in this section extend to (regular) Chu spaces over $\boldsymbol{3}$ as well.

{defi}

[from ordered regular ST-structures to sculptures] We define a mapping $\mathsf{H}$ that for any regular ordered ST-structure $S$ on events $\oldvec{E}=\{e_{1},\dotsc,e_{d}\}$, generates an HDA, as well as a bulk and an embedding, thus a sculpture, $\mathsf{H}(S)$, as follows. By the bijection between the complete ST-structure $\mathbf{S}^{d}$ on events $\oldvec{E}$ and $\mathbf{B}^{d}$, there is an embedding $S\hookrightarrow\mathbf{S}^{d}\mathrel{\leftrightarrow}\mathbf{B}^{d}$, where $\hookrightarrow$ simply maps $e_{i}\in\oldvec{E}$ to $i\in\mathbf{S}^{d}$. $\mathsf{H}(S)$ is given by the composed embedding.

{defi}

[from sculptures to ordered regular ST-structures]

Define a mapping $\mathsf{ST}$ which to a sculpture $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$ associates the ST-structure $\mathsf{ST}(Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d})$ as follows. By the bijection between $\mathbf{B}^{d}$ and the complete ST-structure $\mathbf{S}^{d}$ on events $\{1,\dotsc,d\}$, there is an embedding $Q\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\mathbf{B}^{d}\mathrel{\leftrightarrow}\mathbf{S}^{d}$. $\mathsf{ST}(Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d})$ is given by the composed embedding.

It is clear that $\mathsf{ST}(Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d})$ is rooted, connected and closed under single events, i.e., regular.

The following result shows a one-to-one correspondence between regular ordered ST-structures and sculptures; the proof is clear by composition of the mappings above.

Theorem 7**.**

For any regular ordered ST-structure $\mathsf{ST}$, $\mathsf{ST}(\mathsf{H}(\mathsf{ST}))\cong\mathsf{ST}$. For any sculpture $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$, $\mathsf{H}(\mathsf{ST}(Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}))\cong Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$.

We can also understand $\mathsf{ST}$ as labeling every cell of the sculpture with an ST-configuration, or equivalently (because of Theorem 2) with a Chu state.

Lemma 8**.**

The mapping $\mathsf{H}$ is functorial, in the sense that an ordered ST-morphism $f:\mathsf{ST}_{1}\to\mathsf{ST}_{2}$ is translated into an HDA morphism $\mathsf{H}(f):\mathsf{H}(\mathsf{ST}_{1})\to\mathsf{H}(\mathsf{ST}_{2})$, given by $\mathsf{H}(f)({(S,T)})=\mathsf{H}({f(S,T)})$. If $f$ is total and injective, then $\mathsf{H}(f)$ is also a sculpture morphism.

Proof 3.3**.**

The first part of the lemma is trivial.

For the second part we denote $S_{1}=(E_{1},\mathit{C}_{1})$ and $S_{2}=(E_{2},\mathit{C}_{2})$. The morphism $b:\mathbf{B}^{d_{1}}\cong\mathbf{S}^{|E_{1}|}\to\mathbf{S}^{|E_{2}|}\cong\mathbf{B}^{d_{2}}$ is defined by the map $f:E_{1}\to E_{2}$, which makes the sculptures morphism diagram commute.

[TABLE]

4. Decidability for the Class of Sculptures

We proceed to develop an algorithm to decide whether a given HDA can be sculpted. At first one could simply search for embedding into bulks of any dimension limited by the number of edges in the HDA. But a naive calculation reveals this to be more than doubly exponential in the number of edges.222For an HDA $Q$ with $|Q_{1}|=n$ it is enough to check for embeddings into the single bulk of the largest dimension $n$, because any sculpture can be over-embedded. There are $|\mathbf{B}^{n}|^{|Q|}$ maps to check, which is larger than focusing on maps between transitions only, i.e., larger than $|\mathbf{B}^{n}_{1}|^{n}=(n*2^{(n-1)})^{n}$. This should also be multiplied with the amount of time it takes to check whether an individual map is an embedding, i.e., checking injectivity, cubical laws, face maps preservation for all higher cells, etc.

In this section we work out a more algorithmic approach which is also more efficient. First we define a way of translating HDA into ST-structures without the need of a bulk and an embedding. Instead we give an inductive construction that works with rooted paths.

{defi}

A path having the following form, for $v_{i}\in Q_{0}$ and $e_{j}\in Q_{1}$,

[TABLE]

will be called sequential. An HDA $Q$ has non-repeating events if for every sequential path all universal labels $\lambda(e_{1}),\lambda(e_{2}),\dotsc,\lambda(e_{n})$ are different.

Proposition 9**.**

If $Q$ has repeating events, then it cannot be sculpted.

Proof 4.1**.**

If a path $\pi$ in $Q$ repeats events, then its image $em(\pi)$ in $\mathbf{B}^{d}$ also repeats events, by the functoriality of $\mathit{UE}$; but bulks have non-repeating events.

Proposition 10**.**

If $Q$ has non-repeating events, then it is consistent.

Proof 4.2**.**

Easy.

{exa}

An HDA that has repeating events is the full square, $q$, to the right which has the upper-left and lower-right corners identified into $q_{0}$. We find the sequential path $I\xrightarrow{s}s_{2}(q)\xrightarrow{t}q_{0}\xrightarrow{s}t_{2}(q)\xrightarrow{t}q^{\prime}_{0}$ on which the same label $\lambda_{1}(q)$ appears twice. This example is acyclic; otherwise, the non-repeating property implies acyclicity.

q$$I$$q_{0}$$q_{0}$$q^{\prime}_{0}$$\vphantom{t}s_{2}q$$t_{2}q

{defi}

[from HDA to ST-structures through paths] Define a map $\mathsf{ST}_{\pi}:\mathbb{HDA}\rightarrow\mathbb{ST}$ which builds an ST-structure $\mathsf{ST}_{\pi}(Q)=(\mathit{UE}(Q),\mathit{C})$ in the following way. For every path $\pi=\pi^{\prime}\xrightarrow{\alpha}q$ we assign an ST-configuration $\mathsf{ST}_{\pi}(\pi)=(S_{\pi},T_{\pi})$ in the following way.

1. (1)

For the minimal rooted path we associate $\mathsf{ST}_{\pi}(I)=(\emptyset,\emptyset)$. 2. (2)

If $\alpha=s_{i}$, then we put $\mathsf{ST}_{\pi}(\pi)=\mathsf{ST}_{\pi}(\pi^{\prime})\cup(\{\lambda_{i}(q)\},\emptyset)=(S_{\pi}\cup\{\lambda_{i}(q)\},T_{\pi})$, i.e., we start the event $\lambda_{i}(q)$. 3. (3)

If $\alpha=t_{i}$, then we put $\mathsf{ST}_{\pi}(\pi)=\mathsf{ST}_{\pi}(\pi^{\prime})\cup(\emptyset,\{\lambda_{i}(\mathit{en}(\pi^{\prime}))\})$, i.e., we terminate the event $\lambda_{i}(\mathit{en}(\pi^{\prime}))$.

Finally, $\mathit{C}$ is the set of all these ST-configurations, i.e.,

[TABLE]

where $\operatorname{\mathsf{Path}}(Q)_{*}$ denotes the set of all rooted paths of $Q$.

The construction is similar to an unfolding [FL15]; see [Joh16, Def. 3.39] for a related construction.

The next lemmas are used to establish that for every path $\pi$ the pair $(S_{\pi},T_{\pi})$ is indeed an ST-configuration.

Lemma 11**.**

If $\pi$ is a sequential path (2), then

[TABLE]

Proof 4.3**.**

Obvious induction.

Lemma 12**.**

Homotopic paths have the same associated ST-configurations (i.e., if $\pi\sim\varrho$, then $S_{\pi}=S_{\varrho}$, $T_{\pi}=T_{\varrho}$).

Proof 4.4**.**

It is enough to consider the case when $\pi$ and $\varrho$ are elementary homotopic and that the homotopy changes the final segments of these paths. Thus

[TABLE]

where one of the following cases holds (denote $s=\mathit{en}(\sigma)$).

• •

$\alpha=\beta=s$, $i<j$, $k=j-1$, $l=i$. Then $T_{\pi}=T_{\sigma}=T_{\varrho}$ and

[TABLE]

• •

$\alpha=s$, $\beta=t$, $i>k=j$, $l=i-1$. Then

[TABLE]

• •

$\alpha=s$, $\beta=t$, $i=l<j$, $k=j-1$.

• •

$\alpha=\beta=t$, $k=j<i$, $l=i-1$.

Calculations in the last two cases are similar.

{lemC}

[[Fah05b, Lem.4.38]] Every rooted path is homotopic to a path of the type $(st)^{k}s^{n}$, for any $n,k\geq 0$.

Proof 4.5**.**

Assume that $\pi$ has a segment of type $sst$, namely

[TABLE]

If $j=l$, then we replace it by a homotopic segment

• •

$s_{i}(s_{j}(r))=s_{j-1}(s_{i}(r))\xrightarrow{s_{j-1}}s_{i}(r)\xrightarrow{s_{i}}r\xrightarrow{t_{l}}t_{l}(r)$* if $i<j$*

• •

$s_{i}(s_{j}(r))=s_{j}s_{i+1}(r)\xrightarrow{s_{j}}s_{i+1}(r)\xrightarrow{s_{i+1}}r\xrightarrow{t_{l}}t_{l}(r)$* if $i\geq j$*

to assure that $j\neq l$. Next, we replace it by

1. (1)

$s_{i}(s_{j}(r))\xrightarrow{s_{i}}s_{j}(r)\xrightarrow{t_{l-1}}t_{l-1}(s_{j}(r))=s_{j}(t_{l}(r))\xrightarrow{s_{j}}t_{l}(r)$* if $j<l$,* 2. (2)

$s_{i}(s_{j}(r))\xrightarrow{s_{i}}s_{j}(r)\xrightarrow{t_{l}}t_{l}(s_{j}(r))=s_{j-1}(t_{l}(r))\xrightarrow{s_{j-1}}t_{l}(r)$* if $j>l$,*

and obtain a homotopic segment of type $sts$. We repeat this procedure as long as there is a type $sst$ subpath (which is finitely many times). Eventually we obtain a path homotopic to $\pi$ having the required type.

Lemma 13**.**

Fix $n\geq 1$ and $i\in\{1,\dotsc,n\}$. Every path of type $s^{n}$, starting in a vertex, is homotopic to a path of type $s_{1}s_{2}\dots s_{n-2}s_{n-1}s_{i}$.

Proof 4.6**.**

For $i=n$ this follows from the canonical presentation of an iterated face map. In general, we start with $s_{1}\dots s_{n}$ and move $s_{i}$ to the rightmost place using precubical identities, i.e., $s_{1}\dots s_{i-1}s_{i}s_{i+1}s_{i+2}\dots s_{n}=s_{1}\dots s_{i-1}s_{i}s_{i}s_{i+2}\dots s_{n}=s_{1}\dots s_{i-1}s_{i}s_{i+1}s_{i}s_{i+3}\dots s_{n}=\dots=s_{1}\dots s_{n-2}s_{i}s_{n}=s_{1}\dots s_{n-2}s_{n-1}s_{i}$.

Lemma 14**.**

For every $n,k\geq 0$, every rooted path $\pi$ ending in $q\in Q_{n}$, and any $i\in\{1,\dotsc,n\}$, there exists a path that is homotopic to $\pi$ and has the type $(s_{1}t_{1})^{k}s_{1}s_{2}\dots s_{n-2}s_{n-1}s_{i}$.

Proof 4.7**.**

This follows from the two preceding lemmas.

Proposition 15**.**

For every rooted path $\pi$, $(S_{\pi},T_{\pi})$ is an ST-configuration (i.e., $S_{\pi}\supseteq T_{\pi}$).

Proof 4.8**.**

Induction with respect to $\pi$; enough to check the case when $\pi=\pi^{\prime}\xrightarrow{t_{i}}t_{i}(q)$, $q=\mathit{en}(\pi^{\prime})$. By Lemma 14 there exists a path $\varrho^{\prime}=\varrho^{\prime\prime}\xrightarrow{s_{i}}q$ homotopic to $\pi^{\prime}$. Thus,

[TABLE]

Proposition 16**.**

Assume that an HDA $Q$ has non-repeating events. Then $S_{\pi}\setminus T_{\pi}=\lambda(\mathit{en}(\pi))$ for every rooted path $\pi$.

Proof 4.9**.**

Note that $\lambda(\mathit{en}(\pi))$ is a tuple, thus a set of universal labels with an order on them; and similarly, the set of events on the left are ordered. We use induction with respect to the structure of $\pi$. If $\pi=I$ — obvious. By Lemmas 14 and 12 we can assume that $\pi$ has the type $(s_{1}t_{1})^{l}s_{1}\dots s_{n}$. Denote $q=\mathit{en}(\pi)\in Q_{n}$. Consider two cases:

• •

$n=0$. Then $\pi=\pi^{\prime}\xrightarrow{t_{1}}q$, with $\lambda(q)=\emptyset$. Using the inductive hypothesis we obtain

[TABLE]

• •

$n>0$. Let $\pi^{\prime}$ be the prefix of $\pi$ of length $2l$. Since $\mathit{en}(\pi^{\prime})$ is a state, then $S_{\pi^{\prime}}=T_{\pi^{\prime}}$ (by the previous case) and $S_{\pi}=S_{\pi^{\prime}}\cup\lambda(q)$, $T_{\pi}=T_{\pi^{\prime}}$ (by Definition 4.2). It remains to show that $\lambda(q)\cap S_{\pi^{\prime}}=\emptyset$. For every $i$

[TABLE]

and the path $\pi^{\prime}\xrightarrow{s_{1}}s_{1}\dots s_{i-1}s_{i+1}\dots s_{n}(q)\xrightarrow{t_{1}}s_{1}\dots s_{i-1}t_{i}s_{i+1}\dots s_{n}(q)$ is sequential. Since $Q$ has non-repeating events, Lemma 11 implies that $\lambda_{i}(q)\not\in S_{\pi^{\prime}}$.

Corollary 17**.**

Assume that $Q$ has non-repeating events. Then for every $i$ and $q\in Q$ and every rooted path $\pi\in\operatorname{\mathsf{Path}}(Q)_{*}$ that can be extended to $\pi\xrightarrow{s_{i}}q$, then $\lambda_{i}(q)\not\in S_{\pi}$.

Proof 4.10**.**

Otherwise, $S_{\pi\xrightarrow{s_{i}}q}=S_{\pi}$, which implies that $\lambda(s_{i}(q))=\lambda(q)$.

Proposition 18**.**

If $Q$ has non-repeating events, then $\mathsf{ST}_{\pi}(Q)$ is a regular ST-structure.

Proof 4.11**.**

Conditions (A) and (B) are obvious. To prove (C), fix $\pi\in\operatorname{\mathsf{Path}}(Q)_{*}$ and

[TABLE]

where $q=\mathit{en}(\pi)$. Let $\varrho$ be a rooted path such that $\varrho\xrightarrow{s_{i}}q$ is homotopic to $\pi$ and let $\varrho^{\prime}=\pi\xrightarrow{t_{i}}t_{i}(q)$. Then

[TABLE]

and

[TABLE]

But $e\not\in S_{\varrho}$ by Corollary 17, so $(S_{\varrho},T_{\varrho})=(S_{\pi}\setminus\{e\},T_{\pi})\in\mathsf{ST}_{\pi}(Q)$.

If the HDA in question is a sculpture, then there is a natural equivalence relation on its cells which captures the notion of event better than the universal event labelling.

{defi}

For a sculpture $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d}$, define $\mathit{UE}(\textit{em}):\mathit{UE}(Q)\to\mathit{UE}(\mathbf{B}^{d})\simeq\mathit{UE}(\mathbf{S}^{d})\simeq\{1,\dotsc,d\}$ to be the map induced by em, i.e., $\mathit{UE}(\textit{em})(\lambda(q))=\lambda(\textit{em}(q))$. This induces an equivalence relation on $\mathit{UE}(Q)$ which we denote $\overset{\mathsf{em}}{\sim}$, i.e., $\lambda(q)\overset{\mathsf{em}}{\sim}\lambda(q^{\prime})$ iff $\mathit{UE}(\textit{em})(\lambda(q))=\mathit{UE}(\textit{em})(\lambda(q^{\prime}))$.

Lemma 19**.**

Let $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{S}^{d}$ be a sculpture, then ${(S_{\pi},T_{\pi})}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}=\textit{em}(\mathit{en}(\pi))$ for every rooted path $\pi$.

Proof 4.12**.**

Note that we work with a sculpture that is embedded directly in the $\mathbf{S}^{d}$, which is isomorphic to $\mathbf{B}^{d}$. We do this to simplify the arguments, for otherwise we would have had to go through the isomorphism using the $\mathsf{ST}\mathsf{Chu}$ to translate between tuples and ST-configurations.

We use induction on the length of the path $\pi$. By Lemmas 14 and 12 we may assume that $\pi$ has type $(s_{1}t_{1})^{n}s_{1}\dots s_{k}$, $q=\mathit{en}(\pi)\in Q_{k}$. For $\pi=I$, $(S_{\pi},T_{\pi})=(\emptyset,\emptyset)=\textit{em}(I)$.

For $k=0$, then $\pi=\pi^{\prime}\xrightarrow{s_{1}}e\xrightarrow{t_{1}}q$ is sequential. By Definition 4.2 $S_{\pi}=S_{\pi^{\prime}}\cup\{\lambda(e)\}$ and $T_{\pi}=T_{\pi^{\prime}}\cup\{\lambda(e)\}$ with $\lambda(e)\not\in S_{\pi^{\prime}}$ (because of Corollary 17 since a sculpture has non-repeating events). On the right side, the path $\textit{em}(\pi)=\textit{em}(\pi^{\prime})\xrightarrow{s_{1}}\textit{em}(e)\xrightarrow{t_{1}}\textit{em}(\mathit{en}(\pi))$ has all universal labels different too, thus $\lambda(\textit{em}(e))\not\in S^{\prime}$ for $(S^{\prime},T^{\prime})=\textit{em}(\mathit{en}(\pi^{\prime}))$, and by construction $(S^{\prime}\cup\{\lambda(\textit{em}(e))\},T^{\prime}\cup\{\lambda(\textit{em}(e))\})=\textit{em}(\mathit{en}(\pi))$. We finish this case by applying the induction hypothesis to obtain ${(S_{\pi},T_{\pi})}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}=({S_{\pi^{\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}\cup\{\mathit{UE}(\textit{em})(\lambda(e))\},{T_{\pi^{\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}\cup\{\mathit{UE}(\textit{em})(\lambda(e))\})\stackrel{{\scriptstyle ind}}{{=}}(S^{\prime}\cup\{\mathit{UE}(\textit{em})(\lambda(e))\},T^{\prime}\cup\{\mathit{UE}(\textit{em})(\lambda(e))\})\stackrel{{\scriptstyle\ref{def_eventEquivSculpt}}}{{=}}(S^{\prime}\cup\{\lambda(\textit{em}(e))\},T^{\prime}\cup\{\lambda(\textit{em}(e))\})$.

For $k>0$, then $\pi=\pi^{\prime}\xrightarrow{s_{1}}q_{1}\dots\xrightarrow{s_{k}}q=\pi^{\prime\prime}\xrightarrow{s_{k}}q$ with $\pi^{\prime}$ sequential. From Proposition 16 we have $S_{\pi}=T_{\pi}\cup\{\lambda(q)\}$ and $T_{\pi^{\prime\prime}}=T_{\pi}=T_{\pi^{\prime}}=S_{\pi^{\prime}}$. Denote by $(S,T)=\textit{em}(\mathit{en}(\pi))=\textit{em}(q)$ and by $(S^{\prime\prime},T^{\prime\prime})=\textit{em}(\mathit{en}(\pi^{\prime\prime}))=\textit{em}(s_{k}(q))$. By construction, $(S,T)=(S^{\prime\prime}\cup\{\lambda_{k}(q)\},T^{\prime\prime})$ and by the induction hypothesis we have $(S^{\prime\prime}\cup\{\lambda_{k}(q)\},T^{\prime\prime})\stackrel{{\scriptstyle\text{ind}}}{{=}}({S_{\pi^{\prime\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}\cup\{\lambda_{k}(q)\},{T_{\pi^{\prime\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}})=({S_{\pi^{\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}\cup\{\lambda(s_{k}(q))\}\cup\{\lambda_{k}(q)\},{T_{\pi^{\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}})=({S_{\pi^{\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}\cup\{\lambda(q)\},{T_{\pi^{\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}})=({S_{\pi}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}},{T_{\pi}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}})$, since by the consistency and non-repeated events properties we know that $\lambda_{k}(q)\not\in{S_{\pi^{\prime\prime}}}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}$.

Proposition 20**.**

For a (connected) simplistic sculpture $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{n}$ we have

[TABLE]

Proof 4.13**.**

Note that the requirement of being simplistic is only needed in order to have the same set of events on both sides. The events generated on the left side by $\mathsf{ST}$ are $\{1,\dots,n\}=\mathit{UE}(\mathbf{B}^{n})$ which are the events obtained on the right side due to the application of $\overset{\mathsf{em}}{\sim}$, having the same order.

The isomorphism is then exhibited by the identity map $f$ on the above sets of events. Showing that $f$ preserves ST-configurations is easy by using the previous Lemma 19 since every ST-configuration is generated as $\textit{em}(q)$, but since all cells are reachable then there exists a path $\pi$ ending in $q$ so that we need to show $f(\textit{em}(\mathit{en}(\pi)))={(S_{\pi},T_{\pi})}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}$, which is done by the lemma.

Corollary 21**.**

For a sculpture $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{S}^{d}$ the equivalence $\overset{\mathsf{em}}{\sim}$ is non-collapsing.

{defi}

Let $Q$ be an HDA. A proper event identification on $Q$ is an equivalence relation $\parallel$ on $\mathit{UE}(Q)$ such that

1. (1)

The quotient preorder on $\mathit{UE}(Q)/_{\parallel}$ induced from $\mathit{UE}(Q)$ is antisymmetric. Equivalently, if $a\mathrel{\overset{\mathsf{ev}}{<}}b$, $c\mathrel{\overset{\mathsf{ev}}{<}}d$, $a\parallel d$, $b\parallel c$ for $a,b,c,d\in\mathit{UE}(Q)$, then $a\parallel b\parallel c\parallel d$. 2. (2)

If $\mathit{en}(\pi)=\mathit{en}(\pi^{\prime})$, then $(S_{\pi}/_{\parallel},T_{\pi}/_{\parallel})=(S_{\pi^{\prime}}/_{\parallel},T_{\pi^{\prime}}/_{\parallel})$. 3. (3)

If $(S_{\pi}/_{\parallel},T_{\pi}/_{\parallel})=(S_{\pi^{\prime}}/_{\parallel},T_{\pi^{\prime}}/_{\parallel})$, then $\mathit{en}(\pi)=\mathit{en}(\pi^{\prime})$.

Remark 22**.**

An equivalence relation $\parallel$ is a proper event identification if the sequence of relations

[TABLE]

forms an injective function. Note that the right-most map is not (in general) an ST-map.

Lemma 23**.**

Let $\parallel$ be a proper event identification on $Q$. Then for every $\pi\in\operatorname{\mathsf{Path}}(Q)_{*}$, $\parallel$ is trivial when restricted to $S_{\pi}$.

Proof 4.14**.**

Assume that there exists a path $\pi\in\operatorname{\mathsf{Path}}(Q)_{*}$ and $a\neq b\in S_{\pi}$ such that $a\parallel b$. Without loss of generality we may assume that $\mathit{en}(\pi)$ is a state (extending $\pi$ with some $t_{1}$–type segments if needed), and also that $\pi$ is sequential (by Lemma 12 and 14). Denote

[TABLE]

and let $\pi_{j}$ denote the prefix of $\pi$ ending at $v_{j}$. Since $S_{\pi}=\{\lambda(e_{i})\}_{i=1}^{n}$, then there exist $k<l$ integers such that $\lambda(e_{k})\parallel\lambda(e_{l})$. But then

[TABLE]

so $\parallel$ is not a proper identification, breaking 4(3).

Corollary 24**.**

A proper event identification equivalence on $Q$ is non-collapsing.

Theorem 25**.**

Let $Q$ be a connected HDA with non-repeating events. The following are equivalent:

1. (1)

$Q$* can be sculpted.* 2. (2)

There exists a proper event identification on $Q$.

Proof 4.15**.**

(2)$\Rightarrow$(1). Let $\parallel$ be a proper event identification equivalence. Fix an order-preserving bijective map $j:\mathit{UE}(Q)/_{\parallel}\to\{1,\dotsc,d\}$, which exists by Definition 4(1), with $d$ being the dimension of the quotient. For $q\in Q_{n}$ choose a path $\pi$ ending at $q$ and put

[TABLE]

Lemma 23 tells that the equivalence classes in $S_{\pi}/_{\parallel}$ and $T_{\pi}/_{\parallel}$ are singletons, thus making $\textit{em}(q)=(j(S_{\pi}),j(T_{\pi}))$. We abused the notation here, as the map $j$ should be applied to an equivalence class, but instead we apply it to elements of $\mathit{UE}(Q)$, since for a particular path as we have here, the equivalence classes are singletons. Condition 4(2) assures that $\textit{em}(q)$ does not depend on the choice of $\pi$ as long as $\mathit{en}(\pi)=q$. It remains to prove that em is a morphism of precubical sets, i.e., it preserves the precubical maps.

Let $q\in Q_{n}$, $i\in\{1,\dotsc,n\}$, $\pi=\pi^{\prime}\xrightarrow{s_{i}}q$; then $\textit{em}(q)=(j(S_{\pi}),j(T_{\pi}))$. Since $j$ is injective and order-preserving, we have

[TABLE]

Now let $\pi^{\prime\prime}=\pi\xrightarrow{t_{i}}t_{i}(q)$. A similar calculation shows that

[TABLE]

As a consequence, em is a precubical map $Q\to\mathbf{S}^{d}$.

(1)$\Rightarrow$(2). Let $Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{S}^{d}$ be a sculpture involving $Q$. Consider the equivalence relation $\overset{\mathsf{em}}{\sim}$  from Definition 4. Since this was defined using the functor $\mathit{UE}$ then we know that it preserves the order, thus respecting property 4(1) of being a proper event identification. The other two properties are derived using Lemma 19. For two paths with $\mathit{en}(\pi)=q=\mathit{en}(\pi^{\prime})$ we have ${(S_{\pi},T_{\pi})}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}\stackrel{{\scriptstyle L.\ref{lem:SpiSculpt}}}{{=}}\textit{em}(\mathit{en}(\pi))=\textit{em}(\mathit{en}(\pi^{\prime}))\stackrel{{\scriptstyle L.\ref{lem:SpiSculpt}}}{{=}}{(S_{\pi^{\prime}},T_{\pi^{\prime}})}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}$. For the last property, start with $\textit{em}(\mathit{en}(\pi))\stackrel{{\scriptstyle L.\ref{lem:SpiSculpt}}}{{=}}{(S_{\pi},T_{\pi})}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}={(S_{\pi^{\prime}},T_{\pi^{\prime}})}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}\stackrel{{\scriptstyle L.\ref{lem:SpiSculpt}}}{{=}}\textit{em}(\mathit{en}(\pi^{\prime}))$, and because of the injectivity of em we have $\mathit{en}(\pi)=\mathit{en}(\pi^{\prime})$.

Since the number of equivalence relations on $\mathit{UE}(Q)\times\mathit{UE}(Q)$ is finite, then Theorem 25 translates into an algorithm to determine whether $Q$ is a sculpture: First apply $\mathsf{ST}_{\pi}(Q)$; then choose some equivalence relation on $\mathit{UE}(Q)\times\mathit{UE}(Q)$ and check whether it is a proper event identification. The dimension $m=|\mathit{UE}(Q)|$ is smaller than or equal (when there is no concurrency) to the number of edges $|Q_{1}|=n$. Therefore, the number of relations on $\mathit{UE}(Q)$ that need to be checked is $2^{m^{2}}<2^{n^{2}}$, which in the worst case can be more than exponential in the number of edges of $Q$. For each relation we need to check both that it is an equivalence and the proper event identification properties. If we know how to pick only the equivalence relations, which are exponential in number (i.e., using the Bell numbers333See the Bell numbers sequence as https://oeis.org/A000110 in the OEIS. they are exactly $(\frac{m}{e\cdot ln\,m})^{m}<B_{m}<(\frac{0.792\cdot m}{ln\,(m+1)})^{m}$, see [BT10]) then we have to check these only for proper event identification. But we can do better by constructing a proper event identification (when it exists) while we traverse the HDA with the $\mathsf{ST}_{\pi}$.

In the following we give a more intuitive algorithm, using constructions which iteratively repair $\mathsf{ST}_{\pi}(Q)$ by constructing a finite sequence of increasing equivalence relations, in the end reaching a proper event identification.

For an HDA $Q$, using the notation of Def. 4.2, let $\rho_{0}\subseteq Q\times\mathsf{ST}_{\pi}(Q)$ be the relation $\rho_{0}=\{(q,\mathsf{ST}_{\pi}(\pi))\mid\mathit{en}(\pi)=q\}$. We call this an ST-labeling, forming the composition of the first two relations from Remark 22. For an equivalence relation $\mathord{\sim}\subseteq\mathit{UE}(Q)\times\mathit{UE}(Q)$, let $\rho_{\sim}=\{(q,{(S,T)}_{\!/\mathord{\sim}})\mid(q,(S,T))\in\rho_{0}\}$.

First, the following lemma shows that we can restrict our attention to only ST-labellings of [math]-cells (and because of the previous results, it is enough to apply $\mathsf{ST}_{\pi}$ only to sequential paths).

Lemma 26**.**

If $|\{\sigma\mid(q,\sigma)\in\rho_{0}\}|>1$ for some $q\in Q_{k}$, $k\geq 1$, then also $|\{\sigma^{\prime}\mid(q^{\prime},\sigma^{\prime})\in\rho_{0}\}|>1$ for some $q^{\prime}\in Q_{0}$.

Proof 4.16**.**

Assume $|\{\sigma\mid(q,\sigma)\in\rho_{0}\}|>1$, then there exist two different paths $\pi,\pi^{\prime}$ ending in $q$ s.t. $(q,(S_{\pi},T_{\pi}))$, $(q,(S_{\pi^{\prime}},T_{\pi^{\prime}}))\in\rho_{0}$ with $T_{\pi}\neq T_{\pi^{\prime}}$; this being the only case since, by Proposition 16, $S_{\pi}\setminus T_{\pi}=\lambda(\mathit{en}(\pi))=S_{\pi^{\prime}}\setminus T_{\pi^{\prime}}$. We can complete both $\pi$ and $\pi^{\prime}$ by the same sequence of t-steps from $q$ to its upper corner, i.e., there exist $\pi_{0}=\pi\xrightarrow{t_{k}}\dots\xrightarrow{t_{1}}q_{0}$ and $\pi^{\prime}_{0}=\pi^{\prime}\xrightarrow{t_{k}}\dots\xrightarrow{t_{1}}q_{0}$, with $\mathit{en}(\pi_{0}),\mathit{en}(\pi^{\prime}_{0})\in Q_{0}$. By definition $T_{\pi_{0}}=T_{\pi}\cup\lambda(q)$ and $T_{\pi^{\prime}_{0}}=T_{\pi^{\prime}}\cup\lambda(q)$, which are different, meaning that we found the state $q_{0}$ for the lemma.

We can immediately rule out ST-labellings in which a cell receives ST-configurations with different numbers of events (this would break the property 4(2) of a proper event identification in an irreparable way, cf. Lemmas 23 and 11):

Lemma 27**.**

If there is $q\in Q_{0}$ and $(q,(S,S)),(q,(S^{\prime},S^{\prime}))\in\rho_{0}$ with $|S|\neq|S^{\prime}|$, then $Q$ cannot be sculpted.

Proof 4.17**.**

Assume to the contrary that $Q$ is in a sculpture with embedding $\textit{em}:Q\to\mathbf{B}^{n}$. By construction of $\rho_{0}$, there are two rooted paths $\pi$, $\pi^{\prime}$ in $Q$ which both end in $q$, but with different lengths. By injectivity of em, the images of these paths under em, here denoted $\textit{em}(\pi)$ and $\textit{em}(\pi^{\prime})$, are paths in $\mathbf{B}^{n}$ from the initial state to $\textit{em}(q)$. But inside the bulk $\textit{em}(\pi)$ and $\textit{em}(\pi^{\prime})$ are homotopic, in contradiction to them having different lengths.

We will inductively construct equivalence relations $\sim_{n}$, with the property that $\mathord{\sim}_{n}\subsetneq\mathord{\sim}_{n+1}$. This procedure will either lead to a relation $\mathord{\sim}_{N}=\,\parallel$ that is a proper event identification equivalence as required in Theorem 25 or to an irreparable conflict as explained below.

Let $\mathord{\sim}_{1}=\{(\lambda(q),\lambda(q))\mid\lambda(q)\in\mathit{UE}(Q)\}$, the minimal equivalence relation on $\mathit{UE}(Q)$. If $Q$ is a sculpture, then $\mathord{\sim}_{1}\subseteq\mathord{\overset{\mathsf{em}}{\sim}}$, hence we can safely start our procedure with $\sim_{1}$. Moreover, this minimal equivalence is antisymmetric (preserving the order of $Q$).

Assume, inductively, that $\sim_{n}$ has been constructed for some $n\geq 1$. The next lemma shows that if there are two different cells which receive the same labeling under $\rho_{\sim_{n}}$, then either $Q$ is not a sculpture or we need to backtrack, i.e., we would break property 4(3) since we have equated too much.

Lemma 28**.**

If there are $(q,\sigma),(q^{\prime},\sigma)\in\rho_{\sim_{n}}$ with $q\neq q^{\prime}$, and $Q$ can be sculpted, then $\mathord{\sim}_{n}\not\subseteq\mathord{\overset{\mathsf{em}}{\sim}}$ for any embedding $\textit{em}:Q\hookrightarrow B^{k}$.

Proof 4.18**.**

The proof is by reductio ad absurdum; suppose that there is an embedding for which $\mathord{\sim}_{n}\subseteq\mathord{\overset{\mathsf{em}}{\sim}}$. However, since according to Proposition 20 ${\mathsf{ST}_{\pi}(Q)}_{\!/\mathord{\overset{\mathsf{em}}{\sim}}}$ produces the same labels as $\mathsf{ST}(Q\!\stackrel{{\scriptstyle\textit{em}}}{{\hookrightarrow}}\!\mathbf{B}^{d})$, and since $\mathsf{ST}$ labels each different cell with a different label (because of the injectivity of the embedding), we have a contradiction.

We construct $\sim_{n+1}$ from $\sim_{n}$ by finding and repairing homotopy pairs, which consist of two paths of the form

[TABLE]

The shortest homotopy pair is an interleaving, a pair of two transitions.

Lemma 29**.**

If $q\in Q_{0}$ is such that $|\{\sigma\mid(q,\sigma)\in\rho_{n}\}|>1$, then there exists a homotopy pair with final state $q$.

Proof 4.19**.**

We have $|\{\mathsf{ST}_{\pi}(\pi)\mid\mathit{en}(\pi)=q\}|\geq|\{\sigma\mid(q,\sigma)\in\rho_{n}\}|\geq 2$, hence at least two different rooted paths must lead to $q$. These might share a common prefix $\pi$, which can also be the empty path, i.e., starting at the root. According to Lemma 26 we look only at states, and because of Lemma 14 we can look only at sequential paths, which according to Lemma 11 the corresponding ST-configuration is formed of summing up their events, and since by Lemma 27 these have the same number of events, the paths have the same length.

Now if the homotopy pair is an interleaving $\smash{\pi\xrightarrow{s}e^{a}\xrightarrow{t}v\xrightarrow{s}e^{b}\xrightarrow{t}q}$, $\smash{\pi\xrightarrow{s}e^{c}}$ $\smash{\xrightarrow{t}v^{\prime}\xrightarrow{s}e^{d}\xrightarrow{t}q}$, then we must repair by identifying $\lambda(e^{a})$ with $\lambda(e^{d})$ and $\lambda(e^{c})$ with $\lambda(e^{b})$. If it is not, then there are several choices for identifying events, and some of them may lead into situations like in Lemma 28. Let $\tau$ be any permutation on $\{1,\dotsc,n\}$ with $\tau(1)\neq 1$ and $\tau(n)\neq n$, then we can identify $\lambda(e_{i})$ with $\smash{\lambda(e^{\prime}_{\tau(i)})}$ for all $i=1,\dotsc,n$. The restriction on the permutation is imposed by the fact that we only identify transitions that can possibly be concurrent, which is not the case for two transitions starting from, or ending in, the same cell.

Let $\mathord{\sim_{n+1}}\supsetneq\mathord{\sim_{n}}$ be the equivalence relation thus generated which should still be antisymmetric (otherwise choose another permutation). As this inclusion is proper, it is clear that the described process either stops with a Lemma 28 situation, which cannot be resolved without backtracking, or with a relation $\rho_{N}$ which satisfies Theorem 25.

{exa}

We give an example to illustrate why backtracking might be necessary when applying the algorithm. Figure 11 is a variation of the example in Figure 8 which, as the labeling on the top right shows, can be sculpted. However, if we start our procedure by resolving the homotopy pair on the left in a “wrong” way, see the bottom of the figure, then we get into a contradiction in the top right corner and must backtrack.

Remark 30**.**

In conclusion, our final algorithm has the following steps:

1. (1)

Traverse the HDA using the $\mathsf{ST}_{\pi}$, but because of Lemma 26 we can restrict to only states from $Q_{0}$, and because of Lemmas 12 and 4.4 we can look only at sequential paths. This means that applying $\mathsf{ST}_{\pi}$ is like traversing the graph formed of the $Q_{0}\cup Q_{1}$. This forms the $\rho_{0}$. 2. (2)

During the graph traversal, at each state check the Lemma 27 in constant time. The algorithm can stop here if the check does not succeed. 3. (3)

Form the minimal equivalence relation on $\mathit{UE}(Q)$, called $\mathord{\sim}_{1}$ which produces the coarser labeling $\rho_{1}$. This is the same way as the definition of proper event identification starts, i.e., with an equivalence relation on $\mathit{UE}(Q)$. To build $\mathord{\sim}_{1}$ we need to also traverse all the concurrency 2-cells from $Q_{2}$. 4. (4)

Check in each state the Lemma 28 in constant time. The algorithm can stop here if the check for $\rho_{1}$ does not succeed. 5. (5)

Traverse one more time the graph formed of the $Q_{0}\cup Q_{1}$ to find any homotopy pair, as in Lemma 29.

1. (a)

For each homotopy pair add more equivalences to the previous $\rho_{n}$ resulting from choosing one of the permutations of the transitions of this pair, as explained before. 2. (b)

For all states that have their ST-labels changed by the new equated transitions, check again the Lemma 28. If the check fails, then either backtrack and try another permutation, or the algorithm stops. 3. (c)

For each homotopy pair we may need to try out all the possible permutations, which are $(k-1)!$, with $k$ the length of the homotopy pair.

The complexity of this simple algorithm is mostly influenced by the backtracking that needs to be done for each homotopy pair in step (5). Therefore, the complexity increases with the number of homotopy pairs that exist in the graph, their respective lengths, and the amount of relabeling which triggers checking of Lemma 28. Note that the less concurrency is in the HDA, the more homotopy pairs might exist, which at the same time reduces the amount of work done in step (3), since this decreases with the decrease in amount of concurrency. The length of the homotopy pairs contributes the most, since this induces a factorial amount of backtracking. For the minimal homotopy pair of length 2 (the interleaving square) there is only one choice of permutation. Whereas, the worst case is for a 1-dimensional HDA consisting of a single homotopy pair of length $|Q_{1}|/2$. Calculating precisely the complexity is left as future work, the same as finding more efficient algorithms (e.g., how to combine all into a single traversal).

5. Euclidean Cubical Complexes are Sculptures

This section provides a connection between the combinatorial intuition of sculptures and the geometric intuition of Euclidean HDA. It thus gives a concrete way of identifying precisely the events that a grid imposes on any of its subsets. This is how several works on deadlock detection model their studied systems, as “grids with holes”, which are geometric sculptures in our terminology. We give below only strictly necessary definitions, and one is kindly pointed to [Gra09, FGH*+*16] for background in directed topology.

Directed topological spaces

A directed topological space, or d-space, is a pair $(X,\oldvec{P}X)$ consisting of a topological space $X$ and a set $\oldvec{P}X\subseteq X^{I}$ of directed paths in $X$ which contains all constant paths and is closed under concatenation, monotone reparametrization, and subpath.

Prominent examples of d-spaces are the directed interval $\oldvec{I}=[0,1]$ with the usual ordering and its cousins, the directed $n$-cubes $\oldvec{I}^{n}$ for $n\geq 0$. Similarly, we have the directed Euclidean spaces $\oldvec{\mathbbm{R}}^{n}$, with the usual ordering, for $n\geq 0$.

Morphisms $f:(X,\oldvec{P}X)\to(Y,\oldvec{P}Y)$ of d-spaces are those continuous functions that are also directed, that is, satisfy $f\circ\gamma\in\oldvec{P}Y$ for all $\gamma\in\oldvec{P}X$. It can be shown that for an arbitrary d-space $(X,\oldvec{P}X)$, $\oldvec{P}X=X^{\oldvec{I}}$.

Geometric realization

The geometric realization of a precubical set $Q$ is the d-space $\mathopen{|}Q\mathclose{|}=\bigsqcup_{n\geq 0}Q_{n}\times\oldvec{I}^{n}/\mathord{\sim}$, where the equivalence relation $\sim$ is generated by

[TABLE]

(Technically, this requires us to define disjoint unions and quotients of d-spaces, but there is nothing surprising about these definitions, see [Fah05b].)

Geometric realization is naturally extended to morphisms of precubical sets: if $f:Q\to R$ is a precubical morphism, then $|f|:|Q|\to|R|$ is the directed map given by $|f|(q,(u_{1},\dotsc,u_{n}))=(f(q),(u_{1},\dotsc,u_{n}))$. Geometric realization then becomes a functor from the category of precubical sets to the category of d-spaces.

Euclidean Precubical Sets

Intuitively, a precubical set is Euclidean if its geometric realization can be embedded into a hypercube lattice in some $\smash{\oldvec{\mathbbm{R}}^{d}}$. We make this precise below.

{defi}

A non-selflinked precubical set $Q$ with $\dim Q=d<\infty$ is a grid if there exist $M_{1},\dotsc,M_{d}\in\mathbbm{N}$ and a bijection $\Phi:\{1,\dotsc,M_{1}\}\times\dotsm\times\{1,\dotsc,M_{d}\}\to Q_{d}$, such that for all $k\in\{1,\dotsc,d\}$ and all $(i_{1},\dotsc,i_{d})\in\{1,\dotsc,M_{1}\}\times\dotsm\times\{1,\dotsc,M_{k-1}\}\times\{1,\dotsc,M_{k}-1\}\times\{1,\dotsc,M_{k+1}\}\times\dotsm\times\{1,\dotsc,M_{d}\}$,

[TABLE]

and there are no other face relations between cubes in $Q$.

Hence a grid is a product444Technically, a tensor product, see [Fah05b]. of long intervals: one-dimensional precubical sets with $1$-cells $1,\dotsc,M_{j}$ which are connected such that the upper face of $M_{i}$ is the lower face of $M_{i+1}$ for all $i=1,\dotsc,j-1$. Figure 12 shows an example of a two-dimensional grid with $M_{1}=4$ and $M_{2}=2$. The geometric realization of a grid is a subdivided cube: it can be embedded into $\smash{\oldvec{\mathbbm{R}}^{d}}$ as the product of intervals $[0,M_{1}]\times\dotsm\times[0,M_{d}]$.

{defi}

A precubical set $Q$ is Euclidean if there exists a grid $G$ and an embedding $Q\hookrightarrow G$.

Intuitively, these are precisely the “geometric sculptures” referred to in the introduction: subcomplexes of subdivided cubes. The next theorem shows that geometric sculptures and combinatorial sculptures are the same.

Theorem 31**.**

A precubical set can be sculpted iff it is Euclidean.

Proof 5.1**.**

First off, any bulk is a grid, hence any sculpture can be embedded into a grid. For the reverse direction, it suffices to show that any grid is a sculpture.

Consider a grid of dimension $d$ with $M_{1},\dots,M_{d}$ as the number of grid positions in any dimension. We develop a naming scheme using Chu-style labels as in the canonical naming of bulks from Section 3. We use the following list of events: $(e_{1}^{1},\dots,e_{1}^{M_{1}},e_{2}^{1},\dots,e_{2}^{M_{2}},\dots,$ $e_{d}^{1},\dots,e_{d}^{M_{d}})$ and to each event we give values from $\{0,\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}},1\}$. The tuples have dimension $m=\sum_{1\leq i\leq d}M_{i}$. Construct the bulk $\mathbf{B}^{m}$ of dimension $m$ using the canonical naming starting with the m-tuple of the events ordered as above containing only values. Each $d$-cell of $X_{d}$ is identified by one of the grid cells (i.e., the bijection of the grid) as a $d$-tuple of indices $(i_{1},\dots,i_{d})$ to which we give an $m$-tuple label constructed as follows:

[TABLE]

for $1\leq k\leq d$.

We then label all the faces of each $d$-cell with the canonical naming starting from the above. This face labeling is consistent with the face equality restrictions (3) of the grid. Indeed, take two $d$-cells of the grid that have faces equated, i.e., pick two $d$-tuples differing in only one index $(\dots,i_{k},\dots)$ and $(\dots,i_{k}+1,\dots)$ which are named by the $m$-tuples $(\dots,1,e_{k}^{i_{k}}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}},0,\dots)$ respectively $(\dots,1,1,e_{k}^{i_{k}+1}=\raisebox{1.0pt}{ \leavevmode\hbox to7.29pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{} {}{{}}{} {}{} {}{} {}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{3.44443pt}{0.0pt}\pgfsys@lineto{3.44443pt}{4.30554pt}\pgfsys@lineto{6.88885pt}{4.30554pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}},\dots)$ called $q_{d}^{i_{k}}$ respectively $q_{d}^{i_{k}+1}$. The face maps are named as: $t_{k}(q_{d}^{i_{k}})=(\dots,1,e_{k}^{i_{k}}=1,0,\dots)$ and $s_{k}(q_{d}^{i_{k}+1})=(\dots,1,1,e_{k}^{i_{k}+1}=0,\dots)$ which are the same, thus the equality (3) is respected.

Using the above naming, it is easy to construct an embedding from the grid $(M_{1},\dots,M_{d})$ into the bulk $\mathbf{B}^{m}$: it maps each cell of the grid named by some m-tuple into the cell from the bulk that has the same name. All the cells are uniquely named in the grid, and thus the mapping is correctly defined.

6. Conclusion

Using a precise definition of sculptures as higher-dimensional automata (HDA), we have shown that sculptures are isomorphic to regular ST-structures and also to regular Chu spaces. This nicely captures Pratt’s event-state duality [Pra92]. We have also shown that sculptures are isomorphic to Euclidean cubical complexes, providing a link between geometric and combinatorial approaches to concurrency.

We have made several claims in the introduction about HDA that can or cannot be sculpted. We sum these up in the next theorem; detailed proofs are in Appendix B.

Theorem 32**.**

1. (1)

There are acyclic HDA which cannot be sculpted. 2. (2)

There is an HDA which cannot be sculpted, but whose unfolding can be sculpted. 3. (3)

There is an HDA which can be sculpted, but whose unfolding cannot be sculpted. 4. (4)

There is an HDA which can be sculpted and whose unfolding can be sculpted. 5. (5)

There is an HDA which cannot be sculpted and whose unfolding cannot be sculpted.

The HDA from Figs. 2 (right) and 5 are acyclic but cannot be sculpted. It is enough to apply the minimal equivalence of the decision algorithm to obtain two cells with the same ST-label, cf. Lemma 28. This proves part (1) of the theorem.

Both these examples are also their own unfoldings, which proves part (5). Part (2) is proven by the triangle in Figure 4, which cannot be sculpted due to Lemma 27. For part (4) we can use the triangle’s unfolding and the fact that this is its own unfolding. Part (3) is proven by Figure 2. Finally, also the one-dimensional HDA from Figure 8 cannot be sculpted. There are several interleaving squares (Lemma 29), so the algorithm has to identify all transitions labeled $a$, which leads to a contradiction à la Lemma 28.

Acknowledgements

The authors are grateful to Lisbeth Fajstrup, Samuel Mimram and Emmanuel Haucourt for multiple fruitful discussions on the subject of this paper, and to Martin Steffen and Olaf Owe for help with an early version of this paper.

Appendix A Ordered precubical sets

Fix a consistent precubical set $Q$ and an order $\mathrel{\overset{\mathsf{ev}}{<}}$ on the set $\mathit{UE}(Q)$ of universal labels of $Q$. For every $n>0$ and every $n$–cell $q\in Q_{n}$ let $\sigma(q):\{1,\dotsc,n\}\to\{1,\dotsc,n\}$ be the unique permutation such that

[TABLE]

Let $Q^{\prime}$ be a precubical set that has the same cells as $Q$, i.e., $Q^{\prime}_{n}=Q_{n}$ for all $n\geq 0$, and face maps given by

[TABLE]

It remains to check that the face maps $s^{\prime}_{i}$ and $t^{\prime}_{i}$ satisfy the precubical relations.

Define functions $\mathsf{d}_{i}:\{1,\dotsc,n-1\}\to\{1,\dotsc,n\}$:

[TABLE]

Lemma 33**.**

Let $Q_{n}$, $n\geq 0$ be a family of sets and for every $n$ let $s_{i},t_{i}:Q_{n}\to Q_{n-1}$, $i\in\{1,\dotsc,n\}$ be maps. The following conditions are equivalent:

• •

The maps $s_{i},t_{i}$ satisfy the precubical relations (i.e., $Q_{n}$ with the maps $s_{i},t_{i}$ form a precubical set);

• •

$\alpha_{i}\beta_{j}=\beta_{k}\alpha_{l}$* for $\alpha,\beta\in\{s,t\}$ and all integers $i,j,k,l$ such that $\{\mathsf{d}_{j}(i),j\}=\{\mathsf{d}_{l}(k),l\}$.*

Proof A.1**.**

The latter condition is satisfied only when $(i,j,k,l)=(i,j,i,j)$ (for any $i,j$) or when $(i,j,k,l)=(i,j,j-1,i)\mbox{ or }(j-1,i,i,j)$ (for $i<j$).

Lemma 34**.**

For $q\in Q_{n}$, $\alpha\in\{s,t\}$ and $k\in\{1,\dotsc,n\}$

[TABLE]

Proof A.2**.**

Both maps have the same image $\{1,\dotsc,n\}\setminus\{\sigma(q)(k)\}$ so it is enough to show that they both are increasing. The compositions of both sides with $\lambda(q)$, which when seen as a function from $\{1\dots n\}\to\mathit{UE}(Q)$, it is increasing, are

[TABLE]

and

[TABLE]

They are increasing since $\lambda(x)\circ\sigma(x)$ is increasing for all $x$. The equation above follows from Lemma 1.(1).

Lemma 35**.**

The maps $s^{\prime}_{i}$ and $t^{\prime}_{i}$ satisfy the precubical relations.

Proof A.3**.**

We will use the criterion in Lemma 33. Choose $i,j,k,l$ such that $(\mathsf{d}_{j}(i),j)=(l,\mathsf{d}_{l}(k))$. We have

[TABLE]

and

[TABLE]

Since (Lemma 34)

[TABLE]

and

[TABLE]

the conclusion follows.

Appendix B Proofs for Sec. 6

Proof B.1** (Proof of Theorem 32).**

The two first examples of the theorem are 2-dimensional HDAs which are also their own history unfoldings.

To show that the broken box cannot be sculpted (refer to Figure 14 for annotations) we apply the labeling strategy described in Section 4. First we apply the unfolding procedure $\mathsf{ST}_{\pi}$ and for the two problematic corner states $q_{0}^{1}$ and $q_{0}^{2}$ we obtain the following ST-configurations $\mathsf{ST}_{\pi}(\pi_{1})=(\{q_{1}^{1},q_{1}^{4}\},\{q_{1}^{1},q_{1}^{4}\})$ respectively $\mathsf{ST}_{\pi}(\pi_{2})=(\{q_{1}^{2},q_{1}^{3}\},\{q_{1}^{2},q_{1}^{3}\})$, where $\pi_{1}$ is the lower rooted path ending in $q_{0}^{1}$ and $\pi_{2}$ is the other lower path ending in $q_{0}^{2}$.

The second step is to apply the minimal equivalence $\stackrel{{\scriptstyle\mathsf{ev}}}{{\sim}}$, since this is required for any HDA. Applying $\stackrel{{\scriptstyle\mathsf{ev}}}{{\sim}}$ on our example equates $q_{1}^{1}\stackrel{{\scriptstyle\mathsf{ev}}}{{\sim}}q_{1}^{3}$ because of the three squares: front, top, back, which share horizontal faces. (Transitivity of the equivalence was applied.) The same argument equates $q_{1}^{2}\stackrel{{\scriptstyle\mathsf{ev}}}{{\sim}}q_{1}^{4}$, this time going through the squares left-side, top, right-side.

We now see that through $\rho_{\stackrel{{\scriptstyle\mathsf{ev}}}{{\sim}}}$ we have labeled both $q_{0}^{1}$ and $q_{0}^{2}$ with the same label $(\{[q_{1}^{2}],[q_{1}^{3}]\},\{[q_{1}^{2}],[q_{1}^{3}]\})$, made of equivalence classes. However, for a sculpture we cannot have two cells labeled the same.

Showing that the example of Fig. 5 is similar and is enough to look at the transitions labeled with $d$. After applying the minimal equivalence the first two lower states where the lower $d$-transitions (call these $q_{1}^{1}$ and $q_{1}^{2}$) end are labeled with $([q_{1}^{1}],[q_{1}^{1}])$ and $([q_{1}^{2}],[q_{1}^{2}])$. But these are equated by the minimal equivalence due to the two squares that share the upper $d$-transition.

The example from Fig. 8 is a one-dimensional acyclic HDA that cannot be sculpted (refer to Figure 14 for annotations used in this argument), which also shows that no two-dimensional structure is needed for things to turn problematic: already in dimension $1$ there are acyclic HDA which cannot be sculpted. Our algorithm detects this without using the minimal equivalence $\stackrel{{\scriptstyle\mathsf{ev}}}{{\sim}}$, because this is not applicable for this example. However, there are several homotopy pairs of length 2, i.e., called interleaving squares. Each interleaving square forces the equating of their parallel transitions. In this example, the horisontal transitions of the inner interleaving square, as well as the two ones (upper and lower) connected to it equate the four transition cells that we named $b^{1}\sim b^{2}\sim b^{3}\sim b^{4}$. Similarly, we must equate the vertical transitions of the inner interleaving square, and the two (left and right) connected to it, making $c^{1}\sim c^{2}\sim c^{3}\sim c^{4}$. Now the four outer interleaving squares that we already treated the $b$ and $c$ transitions have in common the parallel transitions labeled by $a^{1}\sim a^{2}\sim a^{3}\sim a^{4}\sim a^{5}$. This necessary equivalence makes the two states connected with a dashed line to be identified because they now receive the same ST-configuration as label $(\{[a^{1}],[b^{1}],[c^{1}]\},\{[a^{1}],[b^{1}],[c^{1}]\})$, which cannot be. Moreover, there is no backtracking possible because for the interleaving squares there is only one possible way to equate their transitions; unlike for longer homotopy pairs where we can try several possible equating alternatives, as it was the case in Example 4 with Figure 11.