2019  OriginalPaper  Buchkapitel Open Access
Trees in Partial Higher Dimensional Automata
1 Introduction

Open maps from [17] can be understood as trivial fibrations, namely weak equivalences (here, bisimulations) that have the right lifting properties with respect to some morphisms.

Those morphisms are precisely extensions of executions, which means that they can be seen as cofibration generators (in the language of cofibrantly generated model structures [15]).

Cofibrations are then morphisms that have the left lifting property with respect to open maps. In particular, this allows us to define cofibrant objects as those objects whose unique morphisms from the initial object is a cofibration. In a way, cofibrant objects are those objects that are constructed by just using extensions of paths, and should correspond to trees.

The cofibrant replacement is then given by canonically constructing a cofibrant object, which is weakly equivalent (here, bisimilar) to a given object. That should correspond to the unfolding.
2 Fixing the Definition of pHDA
2.1 Higher Dimensional Automata
2.2 Original Definition of Partial Higher Dimensional Automata

first the ‘local’ equations are not enough in the partial case. Imagine that we want to model a full cube c without its lower face, that is, \(\partial _{3,3}^0\) is not defined on c, and such that \(\partial _{1,2}^1\) is undefined on \(\partial _{1,3}^1(c)\) and \(\partial _{2,3}^1(c)\), that is, we remove an edge. We cannot prove using the local equations that \(\partial _1^1\circ \partial _2^0\circ \partial _1^1(c) = \partial _1^1\circ \partial _2^0\circ \partial _2^1(c)\), that is, that the vertices of the cube are uniquely defined. Indeed, to prove this equality using the local equations, you can only permute two consecutive \(\partial \). From \(\partial _1^1\circ \partial _2^0\circ \partial _1^1(c)\), you can:and both faces are not defined. On the other hand, those two should be equal because the comaps \(d_1^1\circ d_2^0\circ d_1^1\) and \(d_2^1\circ d_2^0\circ d_1^1\) are equal in \(\Box \), and \(\partial _1^1\circ \partial _2^0\circ \partial _1^1\) and \(\partial _1^1\circ \partial _2^0\circ \partial _2^1\) are both defined on c.

either permute the first two and you obtain \(\partial _1^1\circ \partial _1^1\circ \partial _3^0(c)\),

or permute the last two and you obtain \(\partial _1^0\circ \partial _1^1\circ \partial _1^1(c)\).


secondly, the notion of morphism is not good (or at least, ambiguous). The equations \(f_n\circ \partial _{i,n,X}^\alpha = \partial _{i,n,Y}^\alpha \circ f_{n+1}\) hold in [7] only when both face maps are defined, which authorises many morphisms. For example, consider the segment I, and the ‘split’ segment \(I'\) which is defined as I, except that no face maps are defined (geometrically, this corresponds to two points and an open segment). The identity map from I to \(I'\) is a morphism of partial precubical sets in the sense of [7], which is unexpected. A bad consequence of that is that the notion of paths in a partial HDA does not correspond to morphisms from some particular partial HDA, and paths are not preserved by morphisms, as we will see later.
2.3 Partial Higher Dimensional Automata as Lax Functors

for every object c of \(\mathcal {C}\), a set Fc,

for every morphism \(i : c \longrightarrow c'\), a partial function \(Fi : Fc \longrightarrow Fc'\)

if \(n=0\), \(\epsilon \star (j_1< \ldots< j_m ; \beta _1, \ldots , \beta _m) = (j_1< \ldots < j_m ; \beta _1, \ldots , \beta _m)\),

if \(m = 0\), \((i_1<\ldots< i_n ; \alpha _1, \ldots , \alpha _n) \star \epsilon = (i_1<\ldots < i_n ; \alpha _1, \ldots , \alpha _n)\),

if \(i_1 \le j_1\), \((i_1<\ldots< i_n ; \alpha _1, \ldots , \alpha _n) \star (j_1< \ldots< j_m ; \beta _1, \ldots , \beta _m) = (i_1;\alpha _1).((i_2<\ldots< i_n ; \alpha _2, \ldots , \alpha _n) \star (j_1+1< \ldots < j_m+1 ; \beta _1, \ldots , \beta _m))\),

if \(i_1 > j_1\), \((i_1<\ldots< i_n ; \alpha _1, \ldots , \alpha _n) \star (j_1< \ldots< j_m ; \beta _1, \ldots , \beta _m) = (j_1;\beta _1).((i_1<\ldots< i_n ; \alpha _1, \ldots , \alpha _n) \star (j_2< \ldots < j_m ; \beta _2, \ldots , \beta _m))\).
2.4 Completion of a pHDA

