Labeled homology of higher-dimensional automata

TL;DR

This paper introduces labeled homology for higher-dimensional automata, providing a new algebraic tool that respects automata transformations and has potential applications in concurrency theory.

Contribution

It constructs labeling homomorphisms on cubical homology of HDAs, demonstrating their naturality and compatibility, and suggests applications in concurrency analysis.

Findings

Labeled homology is compatible with cubical dimaps.

Homology respects tensor product of HDAs.

Potential applications in concurrency theory.

Abstract

We construct labeling homomorphisms on the cubical homology of higher-dimensional automata and show that they are natural with respect to cubical dimaps and compatible with the tensor product of HDAs. We also indicate two possible applications of labeled homology in concurrency theory.

Equations

$${\ell }_{\mathcal{A}}={\ell }_{\mathcal{A}}^n:H_n(\mathcal{A})\to \Lambda (\Sigma )(n\ge 0).$$

$${\ell }_{\mathcal{A}}({\alpha }_i)={\mathtt{b}}_{\mathtt{i}}{:=}_{\mathtt{i}}1+\mathtt{t}{:=}_{\mathtt{i}}(1-\mathtt{i})+\mathtt{cri}{\mathtt{t}}_{\mathtt{i}}+{\mathtt{b}}_{\mathtt{i}}{:=}_{\mathtt{i}}0.$$

$$(P\otimes Q{)}_n=\coprod _{p+q=n}{P}_p\times Q_q$$