if \(\partial _{i_1< \ldots < i_k}^{\alpha _1, \ldots , \alpha _k}(x)\) is defined, thenThis means that, if a face of a cube exists in X, this face is identified with both abstract faces \((\epsilon , \partial _{i_1< \ldots < i_k}^{\alpha _1, \ldots , \alpha _k}(x))\) (i.e., the cube \(\partial _{i_1< \ldots < i_k}^{\alpha _1, \ldots , \alpha _k}(x)\) itself) and \(((i_1< \ldots < i_k ; \alpha _1, \ldots , \alpha _k), x)\) (i.e., the face of x, which consists of taking the \((i_k,\alpha _k)\) face, then the \((i_{k1},\alpha _{k1})\) face, and so on).$$((i_1< \ldots< i_k ; \alpha _1, \ldots , \alpha _k), x) \sim (\epsilon , \partial _{i_1< \ldots < i_k}^{\alpha _1, \ldots , \alpha _k}(x)).$$

if \(((i_1< \ldots< i_k ; \alpha _1, \ldots , \alpha _k), x) \sim ((j_1< \ldots < j_l ; \beta _1, \ldots , \beta _l), y)\), then \(((i_1< \ldots< i_k ; \alpha _1, \ldots , \alpha _k)\star (i,\alpha ), x) \sim ((j_1< \ldots < j_l ; \beta _1, \ldots , \beta _l)\star (i,\alpha ), y)\). This means that if two abstract faces coincide, then taking both their \((i,\alpha )\) face gives two abstract faces that also coincide.Let \(\chi (X)_n = Y_n/\sim \) and we denote by \(\ll (i_1< \ldots < i_k ; \alpha _1, \ldots , \alpha _k), x \gg \) the equivalence class of \(((i_1< \ldots < i_k ; \alpha _1, \ldots , \alpha _k), x)\) modulo \(\sim \). We define the iface map as \(\partial _i^\alpha (\ll (i_1< \ldots< i_k ; \alpha _1, \ldots , \alpha _k), x\gg ) = ~ \ll (i_1< \ldots < i_k ; \alpha _1, \ldots , \alpha _k)\star (i,\alpha ), x\gg \), the initial state as \(\ll \epsilon ,i\gg \) and the labelling function as \(\lambda (\ll (i_1< \ldots < i_k ; \alpha _1, \ldots , \alpha _k), x \gg ) = \delta _{i_1}^{\alpha _1}\circ \ldots \circ \delta _{i_k}^{\alpha _k}(\lambda (x))\).
3 Paths in Partial Higher Dimensional Automata
3.1 Path Category, Open Maps, Coverings
3.2 Encoding Paths in pHDA

if \(\alpha _k =0\), then \(x_{k1} = \partial _{j_k}^{0}(x_k)\),

if \(\alpha _k =1\), then \(x_{k} = \partial _{j_k}^{1}(x_{k1})\).

if \(\alpha _k =0\), then \(d_{k1} = d_k  1\), \(\delta _{j_k}(w_k) = w_{k1}\) and \(j_k \le d_k\),

if \(\alpha _k =1\), then \(d_{k} = d_{k1}  1\), \(\delta _{j_k}(w_{k1}) = w_k\) and \(j_k \le d_{k1}\).

\(B\sigma _p = \{k \in \{0,\ldots ,n\} \mid d_k = p\}\),

the partial face maps \(\partial _{i_1< \ldots < i_n}^{\alpha _1, \ldots , \alpha _n}\) are the smallest (as relations ordered by inclusion) partial functions such that:

if \(\alpha _k = 0\), then \(\partial _{j_k}^{0}(k) = k1\),

if \(\alpha _k = 1\), then \(\partial _{j_k}^{1}(k1) = k\),

\(\partial _{j_1< \ldots< j_m}^{\beta _1, \ldots , \beta _m}\circ \partial _{i_1< \ldots< i_n}^{\alpha _1, \ldots , \alpha _n} \subseteq \partial _{k_1< \ldots < k_{n+m}}^{\gamma _1, \ldots , \gamma _{n+m}}\), for \((k_1, \ldots , k_{n+m} ; \gamma _1, \ldots , \gamma _{n+m}) = (i_1,\ldots , i_n ; \alpha _1, \ldots , \alpha _n) \star (j_1, \ldots , j_m ; \beta _1, \ldots , \beta _m)\).