$$d_{i}^{k}(x,y)=\left\{\begin{array}[]{ll}(d_{i}^{k}x,y),&1\leq i\leq{\rm{deg}}(x),\\ (x,d_{i-{\rm{deg}}(x)}^{k}y),&{\rm{deg}}(x)+1\leq i\leq{\rm{deg}}(x)+{\rm{deg}}(y).\end{array}\right.$$

$$|P|=\left(\coprod _{n\ge 0}{P}_n\times [0,1{]}^n\right)/\sim$$

$$(d_i^{k}x,u)\sim (x,{\delta }_i^k(u)),x\in P_{n+1},u\in [0,1{]}^n,i\in \{1,\dots ,n+1\},k\in \{0,1\}.$$

$${\delta }_i^k(u_1,\dots ,u_n)=(u_1,\dots ,u_{i-1},k,u_i,\dots ,u_n).$$

$${\psi }_{P,Q}([(x,y),(u_1,\dots ,u_{\mathrm{deg}(x)+\mathrm{deg}(y)})])$$

$$=([x,(u_1,\dots ,u_{\mathrm{deg}(x)})],[y,(u_{\mathrm{deg}(x)+1},\dots u_{\mathrm{deg}(x)+\mathrm{deg}(y)}]).$$

$$\mathcal{A}=(P_{\mathcal{A}},I_{\mathcal{A}},F_{\mathcal{A}},{\lambda }_{\mathcal{A}})$$

$${\overline{\lambda }}_{\mathcal{A}}(\omega )={\lambda }_{\mathcal{A}}(x_1)\cdot \cdots \cdot {\lambda }_{\mathcal{A}}(x_k);$$

$$dx=\sum _{i=1}^n(-1{)}^i(d_i^{0}x-d_i^{1}x),x\in P_n.$$

$$\mathsf{sing}(x)=|x_{♯}|+D_{\ast }(S|P|),x\in P.$$

$$C_n^{CW}(X)=H_n(X_n,X_{n-1}),$$

$$H_n(X_n,X_{n-1})\stackrel{{\partial }_{\ast }}{\to }{H}_{n-1}(X_{n-1})\to H_{n-1}(X_{n-1},X_{n-2})$$

$$\mathsf{cell}(x)=[|x_{♯}|],x\in P_n$$

$$C_n(P)\to (C_{\ast }(P_{\le n})/C_{\ast }(P_{<n}){)}_n\to H_n(P_{\le n},P_{<n}).$$

$${\mathsf{sing}}_{\ast }:H_n(P_{\le n},P_{<n})\to H_n(|P_{\le n}|,|P_{<n}|),$$

$$C_n(P)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\lambda }_{\mathcal{A}}(\chi (j_1,\dots ,j_{s-1},[j_s,j_s+1],j_{s+1},\dots ,j_n))={\lambda }_{\mathcal{A}}(\chi (0,\dots ,0,[j_s,j_s+1],0,\dots ,0)).$$

$$j^{\prime}_{i}=\left\{\begin{array}[]{ll}j_{i},&i\not=t,\\ j_{t}-1,&i=t.\end{array}\right.$$

$$b_{i}=\left\{\begin{array}[]{ll}\left[j_{s},j_{s}+1\right],&i=s,\\ \left[j_{t}-1,j_{t}\right],&i=t,\\ j_{i},&i\not=s,t.\end{array}\right.$$

$$q=\left\{\begin{array}[]{ll}1,&s>t,\\ 2,&s<t.\end{array}\right.$$

$${\lambda }_{\mathcal{A}}(\chi (j_1,\dots ,j_{s-1},[j_s,j_s+1],j_{s+1},\dots ,j_n))$$

$$={\lambda }_{\mathcal{A}}(\chi (d_q^{1}b))$$

$$={\lambda }_{\mathcal{A}}(d_q^1\chi (b))$$

$$={\lambda }_{\mathcal{A}}(d_q^0\chi (b))$$

$$={\lambda }_{\mathcal{A}}(\chi (d_q^{0}b))$$

$$={\lambda }_{\mathcal{A}}(\chi (j_1^{\prime },\dots ,j_{s-1}^{\prime },[j_s,j_s+1],j_{s+1}^{\prime },\dots ,j_n^{\prime }))$$

$$={\lambda }_{\mathcal{A}}(\chi (0,\dots ,0,[j_s,j_s+1],0,\dots ,0)).\text{qed}$$

$$e^{k}_{i}x=\left\{\begin{array}[]{ll}x,&n=1,\\ d_{1}^{1-k}\cdots d_{i-1}^{1-k}d_{i+1}^{1-k}\cdots d_{n}^{1-k}x,&n>1.\end{array}\right.$$

$${\mathfrak{l}}_{\mathcal{A}}^n:C_{\ast }(\mathcal{A})\to \Lambda (\Sigma )$$

$$\mathfrak{l}_{{\mathcal{A}}}^{n}(x)=\left\{\begin{array}[]{ll}1,&n=0,\vspace{0.2cm}\\ \sum\limits_{j_{1}=1}^{|\lambda_{{\mathcal{A}}}(e^{0}_{1}x)|}\dots\sum\limits_{j_{n}=1}^{|\lambda_{{\mathcal{A}}}(e^{0}_{n}x)|}\lambda_{{\mathcal{A}}}(e^{0}_{1}x)_{j_{1}}\wedge\dots\wedge\lambda_{{\mathcal{A}}}(e^{0}_{n}x)_{j_{n}},&n>0.\end{array}\right.$$

$${\mathfrak{l}}_{\mathcal{A}}^n(x)={\mathfrak{l}}_{\mathcal{A}}^1(e_1^{0}x)\wedge \cdots \wedge {\mathfrak{l}}_{\mathcal{A}}^1(e_n^{0}x)={\mathfrak{l}}_{\mathcal{A}}^1(e_1^{1}x)\wedge \cdots \wedge {\mathfrak{l}}_{\mathcal{A}}^1(e_n^{1}x).$$

Full text

This research was financed by Portuguese funds through FCT - Fundação para a Ciência e a Tecnologia (project UID/MAT/00013/2013).

1. Introduction

1.1. Higher-dimensional automata

Higher-dimensional automata provide a powerful model for concurrent systems. A higher-dimensional automaton (HDA) over a monoid $M$ is a precubical set (i.e., a cubical set without degeneracies) with initial and final states and with 1-cubes labeled by elements of $M$ such that opposite edges of 2-cubes have the same label. The vertices of an HDA represent the states of a concurrent system, the labeled edges model the actions of the system, and a cube of dimension $\geq 2$ indicates that the actions starting at its origin are independent in the sense that they may be executed in any order, or even simultaneously, without any observable difference. The concept of higher-dimensional automaton goes back to Pratt [Pra91]. The notion defined here is essentially the one introduced by van Glabbeek (see [vG06]).

Let us consider the example of Peterson’s algorithm [Pet81] to indicate in more detail how HDAs can be used to model concurrent systems. Peterson’s algorithm is a protocol designed to give two processes fair and mutually exclusive access to a shared resource. The algorithm is based on three shared variables, namely the boolean variables $\mathtt{b_{0}}$ and $\mathtt{b_{1}}$ and the turn variable $\mathtt{t}$, whose possible values are the process IDs—let us assume that these are [math] and $1$. Process $i$ has four local states and moves from one to the next by executing the following actions: It first sets variable $\mathtt{b_{i}}$ to $1$ in order to indicate that it intends to enter the “critical section” and access the shared resource. Then it gives priority to the other process by setting the turn variable $\mathtt{t}$ to $1-i$. After this, it waits until the other process does not intend to enter the critical section or it is its own turn to do so. When this “guard condition” is satisfied, the process enters the critical section and accesses the shared resource. This action has no effect on the shared variables $\mathtt{b_{0}}$, $\mathtt{b_{1}}$, and $\mathtt{t}$. After having used the shared resource, process $i$ leaves the critical section and sets variable $\mathtt{b_{i}}$ to [math] again. The procedure is now repeated arbitrarily often or forever.

An HDA model of the reachable part of the system given by Peterson’s algorithm is depicted in Figure 1. The vertices of the HDA correspond to the reachable global states of the system, which are quintuples whose components are local states of the processes and values of the variables. The HDA has two states, marked with a small incoming arrow and a double circle in Figure 1, that are at the same time initial and final states. In the upper initial and final state, $\mathtt{t}=0$; in the lower one, $\mathtt{t}=1$. The boolean variables $\mathtt{b_{0}}$ and $\mathtt{b_{1}}$ are [math] in both of these states, and each process is in its initial local state. The directed edges starting in a given vertex represent the actions of the processes that are enabled in the corresponding global state. These actions are indicated in the transition labels, indexed by the respective process IDs. The monoid of labels is the free monoid generated by the transition labels. The squares are introduced in order to indicate independence of actions: two actions are independent in a state where both are enabled if they can be executed one after the other in either order and the two sequential executions of the actions lead to the same state. In general, an HDA may also contain higher-dimensional cubes in order to indicate the independence of more than two actions. A more formal description of the construction of HDA models for shared-variable systems can be found in [Kah18].

1.2. Labeled homology

As demonstrated in the literature, concepts and methods from algebraic topology may be employed profitably in concurrency theory (see e.g. [FRG06, FGH*+*16]). The purpose of this paper is to introduce labeled homology of HDAs and to establish results about it that enable one to use the information contained in the homology of HDAs in the analysis of concurrent systems.

We focus on HDAs over the free monoid on an alphabet $\Sigma$. Given such an HDA ${\mathcal{A}}$, we consider its cubical homology and the exterior algebra $\Lambda(\Sigma)$ and show that the labeling function of ${\mathcal{A}}$ induces labeling homomorphisms

[TABLE]

The labeled homology of an HDA is its homology together with the sequence of labeling homomorphisms.

Let us describe the labeled homology of the HDA ${\mathcal{A}}$ modeling the system given by Peterson’s algorithm. The integral homology of ${\mathcal{A}}$ is given by $H_{0}({\mathcal{A}})\cong{\mathbb{Z}}$, $H_{1}({\mathcal{A}})\cong{\mathbb{Z}}^{5}$, and $H_{\geq 2}({\mathcal{A}})=0$. The labeling homomorphism in degree 0 is the obvious monomorphism $H_{0}({\mathcal{A}})\to\Lambda(\Sigma)$, and so the only actually interesting dimension is 1. If, as in ${\mathcal{A}}$, the edge labels of an HDA are indecomposable, the label of a $1\mbox{-}$dimensional homology class is simply the linear combination of labels corresponding to the linear combination of edges in a representing cycle of the class. Hence the labels of the two generators $\alpha_{0}$ and $\alpha_{1}$ of $H_{1}({\mathcal{A}})$ depicted in green in Figure 1 are given by

[TABLE]

The classes $\alpha_{0}$ and $\alpha_{1}$ represent the two processes, executing alone. A third generator of $H_{1}({\mathcal{A}})$, depicted in red in Figure 1, has label $\ell_{{\mathcal{A}}}(\alpha_{0})+\ell_{{\mathcal{A}}}(\alpha_{1})$ and corresponds to an execution where the two processes alternately access the shared resource. Finally, $H_{1}({\mathcal{A}})$ has two generators with zero label, which are represented by the thick multicolored cycles in Figure 1 and reflect the synchronization (coordination) of the processes enforced by the guard condition that must be satisfied before a process enters the critical section: The existence of, say, the left of these homology classes is due the fact that process 1 is blocked in the upper right state of the inner hole of ${\mathcal{A}}$. If process 1 was allowed to enter the critical section in this state, the class would disappear—and the system would lose the important property of starvation freedom as it would become possible that process 0 requests access to the critical section without ever obtaining it.

The example of Peterson’s algorithm shows that the homology of an HDA has meaning from a computer science point of view. The labeling homomorphisms help to interpret the information contained in the homology of HDAs. We introduce labeled homology in Section 4. The earlier sections contain preparatory material on precubical sets and HDAs (Section 2) and cubical chains and homology (Section 3).

1.3. Tensor-product HDAs

An important property of labeled homology is that it is compatible with the tensor product of HDAs, which models the interleaving parallel composition of independent concurrent systems. If two completely independent and disjoint concurrent systems are combined into one, then an HDA model of this interleaving parallel composition of the systems is given by the tensor product of the HDA models of the two systems (see [Kah18]). In Section 5 we establish a cross product formula for the computation of the labeling homomorphisms of a tensor-product HDA from those of its factors.

A concurrent system will, of course, normally not be the interleaving of other systems. It is, however, frequently the case that a concurrent system contains subsystems that are independent from each other. Labeled homology and, in particular, our result on the labeled homology of tensor-product HDAs can be used to aid the analysis of the independence structure of concurrent systems. This will be discussed in Section 8.1.

1.4. Cubical dimaps

In Section 7 we show that labeled homology is natural with respect not only to morphisms of HDAs but also to cubical dimaps. Roughly speaking, a cubical dimap from an HDA to another one is a label-preserving continuous map between the geometric realizations that also is a directed map—or dimap—in the sense that it respects the directed topology of the geometric realization. Cubical dimaps permit one to compare HDAs that model concurrent systems at different abstraction levels and do not admit ordinary morphisms between them. For instance, although the HDA in Figure 1 and the homotopy equivalent smaller one depicted in Figure 2 both model the system given by Peterson’s algorithm (cf. [Kah16, 7.2]), there do not exist any morphisms from one to the other. The two HDAs may, however, be related by a cubical dimap. Cubical dimaps are the subject of Section 6.

The naturality of labeled homology implies that it is invariant under cubical dimaps that are homotopy equivalences. Therefore labeled homology can be considered a directed homotopy invariant of HDAs. Since it does not only depend on the directed topology of the underlying precubical sets, it is, however, not a concept of directed homology as those considered, for instance, in [DGGL16, Fah04, Gau05, GJ92, Gra09, Kah14a, Kri14].

As a possible application of labeled homology, based on its naturality, we discuss in Section 8.2 a necessary condition for an HDA to implement a specification that is given by another HDA.

2. Precubical sets and HDAs

This section presents some fundamental concepts and facts about precubical sets and higher-dimensional automata. The material is mostly taken from [Kah14b].

2.1. Precubical sets

A precubical set is a graded set $P=(P_{n})_{n\geq 0}$ with boundary or face operators $d^{k}_{i}\colon P_{n}\to P_{n-1}$ $(n>0,\;k=0,1,\;i=1,\dots,n)$ satisfying the relations $d^{k}_{i}\circ d^{l}_{j}=d^{l}_{j-1}\circ d^{k}_{i}$ $(k,l=0,1,\;i<j)$. If $x\in P_{n}$, we say that $x$ is of degree or dimension $n$ and write ${\rm{deg}}(x)=n$. The elements of degree $n$ are called the $n$-cubes of $P$. The elements of degree [math] are also called the vertices of $P$, and the $1$-cubes are also called the edges of $P$. Given an $n$-cube $x$, we say that the vertex $\underbracket{d_{1}^{0}\cdots d_{1}^{0}}_{n\;\text{times}}x$ is its initial vertex and that $d_{1}^{1}\cdots d_{1}^{1}x$ is its final vertex. We say that a face $d^{k}_{i}x$ of a cube $x$ is a front (back) face of $x$ if $k=0$ $(k=1)$. A morphism of precubical sets is a morphism of graded sets that is compatible with the boundary operators. A precubical subset of a precubical set $P$ is a graded subset of $P$ that is stable under the boundary operators.

2.2. Intervals

Let $k$ and $l$ be two integers such that $k\leq l$. The precubical interval $\llbracket k,l\rrbracket$ is the precubical set defined by $\llbracket k,l\rrbracket_{0}=\{k,\dots,l\}$, $\llbracket k,l\rrbracket_{1}=\{{[k,k+1]},\dots,{[l-1,l]}\}$, $d_{1}^{0}[j-1,j]=j-1$, $d_{1}^{1}[j-1,j]=j$, and $\llbracket k,l\rrbracket_{\geq 2}=\emptyset$.

2.3. Tensor product

The category of precubical sets is a monoidal category. Given two precubical sets $P$ and $Q$, the tensor product $P\otimes Q$ is defined by

[TABLE]

and

[TABLE]

The $n$-fold tensor product of a precubical set $P$ is denoted by $P^{\otimes n}$. Here we use the convention $P^{\otimes 0}=\llbracket 0,0\rrbracket=\{0\}$.

2.4. Precubical cubes

The precubical $n\mbox{-}$cube is the $n$-fold tensor product ${\llbracket 0,1\rrbracket^{\otimes n}}$. The only element of degree $n$ in $\llbracket 0,1\rrbracket^{\otimes n}$ will be denoted by $\iota_{n}$. We thus have $\iota_{0}=0$ and $\iota_{n}=(\underbracket{[0,1],\dots,[0,1]}_{n\;{\text{times}}})$ for $n>0$. Given an element $x$ of degree $n$ of a precubical set $P$, there exists a unique morphism of precubical sets $\llbracket 0,1\rrbracket^{\otimes n}\to P$ that sends $\iota_{n}$ to $x$. This morphism will be denoted by $x_{\sharp}$.

2.5. Paths

A path of length $k$ in a precubical set $P$ is a morphism of precubical sets $\omega\colon\llbracket 0,k\rrbracket\to P$. If $\omega(0)=\omega(k)$, we say that $\omega$ is a loop. The set of paths in $P$ is denoted by $P^{\mathbb{I}}$. The concatenation $\omega\cdot\nu$ of two paths $\omega\colon\llbracket 0,k\rrbracket\to P$ and $\nu\colon\llbracket 0,l\rrbracket\to P$ with $\omega(k)=\nu(0)$ is defined in the obvious way. Note that for any path $\omega\in P^{\mathbb{I}}$ of length $k\geq 1$, there exists a unique sequence $(x_{1},\dots,x_{k})$ of elements of $P_{1}$ such that $d_{1}^{0}x_{j+1}=d_{1}^{1}x_{j}$ for all $1\leq j<k$ and $\omega=x_{1\sharp}\cdot\,\cdots\,\cdot x_{k\sharp}$.

2.6. Geometric realization

The geometric realization of a precubical set $P$ is the quotient space

[TABLE]

where the sets $P_{n}$ are given the discrete topology and the equivalence relation is given by

[TABLE]

Here the continuous maps $\delta_{i}^{k}\colon[0,1]^{n}\to[0,1]^{n+1}$ are defined by

[TABLE]

The geometric realization of a morphism of precubical sets $f\colon P\to Q$ is the continuous map $|f|\colon|P|\to|Q|$ given by $|f|([x,u])=[f(x),u]$.

The geometric realization of a precubical set $P$ is a CW complex. The $n$-skeleton of $|P|$ is the geometric realization of the precubical subset $P_{\leq n}$ of $P$ defined by $(P_{\leq n})_{m}=P_{m}$ $(m\leq n)$ and $(P_{\leq n})_{m}=\emptyset$ $(m>n)$. As a CW complex, the geometric realization of a precubical set is a compactly generated Hausdorff space. All spaces in this paper are compactly generated Hausdorff spaces, and constructions such as products are performed in the category of these spaces.

The geometric realization is a comonoidal functor with respect to the natural continuous map ${\psi_{P,Q}\colon|P\otimes Q|\to|P|\times|Q|}$ given by

[TABLE]

Since we are working in the category of compactly generated Hausdorff spaces, the map $\psi_{P,Q}$ is a homeomorphism, even a cellular isomorphism, and we may use it to identify the spaces $|P\otimes Q|$ and $|P|\times|Q|$.

The geometric realization of the precubical interval $\llbracket k,l\rrbracket$ will be identified with the closed interval $[k,l]$ by means of the homeomorphism $|\llbracket k,l\rrbracket|\to[k,l]$ given by $[j,()]\mapsto j$ and $[[j-1,j],t]\mapsto j-1+t$.

2.7. Singular precubical sets

The singular precubical set of a space $X$ is the precubical set $SX$ where the $n$-cubes are the continuous maps $\sigma\colon[0,1]^{n}\to X$ and the boundary operators are given by $d_{i}^{k}\sigma=\sigma\circ\delta_{i}^{k}$. The singular precubical set is functorial in the obvious way, and the functor $S$ is right adjoint to the geometric realization.

2.8. Higher-dimensional automata

Let $M$ be a monoid. A higher-dimensional automaton over $M$ (abbreviated $M\mbox{-}$HDA or simply HDA) is a tuple

[TABLE]

where $P_{{\mathcal{A}}}$ is a precubical set, $I_{{\mathcal{A}}}\subseteq(P_{{\mathcal{A}}})_{0}$ is a set of initial states, $F_{{\mathcal{A}}}\subseteq(P_{{\mathcal{A}}})_{0}$ is a set of final or accepting states, and $\lambda\colon(P_{{\mathcal{A}}})_{1}\to M$ is a map, called the labeling function, such that $\lambda_{{\mathcal{A}}}(d_{i}^{0}x)=\lambda_{{\mathcal{A}}}(d_{i}^{1}x)$ for all $x\in(P_{{\mathcal{A}}})_{2}$ and $i\in\{1,2\}$ (cf. [vG06, Kah14b]). We shall abuse notation and write ${\mathcal{A}}$ instead of $P_{{\mathcal{A}}}$. A morphism from an $M\mbox{-}$HDA ${\mathcal{B}}$ to an $M\mbox{-}$HDA ${\mathcal{A}}$ is a morphism of precubical sets $f\colon{\mathcal{B}}\to{\mathcal{A}}$ such that $f(I_{{\mathcal{B}}})\subseteq I_{{\mathcal{A}}}$, $f(F_{{\mathcal{B}}})\subseteq F_{{\mathcal{A}}}$, and $\lambda_{{\mathcal{A}}}(f(x))=\lambda_{{\mathcal{B}}}(x)$ for all $x\in{\mathcal{B}}_{1}$. An $M$-HDA ${\mathcal{B}}$ is a subautomaton of an $M$-HDA ${\mathcal{A}}$ if ${\mathcal{B}}$ is a precubical subset of ${\mathcal{A}}$, $I_{{\mathcal{B}}}\subseteq I_{{\mathcal{A}}}$, $F_{{\mathcal{B}}}\subseteq F_{{\mathcal{A}}}$, and $\lambda_{{\mathcal{B}}}(x)=\lambda_{{\mathcal{A}}}(x)$ for all $x\in{{\mathcal{B}}_{1}}$.

2.9. Extended labeling function

The extended labeling function of an $M\mbox{-}$HDA ${\mathcal{A}}$ is the map $\overline{\lambda}_{{\mathcal{A}}}\colon{\mathcal{A}}^{\mathbb{I}}\to M$ defined as follows: If $\omega=x_{1\sharp}\cdot\,\cdots\,\cdot x_{k\sharp}$ for a sequence $(x_{1},\dots,x_{k})$ of elements of ${\mathcal{A}}_{1}$ such that $d_{1}^{0}x_{j+1}=d_{1}^{1}x_{j}$ $(1\leq j<k)$, then we set

[TABLE]

if $\omega$ is a path of length [math], then we set $\overline{\lambda}_{{\mathcal{A}}}(\omega)=1$.

3. The cubical chain complex of a precubical set

Throughout this article we work over a fixed principal ideal domain $R$. In order to simplify the presentation, we will usually suppress the ring $R$ from the notation. All graded modules are ${\mathbb{Z}}$-graded, and we adopt the usual convention $V^{i}=V_{-i}$.

In this section we define the cubical chain complex and the cubical homology and cohomology of a precubical set and relate cubical chains to singular and cellular chains.

3.1. Cubical (co)chains and (co)homology

Let $P$ be a precubical set. The cubical chain complex of $P$ is the nonnegative chain complex $C_{*}(P)$ where $C_{n}(P)$ is the free module generated by $P_{n}$ and the boundary operator $d\colon C_{n}(P)\to C_{n-1}(P)$ is given by

[TABLE]

It is clear that the cubical chain complex is functorial. The cubical homology of $P$, denoted by $H_{*}(P)$, is the homology of $C_{*}(P)$.

Given a module $G$, we view it as a chain complex concentrated in degree [math] and define the cubical cochain complex of $P$ with coefficients in $G$, $C^{*}(P;G)$, to be the Hom complex ${\rm{Hom}}(C_{*}(P),G)$. The cubical cohomology of P with coefficients in $G$ is the graded module $H^{*}(P;G)=H(C^{*}(P;G))$.

We will not need to consider cubical chains and homology with coefficients in a module.

Remark 3.1.1*.*

An interesting elementary fact about $H_{*}(P)$ is that for every loop $\omega=x_{1\sharp}\cdots x_{k\sharp}\in P^{\mathbb{I}}$ such that ${\rm{char}}(R)\nmid k$, the homology class of the cycle $z_{\omega}=\sum_{i=1}^{k}x_{i}$ is nonzero. Indeed, if $\nu\in C^{1}(P;R)$ is the cochain where $\nu(x)=1$ for all $x\in P_{1}$, then $\nu(z_{\omega})=\sum_{i=1}^{k}\nu(x_{i})=k\cdot 1\not=0$. By definition of the cubical boundary operator, $\nu$ is a cocycle, and therefore $z_{\omega}$ is not a boundary.

3.2. Cubical singular chains

Let us briefly relate the cubical chain complex of a precubical set to the singular chain complex of its geometric realization. The normalized cubical singular chain complex of a space $X$ is the quotient chain complex $S_{*}(X)=C_{*}(SX)/D_{*}(SX)$ where $D_{*}(SX)$ denotes the subcomplex of $C_{*}(SX)$ generated by the degenerate singular cubes [HW67, Mas80]. This chain complex is naturally chain homotopy equivalent to the the usual simplicial singular chain complex of $X$ [HW67, Theorem 8.4.7]. The following theorem can, for instance, be established by adapting the proof of [Hat01, Theorem 2.27], which is an analogous result for $\Delta$-complexes.

Theorem 3.2.1**.**

Let $P$ be a precubical set. A natural chain homotopy equivalence ${{\mathsf{sing}}\colon C_{*}(P)}\to S_{*}(|P|)$ is given by

[TABLE]

3.3. Cellular chains

Recall that the cellular chain complex of a CW complex $X$ with skeleta $X_{n}$, $C^{CW}_{*}(X)$, is defined using (cubical or simplicial) singular homology as follows (see e.g. [Mas80, V.7]). For $n\geq 0$, one sets

[TABLE]

where, by convention, $X_{-1}=\emptyset$. The boundary operator $d\colon C^{CW}_{n}(X)\to C^{CW}_{n-1}(X)$ is the composite

[TABLE]

where $\partial_{*}$ is the connecting homomorphism in the long exact homology sequence of the pair $(X_{n},X_{n-1})$ and the second map is the one occurring in the long exact sequence of the pair $(X_{n-1},X_{n-2})$.

Theorem 3.3.1**.**

A natural chain isomorphism ${\mathsf{cell}}\colon C_{*}(P)\to C^{CW}_{*}(|P|)$ is given by

[TABLE]

or, more precisely, by ${\mathsf{cell}}(x)=[(|x_{\sharp}|+D_{n}(S|P_{\leq n}|))+S_{n}(|P_{<n}|)]$.

Proof.

For each $n\geq 0$, the quotient chain complex $C_{*}(P_{\leq n})/C_{*}(P_{<n})$ is concentrated in degree $n$, and we have a natural isomorphism

[TABLE]

The map ${\mathsf{cell}}\colon C_{n}(P)\to C^{CW}_{n}(|P|)$ is the composite of this isomorphism with the natural map

[TABLE]

which is an isomorphism by Theorem 3.2.1. Consider the following commutative diagram of modules:

[TABLE]

Since the bottom row is the boundary operator $d\colon C^{CW}_{n}(|P|)\to C^{CW}_{n-1}(|P|)$, the map ${\mathsf{cell}}\colon C_{*}(P)\to C^{CW}_{*}(|P|)$ is a natural isomorphism of chain complexes. ∎

4. Labeled homology of an HDA

We use the labeling function of an HDA over a free monoid to define its labeling cochains. The compatibility between the labeling function and the boundary operators—the fact that opposite edges of a $2$-cube have the same label—permits us to show that these cochains are cocycles and induce a labeling in cubical homology.

4.1. Labels of parallel edges

The following lemma establishes that parallel edges in subdivided cubes of HDAs (i.e., images of tensor products of precubical intervals under morphisms of precubical sets) have the same label:

Lemma 4.1.1**.**

Let ${\mathcal{A}}$ be an $M\mbox{-}$HDA, let $\chi\colon{\llbracket 0,l_{1}\rrbracket\otimes\cdots\otimes\llbracket 0,l_{n}\rrbracket}\to{\mathcal{A}}$ be a morphism of precubical sets, and let $1\leq s\leq n$ and $0\leq j_{s}<l_{s}$ be integers. Then for all tuples $(j_{1},\dots,j_{s-1},j_{s+1},\dots,j_{n})$ with $j_{i}\in\{0,\dots,l_{i}\}$,

[TABLE]

Proof.

Order the tuples $(j_{1},\dots,j_{s-1},j_{s+1},\dots,j_{n})$ lexicographically, and suppose inductively that the statement holds for all predecessors of a given such tuple that has at least one nonzero component. Let $t\not=s$ be an index such that $j_{t}\not=0$, and consider the tuple $(j^{\prime}_{1},\dots,j^{\prime}_{s-1},j^{\prime}_{s+1},\dots,j^{\prime}_{n})$ where

[TABLE]

This is a predecessor of the given tuple $(j_{1},\dots,j_{s-1},j_{s+1},\dots,j_{n})$. Consider the $2$-cube $b\in\llbracket 0,l_{1}\rrbracket\otimes\cdots\otimes\llbracket 0,l_{n}\rrbracket$ defined by

[TABLE]

Set

[TABLE]

Then

[TABLE]

4.2. The edge $e^{k}_{i}x$

Let $x$ be an element of degree $n>0$ of a precubical set $P$, and let $k\in\{0,1\}$ and $i\in\{1,\dots,n\}$. We define the element $e^{k}_{i}x\in P_{1}$ by

[TABLE]

The notation, introduced in [Kah16], reflects the fact that the edge $e^{k}_{i}x$ is associated with the face $d^{k}_{i}x$: The element $e^{0}_{i}x$ is an edge of $x$ leading from the final vertex of the face $d^{0}_{i}x$ to the final vertex of $x$, i.e., we have $d_{1}^{0}e^{0}_{i}x=d_{1}^{1}\cdots d_{1}^{1}d^{0}_{i}x$ and $d_{1}^{1}e^{0}_{i}x=d_{1}^{1}\cdots d_{1}^{1}x$. Similarly, $e^{1}_{i}x$ is an edge of $x$ leading from the initial vertex of $x$ to the initial vertex of the face $d^{1}_{i}x$, i.e., we have $d_{1}^{0}e^{1}_{i}x={d_{1}^{0}\cdots d_{1}^{0}x}$ and $d_{1}^{1}e^{1}_{i}x=d_{1}^{0}\cdots d_{1}^{0}d_{i}^{1}x$.

4.3. Free monoid

Let $\Sigma$ be an alphabet (i.e., a set). The free monoid on $\Sigma$ is denoted by $\Sigma^{*}$. The length of a string $m\in\Sigma^{*}$, i.e., the unique integer $n$ such that $m\in\Sigma^{n}$, will be denoted by $|m|$. Given a string $m$ of length $n\geq 1$, we will write $m_{1},\dots,m_{n}$ to denote the uniquely determined elements of $\Sigma$ such that $m=m_{1}\cdots m_{n}$.

4.4. Labeling cochain

Let $\Sigma$ be an alphabet, and let ${\mathcal{A}}$ be a $\Sigma^{*}\mbox{-}$HDA. Consider the exterior algebra on the free module generated by $\Sigma$, $\Lambda(\Sigma)$, and let $n\geq 0$ be an integer. The $n$th labeling cochain

[TABLE]

is the homomorphism of degree $-n$ defined on basis elements $x\in{\mathcal{A}}_{n}$ by

[TABLE]

Note that for an edge $x\in{\mathcal{A}}_{1}$ with $\lambda_{{\mathcal{A}}}(x)=m$, $\mathfrak{l}_{{\mathcal{A}}}^{1}(x)=\sum\limits_{j=1}^{|m|}m_{j}$. Thus $\mathfrak{l}_{{\mathcal{A}}}^{1}(x)$ is the image of $\lambda_{{\mathcal{A}}}(x)$ under the canonical monoid homomorphism from $\Sigma^{*}$ to the free module on $\Sigma$.

We show that the labeling cochain $\mathfrak{l}_{{\mathcal{A}}}^{n}$ is a cocycle. We need three lemmas.

Lemma 4.4.1**.**

For any element $x\in{\mathcal{A}}$ of degree $n\geq 1$, $\mathfrak{l}_{{\mathcal{A}}}^{1}(e^{0}_{i}x)=\mathfrak{l}_{{\mathcal{A}}}^{1}(e^{1}_{i}x)$.

Proof.

If $n=1$, then $e^{0}_{i}x=e^{1}_{i}x=x$. Suppose that $n\geq 2$. Then $e^{0}_{i}x=x_{\sharp}(1,\dots,1,\underset{i}{[0,1]},1,\dots,1)$ and $e^{1}_{i}x=x_{\sharp}(0,\dots,0,\underset{i}{[0,1]},0,\dots,0)$. Hence, by Lemma 4.1.1, $\lambda_{{\mathcal{A}}}(e^{0}_{i}x)=\lambda_{{\mathcal{A}}}(e^{1}_{i}x)$. Thus $\mathfrak{l}_{{\mathcal{A}}}^{1}(e^{0}_{i}x)=\mathfrak{l}_{{\mathcal{A}}}^{1}(e^{1}_{i}x)$. ∎

Lemma 4.4.2**.**

For any element $x\in{\mathcal{A}}$ of degree $n\geq 1$,

[TABLE]

Proof.

We have

[TABLE]

and

[TABLE]

By Lemma 4.4.1, also $\mathfrak{l}_{{\mathcal{A}}}^{n}(x)=\mathfrak{l}_{{\mathcal{A}}}^{1}(e^{1}_{1}x)\wedge\dots\wedge\mathfrak{l}_{{\mathcal{A}}}^{1}(e^{1}_{n}x)$. ∎

Lemma 4.4.3**.**

For all $n\geq 0$, $x\in{\mathcal{A}}_{n+1}$, and $i\in\{1,\dots,n+1\}$,

[TABLE]

Proof.

If $n=0$, then $\mathfrak{l}_{{\mathcal{A}}}^{n}(d^{0}_{i}x)=1=\mathfrak{l}_{{\mathcal{A}}}^{n}(d^{1}_{i}x)$. If $n=1$, then $\lambda_{{\mathcal{A}}}(d^{0}_{i}x)=\lambda_{{\mathcal{A}}}(d^{1}_{i}x)$ and therefore $\mathfrak{l}_{{\mathcal{A}}}^{1}(d^{0}_{i}x)=\mathfrak{l}_{{\mathcal{A}}}^{1}(d^{1}_{i}x)$. Suppose that $n\geq 2$. We have

[TABLE]

Hence, by Lemma 4.4.2 and Lemma 4.4.1,

[TABLE]

Proposition 4.4.4**.**

For each $n\geq 0$, $\mathfrak{l}_{{\mathcal{A}}}^{n}$ is a cocycle.

Proof.

Let $x\in{\mathcal{A}}_{n+1}$. By Lemma 4.4.3,

[TABLE]

4.5. Labeled homology

Let $\Sigma$ be an alphabet, and let ${\mathcal{A}}$ be a $\Sigma^{*}\mbox{-}$HDA. Since the labeling cochain $\mathfrak{l}_{{\mathcal{A}}}^{n}$ is a cocycle, we may define the $n$th labeling homomorphism

[TABLE]

by

[TABLE]

We will be able to drop the superscript $n$ and write $\ell_{{\mathcal{A}}}$ instead of $\ell_{{\mathcal{A}}}^{n}$. The labeled homology of ${\mathcal{A}}$ is the homology of ${\mathcal{A}}$ together with the sequence of labeling homomorphisms.

Examples 4.5.1*.*

(i) Consider the alphabet $\Sigma=\{a,b\}$ and the 1-dimensional $\Sigma^{*}\mbox{-}$HDA ${\mathcal{A}}$ made up of the boundary of a square in the way depicted in Figure 3(a).

For each edge $x$, we have $\mathfrak{l}_{{\mathcal{A}}}^{1}(x)=\lambda_{{\mathcal{A}}}(x)$. Therefore $\ell_{{\mathcal{A}}}(\alpha)=0$ for all $\alpha\in H_{1}({\mathcal{A}})$. This reflects the fact that every $1$-cycle would be a boundary if the square was not missing in ${\mathcal{A}}$. A hole in an HDA that is due to a set of missing cubes is related to what is called a forbidden region in [FGH*+*16]. The label of the homology class corresponding to such a hole is always zero.

(ii) Since $\Lambda(\Sigma)$ is a free module, the label of any torsion element in the homology of a $\Sigma^{*}\mbox{-}$HDA is [math].

(iii) A 1-dimensional $\Sigma^{*}\mbox{-}$HDA ${\mathcal{A}}$ is called a directed circle if it has $n$ distinct vertices $v_{0},\dots,v_{n-1}$ $(n\geq 1)$ and $n$ edges $x_{0},\dots,x_{n-1}$ such that for all $i$ and $k$, $d_{1}^{k}x_{i}=v_{i+k}$ (where $v_{n}=v_{0}$). The chain $z=\sum_{i=0}^{n-1}x_{i}$ is a cycle, and if $\lambda_{{\mathcal{A}}}(x_{i})=a_{i1}\cdots a_{ir_{i}}$ with $a_{i1},\dots,a_{ir_{i}}\in\Sigma$, then

[TABLE]

(iv) Consider the alphabet $\Sigma=\{a_{1},a_{2},b\}$ and the $\Sigma^{*}\mbox{-}$HDA ${\mathcal{A}}$ obtained from the one depicted in Figure 3(b) by identifying the horizontal rows and the left and right vertical edges. Then ${\mathcal{A}}$ is a torus and its ${\mathbb{Z}}_{2}$-homology is generated by two 1-dimensional classes with labels $a_{1}+a_{2}$ and $b$ and by a 2-dimensional class with label $a_{1}\wedge b+a_{2}\wedge b$.

If $a_{1}=a_{2}$, we may identify the horizontal rows of the HDA in Figure 3(b) not only to obtain a torus but also in a way that yields the Klein bottle. In either case, the ${\mathbb{Z}}_{2}$-homology of the resulting HDA is generated by two 1-dimensional classes with labels [math] and $b$ and by a 2-dimensional class with label [math].

5. Tensor-product HDAs

The tensor product of HDAs models the interleaving parallel composition of concurrent systems (see [Kah18]). In this section we show that the labeling cochains and the labeling homomorphisms of a tensor-product HDA are determined by those of its factors.

5.1. Tensor product of HDAs

The tensor product of two $M\mbox{-}$HDAs ${\mathcal{A}}$ and ${\mathcal{B}}$ is the $M\mbox{-}$HDA ${\mathcal{A}}\otimes{\mathcal{B}}$ where $P_{{\mathcal{A}}\otimes{\mathcal{B}}}=P_{{\mathcal{A}}}\otimes P_{{\mathcal{B}}}$, $I_{{\mathcal{A}}\otimes{\mathcal{B}}}=I_{{\mathcal{A}}}\times I_{{\mathcal{B}}}$, $F_{{\mathcal{A}}\otimes{\mathcal{B}}}=F_{{\mathcal{A}}}\times F_{{\mathcal{B}}}$, and $\lambda_{{\mathcal{A}}\otimes{\mathcal{B}}}$ is the composite

[TABLE]

With respect to this tensor product, the category of $M\mbox{-}$HDAs is a monoidal category.

5.2. The maps $\zeta$ and $\gamma$ and the cross products

Given (co)chain complexes $C$ and $D$, let $\kappa$ denote the natural homomorphism of graded modules

[TABLE]

Let $P$ and $Q$ be precubical sets. The homology cross product

[TABLE]

is defined to be the composite $\zeta_{*}\circ\kappa$ where $\zeta$ is the natural isomorphism of chain complexes

[TABLE]

given by

[TABLE]

Let $A$ and $B$ be modules, and consider the cochain complexes $C^{*}(P;A)={\rm{Hom}}(C_{*}(P),A)$ and $C^{*}(Q;B)={\rm{Hom}}(C_{*}(Q),B)$. The cohomology cross product

[TABLE]

is defined to be the composite $H({\rm{Hom}}(\zeta^{-1},A\otimes B)\circ\gamma)\circ\kappa$ where $\gamma$ is the natural chain map

[TABLE]

given by

[TABLE]

The homology cross product for precubical sets coincides with the usual homology cross product for spaces in the sense that it is isomorphic, as one easily checks, to the composite

[TABLE]

where $EZ$ is the Eilenberg-Zilber map

[TABLE]

which for singular cubes $f\colon[0,1]^{p}\to|P|$ and $g\colon[0,1]^{q}\to|Q|$ is given by

[TABLE]

(see [Mas80, VI.3], [HW67, 8.7.5]). The cohomology cross products for precubical sets and spaces are related in a similar fashion.

5.3. Labeled homology of tensor-product HDAs

Let $\Sigma$ be an alphabet, and let ${\mathcal{A}}$ and ${\mathcal{B}}$ be two $\Sigma^{*}\mbox{-}$HDAs.

Lemma 5.3.1**.**

Consider elements $x\in{\mathcal{A}}_{p}$ and $y\in{\mathcal{B}}_{q}$. Then

[TABLE]

Proof.

We may suppose that $p+q>0$. We have

[TABLE]

Hence

[TABLE]

Therefore

[TABLE]

By Lemma 4.4.2, it follows that

[TABLE]

Using the multiplication of $\Lambda(\Sigma)$ and the maps $\zeta$ and $\gamma$ defined in Section 5.2, we are now able to express the labeling cochains of ${\mathcal{A}}\otimes{\mathcal{B}}$ in terms of the labeling cochains of ${\mathcal{A}}$ and ${\mathcal{B}}$:

Proposition 5.3.2**.**

For each $n\geq 0$, ${\mathfrak{l}_{{\mathcal{A}}\otimes{\mathcal{B}}}^{n}}=\sum\limits_{i+j=n}{(-1)^{ij}\wedge\circ\gamma(\mathfrak{l}_{{\mathcal{A}}}^{i}\otimes\mathfrak{l}_{{\mathcal{B}}}^{j})\circ\zeta^{-1}}$.

Proof.

Let $n\geq 0$. Consider elements ${x\in{\mathcal{A}}_{p}}$ and ${y\in{\mathcal{B}}_{q}}$ where $p+q=n$. By Lemma 5.3.1,

[TABLE]

For $p^{\prime}\not=p$ and $q^{\prime}\not=q$ with $p^{\prime}+q^{\prime}=n$,

[TABLE]

Hence ${\mathfrak{l}_{{\mathcal{A}}\otimes{\mathcal{B}}}^{n}(x,y)}=\sum\limits_{i+j=n}{(-1)^{ij}\wedge\circ\gamma(\mathfrak{l}_{{\mathcal{A}}}^{i}\otimes\mathfrak{l}_{{\mathcal{B}}}^{j})\circ\zeta^{-1}(x,y)}$. ∎

Let us write $\wedge_{*}$ to denote the map

[TABLE]

induced by the multiplication of $\Lambda(\Sigma)$.

Theorem 5.3.3**.**

For all $n\geq 0$, $[\mathfrak{l}_{{\mathcal{A}}\otimes{\mathcal{B}}}^{n}]=\wedge_{*}(\sum\limits_{i+j=n}(-1)^{ij}[\mathfrak{l}_{{\mathcal{A}}}^{i}]\times[\mathfrak{l}_{{\mathcal{B}}}^{j}])$.

Proof.

This follows immediately from Proposition 5.3.2 because

[TABLE]

We shall show next that the label of the cross product of two homology classes is the exterior product of their labels. This implies that the labeling homomorphisms of ${\mathcal{A}}\otimes{\mathcal{B}}$ are entirely determined by those of ${\mathcal{A}}$ and ${\mathcal{B}}$. Indeed, by the Künneth theorem, there exists a graded torsion module $U\subseteq H_{*}({\mathcal{A}}\otimes{\mathcal{B}})$ such that

[TABLE]

and, as we have noted in Example 4.5.1(ii), torsion elements have zero label.

Theorem 5.3.4**.**

For all homology classes $\alpha\in H_{p}({\mathcal{A}})$ and $\beta\in H_{q}({\mathcal{B}})$,

[TABLE]

Proof.

Let ${a\in C_{p}({\mathcal{A}})}$ and ${b\in C_{q}({\mathcal{B}})}$ be cycles such that ${\alpha=[a]}$ and ${\beta=[b]}$. By Proposition 5.3.2, we have

[TABLE]

Example 5.3.5*.*

A directed torus is a $\Sigma^{*}\mbox{-}$HDA of the form ${\mathcal{A}}\otimes{\mathcal{B}}$ where ${\mathcal{A}}$ and ${\mathcal{B}}$ are directed circles. Let $x_{0},\dots,x_{n-1}$ and $y_{0},\dots,y_{m-1}$ be the edges of ${\mathcal{A}}$ and ${\mathcal{B}}$, respectively, and consider the cycles $x=\sum_{i}x_{i}$ and $y=\sum_{j}y_{j}$. Then the chain $z=\sum_{i,j}(x_{i},y_{j})$ is a cycle in $C_{*}({\mathcal{A}}\otimes{\mathcal{B}})$ and $[z]=[x]\times[y]$. Suppose that $\lambda_{{\mathcal{A}}}(x_{i})=a_{i1}\cdots a_{ir_{i}}$ and $\lambda_{{\mathcal{B}}}(y_{j})=b_{j1}\cdots b_{js_{j}}$ with all $a_{ip},b_{jq}\in\Sigma$. Then

[TABLE]

6. Cubical dimaps

The purpose of this section is to introduce cubical dimaps. Informally, a cubical dimap between two HDAs is a continuous map between their geometric realizations that sends cubes in an order-preserving way to subdivided cubes and that preserves labels of paths. Cubical dimaps are more flexible than morphisms of HDAs and permit one to relate HDAs that model concurrent systems at different refinement levels.

6.1. Permutation maps

Given $n$ precubical sets $P_{1},\dots,P_{n}$ and a permutation $\sigma\in S_{n}$, we denote by $t_{\sigma}$ the permutation map

[TABLE]

given by

[TABLE]

We remark that for permutations $\sigma,\tau\in S_{n}$, $t_{\sigma\circ\tau}=t_{\tau}\circ t_{\sigma}$. If $n=2$ and $\sigma$ is the transposition $(1\;2)$, we write $t$ instead of $t_{\sigma}$.

6.2. Cubical dimaps of precubical sets

An elementary cubical dimap (directed map) from a precubical set $Q$ to a precubical set $P$ is a continuous map $f\colon|Q|\to|P|$ such that the following two conditions hold:

1. (1)

For every vertex ${v\in Q_{0}}$, there exists a (necessarily unique) vertex $w\in P_{0}$ such that ${f([v,()])}={[w,()]}$. 2. (2)

For every element ${x\in Q_{n}}$ ${(n>0)}$, there exist integers $l_{1},\dots,l_{n}\geq 1$, a morphism of precubical sets ${\chi\colon\llbracket 0,{l_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l_{n}}\rrbracket}\to P$, a permutation $\sigma\in S_{n}$, and increasing homeomorphisms ${\phi_{i}\colon|\llbracket 0,1\rrbracket|=[0,1]\to|\llbracket 0,{l_{i}}\rrbracket|}=[0,l_{i}]$ $(i\in{\{1,\dots,n\})}$ such that ${f\circ|x_{\sharp}|}={|\chi|\circ(\phi_{1}\times\cdots\times\phi_{n})\circ t_{\sigma}}$.

A cubical dimap of precubical sets is a finite composite of elementary cubical dimaps.

Examples 6.2.1*.*

(i) The geometric realization of a morphism of precubical sets is an elementary cubical dimap.

(ii) An important class of cubical dimaps is given by subdivisions in the sense of [Kah14b]: A subdivision of a precubical set $Q$ consists of a precubical set $P$ and a homeomorphism $|Q|\to|P|$ that is an elementary cubical dimap such that the permutation in condition (2) of the definition is always the identity.

(iii) For precubical sets $P_{1},\dots,P_{n}$ and a permutation $\sigma\in S_{n}$, the permutation map $t_{\sigma}\colon|P_{1}\otimes\dots\otimes P_{n}|\to|P_{\sigma(1)}\otimes\dots\otimes P_{\sigma(n)}|$ is an elementary cubical dimap. As we do not need this fact in this paper, we omit the details.

Remarks 6.2.2*.*

(i) Condition (2) in the definition of elementary cubical dimaps guarantees that cubical dimaps are directed maps in the sense that they respect the directed topology of geometric realizations of precubical sets. A prominent framework for directed topology is Grandis’ category of d-spaces [Gra09]. A cubical dimap can be seen as a d-map, i.e., a morphism of d-spaces.

(ii) Cubical dimaps are closely related to weak morphisms as studied in [Kah14a, Kah14b, Kah16]. Although the two concepts are formally incomparable, a weak morphism will normally be a cubical dimap. Permutation maps are cubical dimaps but not in general weak morphisms.

(iii) By construction, a cubical dimap is a cellular map.

We next show that the objects in condition (2) of the definition of elementary cubical dimaps are unique.

Lemma 6.2.3**.**

[Kah14b, 2.3.3]* Consider integers ${n,k_{1},\dots,k_{n},l_{1},\dots,l_{n}\geq 1}$, morphisms of precubical sets ${\xi\colon\llbracket 0,{k_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{k_{n}}\rrbracket\to P}$ and $\zeta\colon{\llbracket 0,{l_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l_{n}}\rrbracket}\to P$, and a homeomorphism $\alpha\colon{|\llbracket 0,{k_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{k_{n}}\rrbracket|}\to{|\llbracket 0,{l_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l_{n}}\rrbracket|}$ such that ${|\zeta|\circ\alpha}=|\xi|$. Then $k_{i}=l_{i}$ for all $i\in\{1,\dots,n\}$, $\alpha=id$, and $\xi=\zeta$.*

Proposition 6.2.4**.**

Let $f\colon|Q|\to|P|$ be an elementary cubical dimap of precubical sets, and let $x\in Q_{n}$ $(n\geq 1)$ be an element. Then there exist unique integers $l_{1},\dots,l_{n}\geq 1$, a unique morphism of precubical sets $\chi\colon{\llbracket 0,{l_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l_{n}}\rrbracket}\to P$, a unique permutation $\sigma\in S_{n}$, and unique increasing homeomorphisms $\phi_{i}\colon{|\llbracket 0,1\rrbracket|}=[0,1]\to{|\llbracket 0,{l_{i}}\rrbracket|}=[0,l_{i}]$ $(i\in\{1,\dots,n\})$ such that ${f\circ|x_{\sharp}|}={|\chi|\circ(\phi_{1}\times\cdots\times\phi_{n})\circ t_{\sigma}}$.

Proof.

The existence of $l_{1},\dots,l_{n}$, $\chi$, $\sigma$, and $\phi_{1},\dots,\phi_{n}$ is guaranteed by the definition of elementary cubical dimaps. Suppose that the integers $l^{\prime}_{1},\dots,l^{\prime}_{n}$, the morphism of precubical sets $\chi^{\prime}\colon\llbracket 0,{l^{\prime}_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l^{\prime}_{n}}\rrbracket\to P$, the permutation ${\sigma^{\prime}\in S_{n}}$, and the increasing homeomorphisms $\phi^{\prime}_{i}\colon|\llbracket 0,{1}\rrbracket|\to|\llbracket 0,{l^{\prime}_{i}}\rrbracket|$ $(i\in\{1,\dots,n\})$ satisfy ${f\circ|x_{\sharp}|}={|\chi^{\prime}|\circ(\phi^{\prime}_{1}\times\cdots\times\phi^{\prime}_{n})\circ t_{\sigma^{\prime}}}$. Consider the homeomorphisms $\phi={(\phi_{1}\times\cdots\times\phi_{n})\circ t_{\sigma}}$, $\psi={(\phi^{\prime}_{1}\times\cdots\times\phi^{\prime}_{n})\circ t_{\sigma^{\prime}}}$, and $\alpha={\psi\circ\phi^{-1}}\colon{|\llbracket 0,{l_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l_{n}}\rrbracket|}\to{|\llbracket 0,{l^{\prime}_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l^{\prime}_{n}}\rrbracket|}$. Then $|\chi^{\prime}|\circ\alpha={|\chi^{\prime}|\circ\psi\circ\phi^{-1}}=f\circ|x_{\sharp}|\circ\phi^{-1}=|\chi|\circ\phi\circ\phi^{-1}=|\chi|$. By Lemma 6.2.3, it follows that $l^{\prime}_{i}=l_{i}$ for all $i\in\{1,\dots,n\}$, $\psi=\phi$, and $\chi^{\prime}=\chi$. We show that $\sigma^{\prime}=\sigma$. This then also implies that $\phi^{\prime}_{1}\times\dots\times\phi^{\prime}_{n}=\phi_{1}\times\dots\times\phi_{n}$ and hence that $\phi^{\prime}_{i}=\phi_{i}$ for all $i$. Consider $i\in\{1,\dots,n\}$, and set

[TABLE]

We have

[TABLE]

On the other hand,

[TABLE]

Hence

[TABLE]

Since $\phi_{i}$ and the $\phi^{\prime}_{j}$ are increasing homeomorphisms, this implies that

[TABLE]

Thus $\sigma^{\prime}(i)=\sigma(i)$. ∎

6.3. Notation

Given precubical sets $P$ and $Q$ and an elementary cubical dimap $f\colon|Q|\to|P|$, Proposition 6.2.4 permits us to fix the following notation for the objects in condition (2) of the definition of elementary cubical dimaps: We write $R_{x}=\llbracket 0,{l_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l_{n}}\rrbracket$, $\phi_{xi}=\phi_{i}$, $\sigma_{x}=\sigma$, and $x_{\flat}=\chi$. Note that here we silently omit any reference to $f$.

6.4. Vertex map

It is clear that condition (1) in the definition of elementary cubical dimaps holds for arbitrary cubical dimaps as well. Therefore a cubical dimap $f\colon|Q|\to|P|$ induces a vertex map $f_{0}\colon Q_{0}\to P_{0}$, which sends a vertex $v\in Q_{0}$ to the unique vertex $w\in P_{0}$ such that $f([v,()])=[w,()]$.

6.5. Paths

Let $f\colon|Q|\to|P|$ be a cubical dimap, and let $\omega\colon\llbracket 0,k\rrbracket\to Q$ be a path.

Proposition 6.5.1**.**

There exist a unique integer $l$, a unique path $\nu\colon\llbracket 0,l\rrbracket\to P$, and a unique increasing homeomorphism $\phi\colon|\llbracket 0,k\rrbracket|=[0,k]\to|\llbracket 0,l\rrbracket|=[0,l]$ such that $|\nu|\circ\phi=f\circ|\omega|$.

Proof.

If $k=0$, we may and must set $l=0$, $\phi=id$, and $\nu=f_{0}(\omega(0))_{\sharp}$.

Suppose that $k>0$. Write $\omega=x_{1\sharp}\cdots x_{k\sharp}$. To show existence, suppose first that $f$ is elementary. For each $i$, let $R_{x_{i}}=\llbracket 0,l_{i}\rrbracket$ and write $\phi_{i}=\phi_{x_{i}1}$. Since $\sigma_{x_{i}}=id$, we have $f\circ|x_{i\sharp}|=|x_{i\flat}|\circ\phi_{i}$. In order to define $\nu$, we will concatenate the paths $x_{i\flat}$. This is possible because for $1\leq i<k$, $x_{i\flat}(l_{i})=x_{(i+1)\flat}(0)$. Indeed,

[TABLE]

Set $l=l_{1}+\dots+l_{k}$ and $\nu=x_{1\flat}\cdots x_{k\flat}$, and consider the increasing homeomorphism $\phi\colon[0,k]\to[0,l]$ given by

[TABLE]

For $i\in\{1,\dots,k\}$ and $t\in[i-1,i]$, we have

[TABLE]

Hence $|\nu|\circ\phi=f\circ|\omega|$, and existence is shown for elementary cubical dimaps. This implies that $l$, $\nu$, and $\phi$ exist if $f$ is an arbitrary cubical dimap. Consider an integer $l^{\prime}$, a path $\nu^{\prime}\colon\llbracket 0,l^{\prime}\rrbracket\to P$, and an increasing homeomorphism $\psi\colon|\llbracket 0,k\rrbracket|=[0,k]\to|\llbracket 0,l^{\prime}\rrbracket|=[0,l^{\prime}]$ such that $|\nu^{\prime}|\circ\psi=f\circ|\omega|$. Consider the homeomorphism $\alpha=\psi\circ\phi^{-1}\colon|\llbracket 0,{l}\rrbracket|\to|\llbracket 0,{l^{\prime}}\rrbracket|$. Then $|\nu^{\prime}|\circ\alpha=|\nu^{\prime}|\circ\psi\circ\phi^{-1}=f\circ|\omega|\circ\phi^{-1}=|\nu|\circ\phi\circ\phi^{-1}=|\nu|$. By Lemma 6.2.3, it follows that $l^{\prime}=l$, $\psi=\phi$, and $\nu^{\prime}=\nu$. ∎

The path $\nu$ of Proposition 6.5.1 will be denoted by $f^{\mathbb{I}}(\omega)$. We remark that if $k=0$, $f^{\mathbb{I}}(\omega)$ is the path in $P$ of length [math] given by $f^{\mathbb{I}}(\omega)(0)=f_{0}(\omega(0))$. Note also that if $f$ is the geometric realization of a morphism of precubical sets $h\colon Q\to P$, then $f^{\mathbb{I}}(\omega)=h\circ\omega$. Note finally that if $g\colon|P|\to|K|$ is a second cubical dimap, then $(g\circ f)^{\mathbb{I}}(\omega)=g^{\mathbb{I}}\circ f^{\mathbb{I}}(\omega)$.

6.6. Cubical dimaps of HDAs

An elementary cubical dimap from an $M\mbox{-}$HDA ${\mathcal{B}}$ to an $M\mbox{-}$HDA ${\mathcal{A}}$ is an elementary cubical dimap of precubical sets $f\colon|{\mathcal{B}}|\to|{\mathcal{A}}|$ such that $f_{0}(I_{{\mathcal{B}}})\subseteq I_{{\mathcal{A}}}$, $f_{0}(F_{{\mathcal{B}}})\subseteq F_{{\mathcal{A}}}$, and $\overline{\lambda}_{{\mathcal{A}}}\circ f^{\mathbb{I}}=\overline{\lambda}_{{\mathcal{B}}}$. A cubical dimap of $M\mbox{-}$HDAs is a finite composite of elementary cubical dimaps. It is clear that the conditions $f_{0}(I_{{\mathcal{B}}})\subseteq I_{{\mathcal{A}}}$, $f_{0}(F_{{\mathcal{B}}})\subseteq F_{{\mathcal{A}}}$, and $\overline{\lambda}_{{\mathcal{A}}}\circ f^{\mathbb{I}}=\overline{\lambda}_{{\mathcal{B}}}$ hold for arbitrary cubical dimaps and not only for elementary ones.

7. Naturality

It is not difficult to see that labeled homology is natural with respect to morphisms of HDAs. Here we establish that it also is natural with respect to cubical dimaps.

7.1. The chain map induced by a cellular map

Given precubical sets $P$ and $Q$ and a cellular map $f\colon|Q|\to|P|$, let $f_{*}\colon C_{*}(Q)\to C_{*}(P)$ be the unique chain map making the following diagram commute:

[TABLE]

Note that if $f$ is the geometric realization of a morphism of precubical sets $g\colon Q\to P$, then $f_{*}=g_{*}\colon C_{*}(Q)\to C_{*}(P)$. In Section 7.4 we give an explicit description of $f_{*}$ for elementary cubical dimaps.

7.2. Naturality of $\zeta$

Recall from Section 5.2 that given precubical sets $P$ and $Q$, $\zeta$ is the isomorphism of chain complexes

[TABLE]

given by

[TABLE]

Lemma 7.2.1**.**

The isomorphism $\zeta$ is natural with respect to cellular maps, i.e., for precubical sets $P$, $P^{\prime}$, $Q$, and $Q^{\prime}$, cellular maps $f\colon|P|\to|P^{\prime}|$ and $g\colon|Q|\to|Q^{\prime}|$, and the cellular map $f\times g\colon|P\otimes Q|=|P|\times|Q|\to|P^{\prime}\otimes Q^{\prime}|=|P^{\prime}|\times|Q^{\prime}|$, the following diagram of chain complexes is commutative:

[TABLE]

Proof.

Given precubical sets $P$ and $Q$, let $\mu$ denote the unique chain map ${C^{CW}_{*}(|P|)\otimes C^{CW}_{*}(|Q|)}\to C^{CW}_{*}(|P|\times|Q|)$ making the following diagram commute:

[TABLE]

A straightforward verification shows that $\mu$ coincides on $C^{CW}_{p}(|P|)\otimes C^{CW}_{q}(|Q|)$ with the composite

[TABLE]

where $j$ is the inclusion and the relative cross product $\times$ is defined using the map

[TABLE]

induced by the Eilenberg-Zilber map (see Section 5.2). It follows that $\mu$ is natural with respect to cellular maps, and this implies that $\zeta$ is natural with respect to cellular maps. ∎

It is clear that $\zeta$ is associative and can be iterated. Given precubical sets $P_{1},\dots,P_{n}$, the chain isomorphism $C_{*}(P_{1})\otimes\dots\otimes C_{*}(P_{n})\to C_{*}(P_{1}\otimes\dots\otimes P_{n})$ will also be denoted by $\zeta$. It follows from Lemma 7.2.1 that this iterated $\zeta$ is natural with respect to cellular maps.

7.3. Interchange map of a square

Consider the interchange map

[TABLE]

and the induced chain map

[TABLE]

Lemma 7.3.1**.**

$t_{*}(\iota_{2})=-\iota_{2}$.

Proof.

Since the boundary operator

[TABLE]

is injective, it is enough to show that $dt_{*}(\iota_{2})=-d\iota_{2}$. In view of the commutative diagram

[TABLE]

it suffices to show that $dt_{*}({\mathsf{cell}}(\iota_{2}))=-d{\mathsf{cell}}(\iota_{2})$. We have

[TABLE]

and hence

[TABLE]

Identifying $|(d^{k}_{i}\iota_{2})_{\sharp}|=\delta^{k}_{i}\colon|\llbracket 0,1\rrbracket|=[0,1]\to|\llbracket 0,1\rrbracket^{\otimes 2}|=[0,1]^{2}$, we compute

[TABLE]

It follows that

[TABLE]

7.4. The chain map induced by an elementary cubical dimap

Let $f$ be an elementary cubical dimap from a precubical set $Q$ to a precubical set $P$.

Proposition 7.4.1**.**

The chain map $f_{*}\colon C_{*}(Q)\to C_{*}(P)$ is given by

[TABLE]

Proof.

Let $x\in Q_{0}$. Since ${f\circ|x_{\sharp}|=|f_{0}(x)_{\sharp}|}$, the map $f_{*}\colon C^{CW}_{0}(|Q|)\to C^{CW}_{0}(|P|)$ sends ${\mathsf{cell}}(x)$ to ${\mathsf{cell}}(f_{0}(x))$. Hence $f_{*}\colon C_{0}(Q)\to C_{0}(P)$ sends $x$ to $f_{0}(x)$.

Let $n>0$ and $x\in Q_{n}$. Consider the following commutative diagram:

[TABLE]

We have $f_{*}(x)=f_{*}\circ x_{\sharp*}(\iota_{n})=x_{\flat*}\circ(\phi_{x1}\times\cdots\times\phi_{xn})_{*}(t_{\sigma_{x}*}(\iota_{n}))$. We show first that $t_{\sigma_{x}*}(\iota_{n})={\rm{sgn}}(\sigma_{x})\iota_{n}$. If $n=1$, there is nothing to show. If $n>1$, write $\sigma_{x}={\sigma_{1}\circ\dots\circ\sigma_{m}}$ where each $\sigma_{j}$ is a transposition of the form $(i\;\;i+1)$. Then $t_{\sigma_{x}}=t_{\sigma_{m}}\circ\dots\circ t_{\sigma_{1}}$ and ${\rm{sgn}}(\sigma_{x})=(-1)^{m}$. It is thus enough to show that $t_{(i\;\;i+1)*}(\iota_{n})=-\iota_{n}$. Since

[TABLE]

Lemma 7.2.1 implies that the following diagram is commutative:

[TABLE]

Thus, by Lemma 7.3.1,

[TABLE]

We next compute $(\phi_{x1}\times\cdots\times\phi_{xn})_{*}(\iota_{n})$. Suppose that $R_{x}=\llbracket 0,{l_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l_{n}}\rrbracket$. By Lemma 7.2.1, we have the following commutative diagram:

[TABLE]

One easily computes that $\phi_{xi*}\colon C_{*}(\llbracket 0,1\rrbracket)\to C_{*}(\llbracket 0,l_{i}\rrbracket)$ sends $\iota_{1}$ to $\sum_{j_{i}=0}^{l_{i}-1}[j_{i},j_{i}+1]$. Hence

[TABLE]

Finally, $f_{*}(x)=x_{\flat*}\circ(\phi_{x1}\times\cdots\times\phi_{xn})_{*}(t_{\sigma_{x}*}(\iota_{n}))={\rm{sgn}}(\sigma_{x})\sum_{y\in(R_{x})_{n}}x_{\flat}(y)$. ∎

7.5. Naturality of labeled homology

We are now ready to establish the naturality of labeled homology with respect to cubical dimaps.

Theorem 7.5.1**.**

Let $f$ be a cubical dimap from a $\Sigma^{*}\mbox{-}$HDA ${\mathcal{B}}$ to a $\Sigma^{*}\mbox{-}$HDA ${\mathcal{A}}$. Then $\mathfrak{l}_{B}^{n}=\mathfrak{l}_{{\mathcal{A}}}^{n}\circ f_{*}$ for all $n\geq 0$. Consequently, $\ell_{{\mathcal{B}}}=\ell_{{\mathcal{A}}}\circ f_{*}$ in all degrees.

Proof.

We may suppose that $f$ is elementary. For any vertex $v\in Q_{0}$, $\mathfrak{l}_{{\mathcal{B}}}^{0}(v)=1=\mathfrak{l}_{{\mathcal{A}}}^{0}(f_{0}(v))=\mathfrak{l}_{{\mathcal{A}}}^{0}\circ f_{*}(v)$. Suppose that $n>0$. Consider an element $x\in Q_{n}$, and let $R_{x}=\llbracket 0,{l_{1}}\rrbracket\otimes\cdots\otimes\llbracket 0,{l_{n}}\rrbracket$. For $i\in\{1,\dots,n\}$ and $j_{i}\in\{0,\dots,l_{i}-1\}$, consider the edge

[TABLE]

of $R_{x}$. We show first that the following diagram is commutative:

[TABLE]

We have $(e^{0}_{\sigma_{x}(i)}\iota_{n})_{\sharp}(\iota_{1})=e^{0}_{\sigma_{x}(i)}\iota_{n}=(1,\dots,1,\underset{\sigma_{x}(i)}{[0,1]},1,\dots,1)$ and hence

[TABLE]

Let $j_{i}\in\{0,\dots,l_{i-1}\}$ and $s\in[0,1]$ be numbers such that $\phi_{xi}(t)=j_{i}+s=[[j_{i},j_{i}+1],s]$. Then

[TABLE]

Since $x_{\sharp}\circ(e^{0}_{\sigma_{x}(i)}\iota_{n})_{\sharp}(\iota_{1})=x_{\sharp}(e^{0}_{\sigma_{x}(i)}\iota_{n})=e^{0}_{\sigma_{x}(i)}x_{\sharp}(\iota_{n})=e^{0}_{\sigma_{x}(i)}x$, we have

[TABLE]

and therefore

[TABLE]

Hence

[TABLE]

Consequently,

[TABLE]

Thus

[TABLE]

Consider the element $y=([j_{1},j_{1}+1],\dots,[j_{n},j_{n}+1])\in(R_{x})_{n}$. We have

[TABLE]

Now, by Lemma 4.1.1,

[TABLE]

Thus $\mathfrak{l}_{{\mathcal{A}}}^{1}(x_{\flat}(e^{0}_{i}y))=\mathfrak{l}_{{\mathcal{A}}}^{1}(x_{\flat}(b_{i}^{j_{i}}))$ and therefore

[TABLE]

Using Proposition 7.4.1, we obtain

[TABLE]

As an immediate consequence of Theorem 7.5.1, we note the following result:

Corollary 7.5.2**.**

Let ${\mathcal{A}}$ be a $\Sigma^{*}\mbox{-}$HDA such that the label of some homology class of degree $>0$ is nonzero. Then there does not exist any cubical dimap from ${\mathcal{A}}$ to a contractible $\Sigma^{*}\mbox{-}$HDA.

8. Applications

In this section we discuss two potential applications of labeled homology in concurrency theory.

8.1. Independence

An important global question about a given concurrent system is which subsystems are independent from each other. Let us define here that the $M\mbox{-}$HDAs ${\mathcal{B}}_{1},\dots,{\mathcal{B}}_{n}$ are independent in the $M\mbox{-}$HDA ${\mathcal{A}}$ if there exist a subautomaton ${\mathcal{B}}$ of ${\mathcal{A}}$ and a cubical dimap of $M\mbox{-}$HDAs ${|{\mathcal{B}}_{1}\otimes\dots\otimes{\mathcal{B}}_{n}|}\to|{\mathcal{B}}|$ that is a homeomorphism. This concept of independence is a variant of the one considered in [FGH*+*16, 5.21].

Proposition 8.1.1**.**

Suppose that the $\Sigma^{*}\mbox{-}$HDAs ${\mathcal{B}}_{i}$ $(i=1,\dots,n)$ are independent in the $\Sigma^{*}\mbox{-}$HDA ${\mathcal{A}}$, and consider homology classes $\beta_{i}\in H_{*}({\mathcal{B}}_{i})$ $(i=1,\dots,n)$. Then there exists a homology class $\alpha\in H_{*}({\mathcal{A}})$ such that

[TABLE]

Proof.

This follows immediately from Theorems 5.3.4 and 7.5.1. ∎

Example 8.1.2*.*

Let us consider the following version of the classical dining philosophers system [Dij71]: Four philosophers sit at a round table having dinner. A chopstick is placed to the left of each philosopher. In order to eat, a philosopher needs this chopstick and also the one on the right. Each philosopher alternately thinks and eats according to the following instructions:

• •

Think.

• •

Wait until the left chopstick is free and pick it up.

• •

Wait until the right chopstick is free and pick it up.

• •

Eat.

• •

Put the left chopstick down.

• •

Put the right chopstick down.

• •

Repeat the procedure from the beginning.

At the beginning of the dinner, all chopsticks are free.

The reachable part of the state space of the dining philosophers system may be modeled by a $\Sigma^{*}\mbox{-}$HDA ${\mathcal{A}}$ where the alphabet $\Sigma$ is given by

[TABLE]

Here the indexes correspond, of course, to the four philosophers. The HDA ${\mathcal{A}}$ is of dimension 4 and has 465 vertices, 1508 edges, 1766 2-cubes, 884 3-cubes, and 160 4-cubes.

For each $i\in\{0,1,2,3\}$, the HDA ${\mathcal{A}}$ contains a subautomaton ${\mathcal{B}}_{i}$ corresponding to the subsystem where only the $i$th philosopher has dinner and the others remain inactive in their initial states. The HDA ${\mathcal{B}}_{i}$ is a directed circle and has a 1-dimensional homology generator with label

[TABLE]

By Theorem 7.5.1, it follows that ${\mathcal{A}}$ has four 1-dimensional homology classes with labels $l_{0}$, $l_{1}$, $l_{2}$, and $l_{3}$, respectively. Since these labels are linearly independent, so are the homology classes.

If two philosophers, say philosophers $i$ and $j$, are not neighbors at the table, they eat independently because they do not share any chopstick. Consequently, ${\mathcal{B}}_{i}$ and ${\mathcal{B}}_{j}$ are independent in ${\mathcal{A}}$. By Proposition 8.1.1, it follows that ${\mathcal{A}}$ has a 2-dimensional homology class with label $l_{i}\wedge l_{j}$. Since the other two philosophers are also not neighbors, ${\mathcal{A}}$ has a second 2-dimensional homology class of this type, and the two homology classes are linearly independent because their labels are.

Computing the ${\mathbb{Z}}_{2}$-homology of ${\mathcal{A}}$ using the software CHomP [Pil18], one obtains that $H_{n}({\mathcal{A}})=0$ for $n>2$, $\dim H_{0}({\mathcal{A}})=1$, $\dim H_{1}({\mathcal{A}})=4$, and $\dim H_{2}({\mathcal{A}})=2$. We have thus completely determined the labeled ${\mathbb{Z}}_{2}\mbox{-}$homology of ${\mathcal{A}}$.

Suppose that philosophers $i$ and $j$ are neighbors at the table. Then, as one might expect, the HDAs ${\mathcal{B}}_{i}$ and ${\mathcal{B}}_{j}$ are not independent in ${\mathcal{A}}$. Otherwise, by Proposition 8.1.1, $l_{i}\wedge l_{j}$ would be the label of a 2-dimensional homology class of ${\mathcal{A}}$, which is not the case. Note that the reason for the dependence of ${\mathcal{B}}_{i}$ and ${\mathcal{B}}_{j}$ is not just that philosophers $i$ and $j$ share a resource. Indeed, as shows Example 8.2.2 below, processes that share resources may very well be independent.

8.2. Specification

Consider the practical problem to decide whether an $M\mbox{-}$HDA ${\mathcal{A}}$ implements a certain specification that is given by another $M\mbox{-}$HDA $\mathcal{S}$. Let us say here that ${\mathcal{A}}$ implements $\mathcal{S}$ if there exists a finite sequence of cubical dimaps of $M\mbox{-}$HDAs

[TABLE]

where the cubical dimaps indicated by $\xleftarrow{\sim}$ are homotopy equivalences that could also be required to preserve relevant constructions such as the trace category and the homology graph (see [Kah14a, Kah14b, Kah16]). This implementation relation can be seen as a kind of simulation preorder that permits one to relate HDAs of different refinement levels.

Proposition 8.2.1**.**

Let ${\mathcal{A}}$ and $\mathcal{S}$ be $\Sigma^{*}$-HDAs such that ${\mathcal{A}}$ implements $\mathcal{S}$. Then for each homology class $\alpha\in H_{*}({\mathcal{A}})$, there exists a homology class $\beta\in H_{*}(\mathcal{S})$ such that $\ell_{\mathcal{S}}(\beta)=\ell_{{\mathcal{A}}}(\alpha)$.

Proof.

This follows immediately from Theorem 7.5.1. ∎

Example 8.2.2*.*

As an example, consider the task to implement a locking mechanism for two processes by incrementing and decrementing an integer variable $\mathtt{x}$ using the operators $\mathtt{x{\scriptstyle{++}}}$ and $\mathtt{x{\scriptstyle{--}}}$, respectively. These operators are to be interpreted in such a way that $\mathtt{x{\scriptstyle{++}}}$ means to acquire the lock and $\mathtt{x{\scriptstyle{--}}}$ means to release it. In order to specify the task more formally, consider the alphabet

[TABLE]

where the indexes in the instructions are the process IDs, and the $\Sigma^{*}\mbox{-}$HDA $\mathcal{S}$ given by a wedge of two directed circles, one labeled with the string $\mathtt{x{\scriptstyle{++}}_{0}};\mathtt{x{\scriptstyle{--}}_{0}}$ and the other with the string $\mathtt{x{\scriptstyle{++}}_{1}};\mathtt{x{\scriptstyle{--}}_{1}}$. Let us suppose now we had the (bad) idea to implement this locking mechanism through a concurrent program where both processes execute a loop consisting of the instruction sequence $\mathtt{x{\scriptstyle{++}}};\mathtt{x{\scriptstyle{--}}}$. Assuming that $\mathtt{x}$ is initially [math], the HDA ${\mathcal{A}}$ corresponding to the reachable part of the state space of this program is a directed torus, and there exists a 2-dimensional homology class with label

[TABLE]

which is nonzero. Since the 2-dimensional homology of $\mathcal{S}$ is trivial, Proposition 8.2.1 implies that ${\mathcal{A}}$ does not implement $\mathcal{S}$. The error in our program is, of course, that we forgot to include a guard condition that forces the processes to wait until the variable $\mathtt{x}$ is [math] before they increment it.