the initial state is 0,

the labelling functions \(\lambda _n\) map k to \(w_k\).
4 Trees and Unfolding in pHDA
4.1 Trees, as Colimits of Paths in pHDA

\(X_0 = \{(u,k) \mid u \in \mathcal {C}, k \le l_u \wedge d^u_k = 0\} \sqcup \{\epsilon \}\),

\(X_n = \{(u,k) \mid u \in \mathcal {C}, k \le l_u \wedge d^u_k = n\}\).

for every u, \((u,0) \sim \epsilon \),

if \(i : u \longrightarrow v \in \mathcal {C}\), and if \(k \le l_u, l_v\), then \((u,k) \sim (v,k)\).

\([u_0,k] \approx [v_0,k]\),

for every \(0 \le s \le l\), \(\alpha _{k+1+s}^{u_s} = \alpha _{k+1+s}^{v_s} = 1\),

for every \(0 \le s < l\), \([u_s,k+s+1] \approx [u_{s+1},k+s+1]\) and \([v_s,k+s+1] \approx [v_{s+1},k+s+1]\),

\((j_{k+1}^{u_0};1)\star \ldots \star (j_{k+l+1}^{u_l};1) = (j_{k+1}^{v_0};1)\star \ldots \star (j_{k+l+1}^{v_l};1)\),then, \([u_l,k+l+1] \approx [v_l,k+l+1]\). \(\text {col} \, D\) is the pHDA \(Z_N\) with the face maps being the smallest relations for inclusion such that:

if \(\alpha _k^u = 0\), then \(\partial _{j_k^u}^0(\langle u,k \rangle )\) is defined and is equal to \(\langle u,k1 \rangle \),

if \(\alpha _{k+1}^u = 1\) then \(\partial _{j_k^u}^1(\langle u,k \rangle )\) is defined and is equal to \(\langle u,k+1 \rangle \),

\(\partial _{j_1< \ldots< j_m}^{\beta _1, \ldots , \beta _m}\circ \partial _{i_1< \ldots< i_n}^{\alpha _1, \ldots , \alpha _n} \subseteq \partial _{k_1< \ldots < k_{n+m}}^{\gamma _1, \ldots , \gamma _{n+m}}\), for \((k_1, \ldots , k_{n+m} ; \gamma _1, \ldots , \gamma _{n+m}) = (i_1,\ldots , i_n ; \alpha _1, \ldots , \alpha _n) \star (j_1, \ldots , j_m ; \beta _1, \ldots , \beta _m)\).
4.2 The Unique Path Properties of Trees

for all \(k < s\) or \(k \ge t\), \(x_k = x'_k\),

for all \(k < s\) or \(k > t\), \(j_k = j'_k\) and \(\alpha _k = \alpha '_k\),

for all \(s \le k \le t\), \(\alpha _k = \alpha '_k = 1\),

\((j_{s},\alpha _{s})\star \ldots \star (j_t,\alpha _t) = (j'_{s},\alpha '_{s})\star \ldots \star (j'_t,\alpha '_t)\).
4.3 Trees Are Unfoldings

\(U(X)_n\) is the set of equivalence classes \([\pi ]\) of paths modulo confluent homotopy, such that \(e(\pi )\) is of dimension n,

the face maps are the smallest relations for inclusion such that:

\(\partial _i^1(\alpha ) = [\pi \xrightarrow {i,1} \partial _i^1(e(\pi ))]\), for any \(\pi \in \alpha \) such that \(\partial _i^1(e(\pi ))\) is defined,

\(\partial _i^0(\alpha ) = [\pi _{1}]\) for any \(\pi \in \alpha \) such that \(\pi = \pi _{1} \xrightarrow {i,0} e(\pi )\),

\(\partial _{j_1< \ldots< j_m}^{\beta _1, \ldots , \beta _m}\circ \partial _{i_1< \ldots< i_n}^{\alpha _1, \ldots , \alpha _n} \subseteq \partial _{k_1< \ldots < k_{n+m}}^{\gamma _1, \ldots , \gamma _{n+m}}\), for \((k_1, \ldots , k_{n+m} ; \gamma _1, \ldots , \gamma _{n+m}) = (i_1,\ldots , i_n ; \alpha _1, \ldots , \alpha _n) \star (j_1, \ldots , j_m ; \beta _1, \ldots , \beta _m)\).


the initial state is [i],

the labelling is given by \(\lambda (\alpha ) = \lambda (e(\pi ))\) for \(\pi \in \alpha \).