On the topology of concurrent systems
Catarina Faustino Thomas Kahl Rodrigo Lopes






55U10, 68Q85, 05E45



On the topology of concurrent systems
    Mathieu Isoard
    
=====================================




	Higher-dimensional automata, i.e., pointed labeled precubical sets, are a powerful combinatorial-topological model for concurrent systems. In this paper, we show that for every (nonempty) connected polyhedron there exists a shared-variable system such that the higher-dimensional automaton modeling the state space of the system has the homotopy type of the polyhedron.





§ INTRODUCTION


As amply demonstrated in the literature, concepts and methods from algebraic topology can be profitably employed in concurrency theory, the field of computer science that studies systems of simultaneously executing processes, see, e.g., <cit.>. Several topological models of concurrency have been introduced by various authors, e.g., <cit.>. A particularly important combinatorial-topological model of concurrency is given by higher-dimensional automata <cit.>, which go back to <cit.>. It has been shown in <cit.> that higher-dimensional automata are more expressive than the principal traditional models of concurrency. 


A higher-dimensional automaton (HDA) is a pointed precubical set (cubical set without degeneracy maps) with edge labeling such that opposite edges of cubes have the same label. The vertices of an HDA represent the states of a concurrent system, with the base vertex corresponding to the initial state. The labeled edges model the transitions of the system, and two- and higher-dimensional cubes express the independence of transitions: an n-cube in an HDA indicates that the n transitions starting from its origin are independent in the sense that they can occur in any order or even simultaneously without any observable difference.  


	A standard procedure for constructing an HDA model of a concurrent system is to first construct a transition system and then fill in empty squares and higher-dimensional cubes, see,  e.g., <cit.>. To make this more precise, consider the example of Peterson's algorithm, a protocol designed to give two processes fair and mutually exclusive access to a shared resource <cit.>. Peterson's algorithm is based on three shared variables—namely, a variable t whose possible values are the process IDs, say 0 and 1, and two  boolean variables b_0 and b_1. Process i executes the following protocol with four local states and four transitions: 
	
		
  * Set b_i to 1 to indicate the intention to enter the “critical section".
		
  * Set t to 1-i to give priority to the other process.
		
  * Wait until b_1-i = 0 or t = i, and then enter the critical section. 
		
  * Leave the critical section setting b_i to 0, and repeat the procedure from the beginning. 
	
    To start, all variables are set to 0. A global state of such a shared-variable system is a tuple whose components are local states of the processes and values of the variables. The transition system associated with the shared-variable system is a labeled directed graph whose vertices correspond to  the global states that are actually visited during some execution of the system, and whose edges model the transitions between these global states. 
    The transitions starting from a given global state correspond to the actions that are enabled in that state. These actions are specified in the edge labels, indexed by the respective process IDs. The HDA model of the system is then constructed from the transition system as a kind of coskeleton, i.e., by suitably filling in empty cubes of dimensions ≥ 2, see Figure <ref> for the case of Peterson's algorithm.
	



    It turns out that the topological analysis of HDAs provides information that is relevant from the point of view of computer science. Indeed, two executions of a concurrent system can be considered equivalent if and only if they can be modeled as directed paths that are homotopic in a directed sense, see, e.g., <cit.>. Additionally, the homology of an HDA model of a concurrent system contains global information about the independence of processes and components of the system <cit.>. Further connections between algebraic topology and concurrency theory are developed in <cit.>.
    



It turns out that the topological analysis of HDAs provides information that is relevant from the point of view of computer science. Indeed, two executions of a concurrent system can be considered equivalent if and only if they are modeled by directed paths that are homotopic in a directed sense, see, e.g., <cit.>. Additionally, the homology of an HDA contains global information about the independence of processes and components of the modeled concurrent system <cit.>. Further connections between algebraic topology and concurrency theory are developed in <cit.>.


The purpose of this paper is to show that the topology of an HDA model of a concurrent system can be arbitrarily complex. More precisely, we show that for every (nonempty) connected polyhedron there exists a shared-variable system whose HDA model has the same homotopy type as the polyhedron. This is similar in spirit to <cit.>, where it is shown that for every connected polyhedron there exists a PV-program (a particular kind of shared-variable system) whose execution space contains a connected component with the same homotopy type as the polyhedron. This paper is also related to <cit.>, where in particular it is shown that every polyhedron admits a cubical local partial order. In fact, the first step in the proof of our result is to show that the cubical barycentric subdivision of a simplicial complex can be constructed as a precubical set. This actually strengthens <cit.> because it shows that no further subdivision of the cubical barycentric subdivision is needed to equip a polyhedron with a cubical local partial order. 

The paper is organized as follows. The precubical set corresponding to the cubical barycentric subdivision of a simplicial complex is constructed in Section <ref>. In Section <ref>, we turn this precubical set into an HDA, which we show to be an HDA model of the transition system given by its 1-skeleton. In the next section, we show that one can replace this HDA by a homotopy equivalent accessible one, i.e., an HDA where all states are reachable by a directed path from the initial state. In the last section, we then show that this accessible HDA is isomorphic to the HDA model of a shared-variable system. 




§ THE SIMPLICIAL COMPLEX  AND ITS CUBICAL BARYCENTRIC SUBDIVISION 
 

Throughout this paper, we consider a connected abstract simplicial complex K with vertices 1, …, N and the associated polyhedron |K|, which we view as a subspace of the standard (N-1)-simplex Δ^N-1⊆^N. More precisely, we define |K| to be the subspace ⋃_σ∈ K |σ| ⊆Δ^N-1, where for a simplex σ∈ K, |σ| is the geometric simplex in ^N with vertices e_i = (0, …, 0, i1, 0, … 0), i ∈σ. In this section, we construct the cubical barycentric subdivision of K as a precubical set. 









 §.§ Precubical sets


Let us briefly recall some basic concepts about precubical sets. A precubical set is a graded set X = (X_n)_n ≥ 0 with face maps d^k_i X_n → X_n-1 (n>0, k∈{0,1}, i ∈{1, …, n}) satisfying the relations d^k_i∘ d^l_j= d^l_j-1∘ d^k_i (k,l ∈{0,1},  i<j). If x∈ X_n, we say that x is of  degree or dimension n. The elements of degree n are called the n-cubes of X. The elements of degree 0 are also called the vertices of X, and the 1-cubes are also called the edges of X. Precubical sets form a category in which  morphisms are morphisms of graded sets that are compatible with the face maps. A precubical subset of a precubical set X is a graded subset of X that is stable under the face maps. The tensor product of two precubical sets X and Y is the precubical set X⊗ Y given by 
    (X⊗ Y)_n = ∐_p+q = n X_p× Y_q
 
and

    d_i^k(x,y) = {[   (d_i^kx,y),     1≤ i ≤ p,; (x,d_i-p^ky),    p < i ≤ n, ].    (x,y) ∈ X_p× Y_q.
 The geometric realization of a precubical set X is the quotient space 
    |X|=(∐ _n ≥ 0 X_n × [0,1]^n)/∼
 where the sets X_n are given the discrete topology and the equivalence relation is generated by

    (d^k_ix,u) ∼ (x,δ_i^k(u)),     x ∈ X_n+1,  u∈ [0,1]^n,  i ∈{1, …, n+1},  k ∈{0,1}.

Here the map δ^k_i [0,1]^n → [0,1]^n+1 is defined by 
    δ^k_i(u_1, …, u_n) = (u_1, …, u_i-1,k,u_i, …, u_n).

The geometric realization is functorial. For a morphism of precubical sets f X → Y, the continuous map |f| |X| → |Y| is given by |f|([x,u])= [f(x),u]. The geometric realization of a precubical set is a CW complex. The nskeleton of |X| is the geometric realization of the precubical subset X_≤ n of X defined by (X_≤ n)_i = X_i for i ≤ n and (X_≤ n)_i = ∅ for i > n.



 §.§ The precubical set P


The cubical barycentric subdivision of K is the precubical set P where the elements of P_n are pairs (τ, σ) of simplexes of K such that τ is a face of σ and σ∖τ has n elements, see Figure <ref> for a picture. 
 
Considering the natural order on the set of vertices of K, the face maps of P are defined as follows: if σ∖τ = {w_1 < ⋯ < w_n}, we set 

    d^0_i(τ, σ) = (τ, σ∖{w_i} )
 and 
    d^1_i(τ, σ) = (τ∪{w_i}, σ).
 
One easily checks that P is indeed a precubical set. The remainder of this section is devoted to the proof that |P|≈ |K|.

















 §.§ The map 
 


Let (τ, σ) ∈ P_n, and suppose that 
    τ = {v_1 < ⋯ < v_r}    σ∖τ = {w_1 < ⋯ < w_n}.
 
We decompose the standard n-cube [0,1]^n as the union of the n-simplexes

    Δ_θ = {(t_1, …, t_n) ∈ [0,1]^n|  t_θ(1)≥⋯≥ t_θ(n)},   θ∈ S_n

and define a continuous map f_τ, σ [0,1]^n → |K| by setting for an element (t_1, … , t_n) ∈Δ_θ, 

    f_τ, σ(t_1, … , t_n)
       = 1 -t_θ(1)r∑_i=1^r e_v_i + t_θ(1) -t_θ(2)r+1(∑_i=1^r e_v_i + e_w_θ(1)) + ⋯
           +  t_θ(n-1) -t_θ(n)r+n-1(∑_i=1^r e_v_i + ∑_i=1^n-1 e_w_θ(i)) + t_θ(n)r+n(∑_i=1^r e_v_i + ∑_i=1^n e_w_θ(i))

(see Figure <ref>). If σ = τ, this formula is to be interpreted in such a way that f_τ, σ(()) = 1/r∑_i=1^r e_v_i. Note that f_τ, σ(t_1, … , t_n) is a convex combination of barycenters of faces of |σ| and hence itself an element of |σ|. By  the following fact, the proof of which is left to the reader, f_τ, σ is well defined:

 
	Let θ, ψ∈ S_n and (t_1, …, t_n) ∈Δ_θ∩Δ_ψ. Then t_θ(i) = t_ψ(i) for all i ∈{1, …, n}. Moreover, if 1 ≤ i_1 < … < i_k = n are indices such that 
	
    t_θ(1) = … = t_θ(i_1) >  t_θ(i_1+1) = … > t_θ(i_k-1+1) = … = t_θ(n),

	then {θ(1), … , θ(i_s)} = {ψ(1), …, ψ(i_s)} for all s ∈{1, …, k}.	


  



The next lemma shows that a well-defined continuous map f  |P| → |K| is given by 
    f([(τ, σ),(t_1, …, t_n)]) = f_τ, σ(t_1, …, t_n),    (τ, σ) ∈ P_n,  (t_1, …, t_n) ∈ [0,1]^n.



	Let (τ, σ) ∈ P_n (n ≥ 1), and suppose that τ = {v_1 < ⋯ < v_r} and σ∖τ = {w_1 < ⋯ < w_n}. Then 
	f_τ, σ∖{w_i} = f_τ, σ∘δ^0_i  [0,1]^n-1→ |K| and f_τ∪{w_i}, σ = f_τ, σ∘δ^1_i  [0,1]^n-1→ |K|. 



	We prove only the first equality and leave the similar proof of the second to the reader. Let us first note that 
	
    ( σ∖{ w_i } ) ∖τ    =  { w_1 < … < w_i-1 < w_i+1 < … < w_n}
        =  {w̅_1 < … < w̅_i-1 < w̅_i < … < w̅_n-1}
 	
	with 	
	
    w̅_j =
    		
    			w_j,      j<i, 
    
    			w_j+1,      j≥ i.

	Let θ∈ S_n-1 and (t_1, …, t_n-1) ∈Δ_θ⊆  [0,1]^n-1. Then t_θ(1)≥…≥ t_θ(n-1), and so defining (x_1, …, x_n)  = (t_1, …, t_i-1, 0, t_i, …, t_n-1), we will have that (x_1, …, x_n) ∈Δ_ψ⊆ [0,1]^n, with ψ∈ S_n defined by  
	
    ψ (j) =
    		θ(j),      j<n, θ(j)<i, 
    θ(j) + 1,      j<n, θ(j)≥ i, 
    
    			i,     j=n.

	Indeed, 
	
    x_ψ (j)   =
    		
    			x_θ(j) = t_θ(j),      j<n, θ(j)<i, 
    
    			x_θ(j) + 1 = t_θ(j),       j<n, θ(j)≥ i, 
    
    			x_i = 0,     j=n
    		  = 
    		
    			t_θ(j),      j<n, 
    
    			0,     j=n.

	So x_ψ(1)≥…≥ x_ψ(n), i.e.,  (x_1, …, x_n) ∈Δ_ψ. Note also that 
	
    w_ψ (j)    =
    		
    			w_θ(j) = w̅_θ(j),      j<n, θ(j)<i, 
    
    			w_θ(j) + 1 = w̅_θ(j),     j<n, θ(j)≥ i, 
    
    			w_i,     j=n
    		   =
    		w̅_θ(j),     j<n, 
    
    			w_i,     j=n.

	We finally have that
	
    f_τ, σ∘δ_i^0 (t_1 …, t_n-1) = 	f_τ, σ (t_1 …, t_i-1, 0, t_i, … t_n-1) = f_τ, σ (x_1, …, x_n) 
        = 1-x_ψ (1)r∑_l=1^r e_v_l + x_ψ (1) - x_ψ(2)r+1 (∑_l=1^r e_v_l + e_w_ψ(1))+ …
            + x_ψ (n-1) - x_ψ(n)r+n-1 (∑_l=1^r e_v_l + ∑_l=1^n-1 e_w_ψ(l))   + x_ψ (n)r+n (∑_l=1^r e_v_l + ∑_l=1^n e_w_ψ(l)) 
        =  1-t_θ (1)r∑_l=1^r e_v_l + t_θ (1) - t_θ(2)r+1 (∑_l=1^r e_v_l + e_w̅_θ(1)) + …
           + t_θ (n-1) - 0r+n-1 (∑_l=1^r e_v_l + ∑_l=1^n-1 e_w̅_θ(l))   + 0r+n (∑_l=1^r e_v_l + ∑_l=1^n-1 e_w̅_θ(l) + e_w_i) 
        = f_τ, σ∖{ w_i } (t_1, …, t_n-1).
	






We can now prove the main result of this section:

 
	The map f  |P| → |K| is a homeomorphism.




	In order to define a map g |K| → |P|, consider an element x∈ |K|. Let σ = {u_1 < ⋯ < u_n} be the unique simplex of K such that x = ∑_i = 1^n s_ie_u_i for (unique) numbers s_i > 0 such that ∑_i = 1^n s_i = 1. Choose a permutation α∈ S_n such that s_α(1)≥⋯≥ s_α(n). 
	Let 
    m = max{i ∈{1, …, n} |  s_α(i) = s_α (1)},
 and set τ = {u_α(1), …, u_α(m)}. Let ϕ be the unique order-isomorphism 
    {α(m+1), …, α(n)}→{1, …, n-m},
 and define θ∈ S_n-m by
	θ(i) = ϕ(α(m+i)). Set 
    t_θ(i) = (m+i)s_α(m+i) + ∑_j = m+i+1^ns_α(j).
 Then 
    0 ≤ t_θ(n-m)≤⋯≤ t_θ(1)≤∑_j = 1^n s_α(j) = 1.
 Hence (t_1, …, t_n-m) ∈Δ_θ⊆ [0,1]^n-m. We set 
    g(x) = [(τ,σ),(t_1, …, t_n-m)].

	Using Lemma <ref>, one easily checks that g(x) does not depend on the choice of the permutation α. We have thus defined a map g |K| → |P|. Tedious but rather straightforward computations now show that f∘ g = id_|K| and g∘ f = id_|P|. Since f is a continuous map between compact Hausdorff spaces, it follows that f is a homeomorphism.







§ THE HDA 
 

A higher-dimensional automaton (HDA) is a tuple = (P_,I_,Σ_, λ_) where  P_ is a precubical set, I_∈ (P_)_0 is a vertex, called the initial state, Σ_ is a finite set of labels, and λ_ (P_)_1 →Σ_ is a map, called the labeling function, such that λ_ (d_i^0x) = λ_ (d_i^1x) for all x ∈ (P_)_2 and i ∈{1,2} <cit.>. The vertices of an HDA are also called its states. 
Originally, an HDA is also equipped with a set of final states, but since we will never need final states, we omit this part of the structure. HDAs form a category in which a morphism from an HDA  to an HDA  is a pair (f,g) consisting of a morphism of precubical sets f P_→ P_ and a map g Σ_→Σ_ such that f(I_) = I_ and λ_(f(x)) = g(λ_(x)) for all x ∈ (P_)_1. 

 



We turn the precubical set P defined in the previous section into an HDA  by setting P_ = P, I_ = ({1},{1}), Σ_ = {1, … , N}, and λ_(τ, σ) = a
for (τ, σ) ∈ P_1 with σ∖τ = {a}. This is indeed an HDA since for (τ, σ)∈ P_2 with σ∖τ = {a < b},

    λ_(d^0_1(τ, σ)) = λ_(τ, τ∪{b}) = b = λ_(τ∪{a}, σ) = λ_(d^1_1(τ, σ))

and 

    λ_(d^0_2(τ, σ)) = λ_(τ, τ∪{a}) = a = λ_(τ∪{b}, σ) = λ_(d^1_2(τ, σ)).




An HDA is said to be deterministic if no two edges with the same source have the same label. An HDA is said to be codeterministic if no two edges with the same target have the same label. We say that an HDA is bideterministic if it is both deterministic and codeterministic.

 
	The HDA  is bideterministic.



	Let (τ, τ) be a vertex of , and let (τ, σ) and (τ, ρ) be two edges with the same label starting in (τ, τ). Suppose that σ∖τ = {a} and that ρ∖τ = {b}. Then a = λ_(τ, σ) = λ _(τ, ρ) = b. Hence σ = τ∪{a} = τ∪{b} = ρ, and so the two edges are the same. Thus,  is deterministic. A similar argument shows that  is codeterministic.	




 §.§ HDA models


An HDA is extensional if no two edges with the same endpoints have the same label. If an HDA is deterministic or codeterministic, it is extensional. A transition system is a 1-truncated extensional HDA, i.e., an extensional HDA concentrated in degrees ≤ 1.

Let  be a transition system, and let R be a relation on the alphabet Σ_.  The HDA model of  with respect to R is the by <cit.> up to isomorphism uniquely determined HDA 𝒬 which satisfies the following conditions:

	
  HM1 The 1-skeleton of , _≤ 1 = ((P_)_≤ 1, I_, Σ_, λ_), is . 
	
  HM2 For all x ∈ (P_𝒬)_2, λ_𝒬(d^0_2x)  R λ_𝒬(d^0_1x).		
	
  HM3 For all m≥ 2 and x,y ∈ (P_𝒬)_m, if d^k_rx = d^k_ry for all r ∈{1,… ,m} and k ∈{0,1}, then x = y.		
	
  HM4 𝒬 is maximal with respect to the properties HM1–HM3, i.e., there is no HDA  satisfying HM1–HM3 with P_⫋ P_.	

Condition HM1 says that  is built on top of  by filling in empty cubes. By condition HM2, an empty square may only be filled in if the labels of its edges are related. Condition HM3 ensures that no empty cube is filled in twice in the same way. By condition HM4, all admissible empty cubes are filled in. 

 
	 is the HDA model of its 1-skeleton _≤ 1 with respect to <.



	Since  is deterministic, _≤ 1 is indeed a transition system. 
	
	HM1 is obvious. 
	
	HM2: Let (τ, σ) be a 2-cube of . Suppose that σ∖τ = {a < b}. We have 
	
    λ_(d^0_2(τ, σ)) = λ_(τ,τ∪{a}) = a < b = λ_(τ,τ∪{b}) = λ_(d^0_1(τ, σ)).

	
	HM3: Let m ≥ 2, and let (τ, σ), (τ', σ')∈ P_m such that  d^k_r(τ, σ) = d^k_r(τ',σ') for all r ∈{1,… ,m} and k ∈{0,1}. Suppose that σ∖τ = {w_1 < … < w_m} and that σ' ∖τ' = {w_1' < … < w_m'}. Since d^0_1(τ, σ) = d^0_1(τ',σ'), we have 
	(τ, σ∖{w_1}) = (τ', σ' ∖{w_1'}) and therefore τ = τ'. Since d^1_1(τ, σ) = d^1_1(τ',σ'), we have 
	(τ∪{w_1}, σ ) = (τ' ∪{w_1'}, σ' ) and therefore σ = σ'. Thus, (τ, σ) = (τ', σ'). 
	
	HM4: Let  be an HDA satisfying HM1–HM3 with respect to _≤ 1 and < such that P_ = P is a precubical subset of P_. By HM1, (P_)_m = P_m for m ≤ 1. Let m ≥ 2, and suppose inductively that (P_)_m-1 = P_m-1. Let x ∈ (P_)_m. By the inductive hypothesis, d^k_ix ∈ P_m-1 for all i and k. Write d^k_ix = (τ^k_i, σ^k_i) and σ^k_i ∖τ^k_i = {w^k_i,1 < … < w^k_i,m-1}. Consider i ∈{1, …, m} and j ∈{1, …, m-1}. If m = 2, we have 
	
    w^0_i,j   = w^0_i,1 = λ_(τ^0_i,τ^0_i∪{w^0_i,1}) = λ_(τ^0_i,σ^0_i) = 
    		λ_(d^0_ix)
       = λ_(d^1_ix) = λ_(τ^1_i, σ^1_i) = λ_(τ^1_i, τ^1_i ∪{w^1_i,1}) = w^1_i,1 = w^1_i,j.

	If m ≥ 3, we have
	
    λ_(d^0_1⋯ d^0_j-1d^0_j+1⋯ d^0_m-1d^0_ix)
       = λ_(d^0_1⋯ d^0_j-1d^0_j+1⋯ d^0_m-1(τ^0_i,τ^0_i∪{w^0_i,1< … < w^0_i,m-1}))
       = λ_(d^0_1⋯ d^0_j-1d^0_j+1⋯ d^0_m-2(τ^0_i,τ^0_i∪{w^0_i,1 < … < w^0_i,m-2}))
       = ⋯
       = λ_(d^0_1⋯ d^0_j-1d^0_j+1 (τ^0_i,τ^0_i∪{w^0_i,1 < … < w^0_i,j-1< w^0_i,j< w^0_i,j+1}))
       = λ_(d^0_1⋯ d^0_j-1 (τ^0_i,τ^0_i∪{w^0_i,1 < … < w^0_i,j-1< w^0_i,j}))
       = ⋯
       = λ_(τ^0_i,τ^0_i∪{w^0_i,j})
       = w^0_i,j

	and 
	
    λ_(d^1_1⋯ d^1_j-1d^1_j+1⋯ 	d^1_m-1d^1_ix)
       = λ_(d^1_1⋯ d^1_j-1d^1_j+1⋯ d^1_m-1(τ^1_i,τ^1_i∪{w^1_i,1< … < w^1_i,m-1}))
       = λ_(τ^1_i∪{w^1_i,1< … < w^1_i,j-1< w^1_i,j+1< ⋯  w^1_i,m-1},
             τ^1_i∪{w^1_i,1< … < w^1_i,m-1})
       = w^1_i,j.

	Since parallel edges in an HDA have the same label (see, e.g., <cit.>, it follows that w^0_i,j = w^1_i,j in the case m ≥ 3 as well.
	
	
	Let 1 ≤ i < j ≤ m. Since 
	
    d^0_id^0_jx    = d^0_i(τ^0_j, σ^0_j) = (τ^0_j, σ^0_j∖{w^0_j,i})

	and 
	
    d^0_j-1d^0_ix    = d^0_j-1(τ^0_i, σ^0_i) = (τ^0_i, σ^0_i∖{w^0_i,j-1}),

	we have τ^0_i = τ^0_j. Set τ = τ^0_i = τ^0_j. Since 
	
    d^0_id^1_jx    = d^0_i(τ^1_j, σ^1_j) = (τ^1_j, σ^1_j∖{w^1_j,i})

	and 
	
    d^1_j-1d^0_ix    = d^1_j-1(τ^0_i, σ^0_i) = (τ^0_i ∪{w^0_i,j-1}, σ^0_i),

	we have τ^1_j = τ∪{w^0_i,j-1}. Since 
	
    d^1_id^0_jx    = d^1_i(τ^0_j, σ^0_j) = (τ^0_j ∪{w^0_j,i}, σ^0_j)

	and 
	
    d^0_j-1d^1_ix    = d^0_j-1(τ^1_i, σ^1_i) = (τ^1_i, σ^1_i ∖{w^1_i,j-1}),

	we have τ^1_i = τ∪{w^0_j,i}.
	
	Since τ^1_j = τ∪{w^0_i,j-1} for all 1≤  i < j ≤ m, we have 
	
    w^0_1,j-1 = w^0_2,j-1 = …  = w^0_j-1,j-1

	for all 1 < j ≤ m. Since τ^1_i = τ∪{w^0_j,i} for all 1≤  i < j ≤ m, we have 
	
    w^0_i+1,i = w^0_i+2,i = …  = w^0_m,i

	for all 1≤ i < m. Since  τ∪{w^0_i+1,i} = τ^1_i =  τ∪{w^0_i-1,i-1} for all 1 < i < m, we have 
	
    w^0_1,i-1 = w^0_2,i-1 = …  = w^0_i-1,i-1 = w^0_i+1,i = w^0_i+2,i = …  = w^0_m,i
 
	for all 1 < i < m.
 
Set 

    w_i = 
    	w^0_i+1,i,     1 ≤ i < m,
    
    	w^0_1, m-1,     i = m.

Then w_1 < … < w_m. Indeed, if m = 2, since  satisfies HM1 and HM2,

    w_1    = w^0_2,1 = λ_(τ^0_2, τ^0_2 ∪{w^0_2,1}) = λ_(d^0_2x) =  λ_(d^0_2x)
       < λ_(d^0_1x) = λ_(d^0_1x) = λ_(τ^0_1, τ^0_1 ∪{w^0_1,1}) = w^0_1,1 = w_2.

If m≥ 3, we have 

    w_m-1 = w^0_m,m-1 = w^0_m-2,m-2 < w^0_m-2,m-1 = w^0_1,m-1 = w_m

and

    w_i = w^0_i+1, i = w^0_i+2,i < w^0_i+2,i+1 = w_i+1

for 1≤ i  < m-1.

We have 

    d^0_m(τ, τ∪{w_1 < …  < w_m})
       = (τ, τ∪{w_1 <  … < w_m-1})
       = (τ, τ∪{w^0_2,1 < … <  w^0_m, m-1})
       = (τ, τ∪{w^0_m,1 < … <  w^0_m, m-1})
       = (τ^0_m, σ^0_m)
       = d^0_mx

and 

    d^1_m(τ, τ∪{w_1 < …  < w_m})
       = (τ∪{w_m}, τ∪{w_1 <  … < w_m})
       = (τ∪{w_m}, τ∪{w_m}∪{w_1 <  … < w_m-1})
       = (τ∪{w^0_1,m-1}, τ∪{w^0_1,m-1}∪{w^0_2,1 <  … < w^0_m,m-1})
       = (τ^1_m, τ^1_m ∪{w^0_m,1 <  … < w^0_m,m-1})
       = (τ^1_m, τ^1_m ∪{w^1_m,1 <  … < w^1_m,m-1})
       = (τ^1_m, σ^1_m)
       = d^1_mx.

For 1 ≤ i < m, we have

    d^0_i(τ, τ∪{w_1 < … < w_m})
       = (τ, τ∪{w_1 < … w_i-1 < w_i+1 < … < w_m-1 <  w_m})
       = (τ, τ∪{w^0_2,1 < … < w^0_i,i-1 < w^0_i+2,i+1 < … <  w^0_m, m-1 < w^0_1,m-1})
       = (τ, τ∪{w^0_i,1 < … < w^0_i,i-1 < w^0_i,i < … <  w^0_i, m-2 < w^0_i,m-1})
       = (τ^0_i, σ^0_i)
       = d^0_ix

and 

    d^1_i(τ, τ∪{w_1 < … < w_m})
       = (τ∪{w_i}, τ∪{w_1 < … <  w_m})
       = (τ∪{w^0_i+1,i}, τ∪{w^0_2,1 <  … <  w^0_m, m-1 < w^0_1,m-1})
       = (τ∪{w^0_i+1,i}, τ∪{w^0_i+1,i}
             ∪{w^0_2,1 < … < w^0_i,i-1 < w^0_i+2,i+1 < … <  w^0_m, m-1 < w^0_1,m-1})
       = (τ∪{w^0_i+1,i}, τ∪{w^0_i+1,i}
             ∪{w^0_i,1 < … < w^0_i,i-1 < w^0_i,i < … <  w^0_i, m-2 < w^0_i,m-1})
       = (τ^1_i, τ^1_i∪{w^1_i,1 < … < w^1_i,i-1 < w^1_i,i < … <  w^1_i, m-2 < w^1_i,m-1})
       = (τ^1_i, σ^1_i)
       = d^1_ix.

Since  satisfies HM3, it follows that x = (τ, τ∪{w_1 < … < w_m}) ∈ P_m. Thus, (P_)_m = P_m.




§ ACCESSIBILITY
 

A state v in HDA is said to be reachable if there exists a path, i.e., a sequence of consecutive edges, from the initial state to v. An HDA in which all states are reachable is called accessible. Unreachable states are of very limited interest for the analysis of concurrent systems, since the executions of a system only pass through reachable states. Therefore, it makes sense to model only the accessible part of the  state space of a system. Another important reason for doing so is the state explosion problem: the state space of a concurrent system can easily become very large, and including unreachable states in the model would dramatically aggravate this problem. Unfortunately, the HDA  defined in the previous section is highly inaccessible. In this section, we show that it is possible to modify  to obtain an accessible HDA of the same homotopy type. More precisely, we prove the following theorem:

 
	Let  be a bideterministic HDA which is the HDA model of its 1-skeleton with respect to a strict total order on Σ_. Suppose that  is connected, i.e., |P_| is path-connected, and that  has only a finite number of unreachable states (e.g.,  is finite). Then there exists an accessible and bideterministic HDA  which is the HDA model of its 1skeleton with respect to a strict total order on Σ_ and satisfies |P_| ≃ |P_|.


For the proof, we may suppose that  is not accessible. Clearly, it is enough to show that there exists a bideterministic HDA  with less unreachable states than  that is the HDA model of its 1-skeleton with respect to a strict total order on Σ_ and satisfies |P_| ≃ |P_|. We show first that  admits an edge from an unreachable to a reachable state. Suppose that there is no such edge. Let v be an unreachable state. Since  is connected, there is a sequence of vertices I_ = v_1, v_2, …, v_k = v such that for each 1 ≤ i < k there exists an edge between v_i and v_i+1. Inductively, all v_i are reachable, which is impossible. 


Let e be an edge of  from an unreachable state v to a reachable state w. If w = I_, we define  to be the same as  but with I_ = v. Suppose that w ≠ I_. Let λ_(e) = a, and let ω = (x_1,…, x_k) be a path from I_ to w with no repeated vertices, e.g., a shortest possible path. We view ω as a morphism of precubical sets 0, k → P_, where the precubical interval p, q (p,q ∈, p≤ q) is the precubical set defined by p,q _0 = {p,… , q}, p,q _1 =  {[p,p+1], … , [q- 1,q]}, d_1^0[j-1,j] = j-1, d_1^1[j-1,j] = j, and p,q _n = ∅ for n > 1.




 §.§ The HDA 



We first extend  to an HDA  such that |P_| ≃ |P_|. We define the precubical set P_ by the pushout diagram

    0, k⊗{2}[r, "≅"] [d, hook]     0, k[r, "ω"]      P_[d, hook]
     -1,0⊗{1}∪ 0, k⊗ 1,2 [rr, "ξ"']
    	       P_.

Since the geometric realizations of the precubical sets on the left are contractible and, as is well known, the geometric realization functor preserves colimits, the inclusion |P_| ↪ |P_| is a homotopy equivalence. Let Σ_ = Σ_∪{c} for some element c ∉Σ_. We extend the labeling function of  to  by setting λ_(ξ(i,[1,2])) = c (i ∈{0, …, k}),  λ_(ξ([i-1,i],1)) = λ_(x_i) (i ∈{1, …, k}), and λ_(ξ([-1,0],1)) = a. The initial state of  is I_ = ξ(-1,1).






 
	 is  bideterministic and has the same unreachable states as .



	Since all edges of  that are not edges of  start in vertices of  that are not vertices of  and in no such vertex start two edges with the same label,  is deterministic. Since ω has no repeated vertices, no two edges of  that are not edges of  end in the same vertex. Since any such edge that ends in a vertex of  has label c, it follows that  is codeterministic. 
	
	Since I_ is reachable in , all states of  that are reachable in  are also reachable in . On the other hand, since any path in  from I_ to a state of  intersects ω, all states of  that are reachable in  are also reachable in . Since all states in ξ( -1,0⊗{1}∪ 0, k⊗ 1,2 ) are reachable in , it follows that  has the same unreachable states as .




Let < be the strict total order on Σ_ with respect to which  is the HDA model of its 1-skeleton. We extend < to a strict total order on Σ_ by setting b< c for all b∈Σ_.  

 
 is the HDA model of _≤ 1 with respect to <.	



	Condition HM1 is trivially satisfied. Since  satisfies HM2 and, for all i ∈{1,…, k}, 
	
    λ_(d^0_2ξ([i-1,i],[1,2]))    =  λ_(ξ(d^0_2([i-1,i],[1,2])))
       = λ_(ξ([i-1,i],1))
       = λ_(x_i)
       <  c
       = λ_(ξ(i-1,[1,2]))
       = λ_(ξ(d^0_1([i-1,i],[1,2])))
       = λ_(d^0_1ξ([i-1,i],[1,2])),

	 satisfies HM2. Let x,y ∈ (P_)_m (m≥ 2) such that d^k_rx = d^k_ry for all r ∈{1,… ,m} and k ∈{0,1}. Since  satisfies HM3, x = y if x, y ∈ (P_)_m. If x ∉ (P_)_m, then m = 2 and x = ξ([i-1,i],[1,2]) for some i ∈{1, …, k}. Since x is the only 2-cube of  having ξ([i-1,i],1) in its boundary, y = x. Hence  satisfies HM3. Let  be an HDA with P_⊆ P_ that satisfies HM1–HM3. Since  is the HDA model of _≤ 1, all m-cubes of  (m≥ 2)  with faces in  belong to . Let x ∈ (P_)_2 such that at least one edge of x does not belong to . Since every edge that starts in a vertex of  belongs to , d^0_1d^0_2x is not a vertex of . Hence d^0_1d^0_2x = ξ(i,1) for some i ∈{-1,…, k}. Since λ_(d^0_2x)<  λ_(d^0_1x), we have d^0_1x ≠ d^0_2x and therefore 0 ≤ i < k. Since λ_(ξ([i,i+1],1)) < λ_ (ξ(i,[1,2])) = c, we have d^0_1x = ξ(i,[1,2]) and d^0_2x = ξ([i,i+1],1). Since λ_(d^1_1x) = λ_(d^0_1x) = c, we have d^1_1x = ξ(i+1,[1,2]). Since, by Lemma <ref>, _≤ 1 = _≤ 1 is deterministic, d^1_2x = x_i+1 because d^1_2x starts in ξ(i,2) = d^0_1x_i+1 and λ_(d^1_2x) = λ_(d^0_2x) = λ_(ξ([i,i+1],1)) = λ_(x_i+1). Since  satisfies HM3, x = ξ([i,i+1],[1,2]) ∈ (P_)_2. Suppose that there exist an integer m≥ 3 and an element y ∈ (P_)_m such that at least one face of y does not belong to . Then d^0_1⋯ d^0_my is not a vertex of . Hence d^0_1⋯ d^0_my = ξ(i,1) for some i. Since, by <cit.>, for all 1 ≤ i < j ≤ m, 
	
    λ_(d^0_1⋯ d^0_i-1d^0_i+1⋯ d^0_mx) < λ_(d^0_1⋯ d^0_j-1d^0_j+1⋯ d^0_mx),

	m different edges start in ξ(i,1). This is not the case. Thus, = and  satisfies HM4.

 
 


 §.§ The HDA 
 



We now extend  to an HDA  that still satisfies |P_| ≃ |P_| but in which v is reachable. Let i be the largest index in {0, …, k} such that λ_(ξ([i-1,i],1)) = a. Since  is codeterministic, λ_(ξ([k-1,k],1)) = λ_(x_k) ≠ a. Hence i < k. We define the precubical set P_ by the pushout diagram

    i, k+1⊗{1}∪{i,k+1}⊗ 0,1[r, "ν"] [d, hook]      P_[d, hook]
     i, k+1⊗ 0,1 [r,"χ"']
    	     P_

where ν is the unique morphism of precubical sets such that ν([j-1,j],1) = ξ([j-1,j],1) (i < j ≤ k), ν([k,k+1],1) = ξ(k,[1,2]), ν(i,[0,1]) = ξ([i-1,i],1), and ν(k+1,[0,1]) = e. Note that ν is injective. Since the geometric realizations of the precubical sets on the left are contractible, the inclusion |P_| ↪ |P_| is a homotopy equivalence. Hence |P_| ≃ |P_|. We set I_ = I_ and Σ_ = Σ_ and extend the labeling function of  to  by setting λ_(χ(j,[0,1])) = a, λ_(χ([j-1,j],0)) = λ_(x_j) (i < j ≤ k),  and λ_(χ([k,k+1],0)) = c. 




 
	 is bideterministic and has less unreachable states than .



	In each vertex of  that is not a vertex of  start exactly two edges, one with label a and the other with a different label. The only vertex of  in which starts an edge of  that is not an edge of  is ν(i,0) = ξ(i-1,1). By definition of i, the label of this edge is different from a. Since i < k, this label is also different from c. Hence the edges starting in ν(i,0) = ξ(i-1,1) have different labels. Since, by Lemma <ref>,  is deterministic, it follows that  is deterministic. Since no two edges of  that are not edges of  end in the same vertex, no edge in  with label c ends in v, and the edges ξ ([i,i+1],1), …, ξ ([k-1,k],1) have labels different from a,  is codeterministic. 
	
	All states of  that are reachable in  are also reachable in . Since all states in χ( i, k+1⊗ 0,1 ) are reachable in  and, in particular, v = χ(k+1,0) is reachable in , the number of unreachable states of  is less than the number of unreachable states of  and hence, by Lemma <ref>, of .




 §.§ The HDA 


Unfortunately, we cannot guarantee that  is the HDA model of its skeleton, because the labels of the edges of the squares added to  might be related in the wrong way. In the final HDA , we solve this problem. We set (P_)_m = (P_)_m for all m and define the face maps of P_ by

    ∂ ^k_i x = {[                                      d^k_3-ix, x ∈ (P_)_2 ∖ (P_)_2,  λ_(d^0_1x) < λ_(d^0_2x),;                                        d^k_ix,                                              . ].

Then P_ is a precubical set and |P_| ≈ |P_|. Hence |P_| ≃ |P_|. We set I_ = I_ = I_, Σ_ = Σ_ = Σ_, and λ_ = λ_. Then  is an HDA with _≤ 1 = _≤ 1. By Lemma <ref>,  is bideterministic and has less unreachable states than . To finish the proof of Theorem <ref>, it remains to show that  is the HDA model of its 1-skeleton. This is done in Proposition <ref> below. 

 
	Let  be an HDA which satisfies HM2 with respect to _≤ 1 and a strict total order on Σ_, and let x be an element of P_ of degree m≥ 3. Then d^k_px ≠ d^l_qx for all 1 ≤ p < q ≤ m and k, l ∈{0,1}.




    Suppose that d^k_px = d^l_qx for some 1 ≤ p < q ≤ m and k, l ∈{0,1}. Then 
	
    d^0_1 ⋯ d^0_p-1d^k_pd^0_p+2⋯ d^0_mx = d^0_1 ⋯ d^0_p-1d^0_p+1⋯ d^0_m-1d^k_px
       = d^0_1 ⋯ d^0_p-1d^0_p+1⋯ d^0_m-1d^l_qx
    		= d^0_1 ⋯ d^0_p-1d^0_p+1⋯ d^0_q-1d^l_qd^0_q+1⋯ d^0_mx.

	By the arguments given in <cit.>, it follows that 
	
    λ_(d^0_1 ⋯ d^0_pd^0_p+2⋯ d^0_mx)    = λ_(d^0_1 ⋯ d^0_p-1d^0_p+1⋯ d^0_mx)
       < λ_(d^0_1 ⋯ d^0_pd^0_p+2⋯ d^0_mx),

	which is impossible.




 
	 is the HDA model of _≤ 1 with respect to <. 



	By construction,  satisfies HM1 and HM2. HM3 can be shown in a similar way as for , see Lemma <ref>. Let  be an HDA that contains  and satisfies HM1–HM3 with respect to _≤ 1 and <. Since, by Lemma <ref>,  is the HDA model of _≤ 1, all m-cubes of  (m≥ 2)  with faces in  belong to . Let x ∈ (P_)_2 such that at least one edge of x does not belong to . Since every edge with endpoints in  belongs to , x has a vertex that does not belong to . Since λ_(∂^1_2x)< λ_(∂^1_1x), we have ∂^1_1x ≠∂^1_2x. Since in no vertex that does not belong to  ends more than one edge, it follows that ∂^1_1∂^1_2x ∈ (P_)_0. This implies that if ∂^0_1∂^0_2x ∈ (P_)_0, then ∂^0_1∂^0_2x = χ(i,0). Indeed, in this case, ∂^1_1∂^0_1x ∉ (P_)_0 or ∂^1_1∂^0_2x ∉ (P_)_0, and so ∂^0_1∂^0_2x is a vertex of  in which starts an edge that ends in a vertex of (P_)_0∖ (P_)_0. The only such vertex is χ(i,0). Thus, there exists j ∈{i, …, k} such that ∂^0_1∂^0_2x = χ(j,0).
	
	Suppose that ∂^0_1∂^0_2x = χ(j,0) with i < j ≤ k. Since λ_(∂^0_2x) <  λ_(∂^0_1x), we have ∂^0_1x ≠∂^0_2x. Therefore there exists r ∈{1,2} such that ∂^0_rx = χ(j,[0,1]) and ∂^0_3-rx = χ([j,j+1],0). Since λ_(∂^1_rx) = λ_(∂^0_rx) = a, we have ∂^1_rx = χ(j+1,[0,1]). Since _≤ 1 = _≤ 1 is deterministic, we have ∂^1_3-rx = χ([j,j+1], 1) because ∂^1_3-rx starts in χ(j,1) = ∂^0_1χ([j,j+1], 1) and λ_(∂^1_3-rx) = λ_(∂^0_3-rx) = λ_(χ([j,j+1],0)) = λ_(χ([j,j+1],1)).
	Since  satisfies HM3 and < is asymmetric, it follows that x = χ([j,j+1],[0,1]) ∈ (P_)_2. 
	
	Suppose now that ∂^0_1∂^0_2x = χ(i,0). Since λ_(∂^0_2x)< λ_(∂^0_1x), we have ∂^0_1x ≠∂^0_2x. The edges starting at χ(i,0) are χ(i,[0,1]) and χ([i,i+1],0), and  ξ(i-1, [1,2]) when i > 0. Since all edges starting at the endpoints of χ(i,[0,1]) and ξ(i-1, [1,2]) are edges of , there exists r ∈{1,2} such that ∂^0_rx is χ(i,[0,1]) or ξ(i-1, [1,2])}, and ∂^0_3-rx = χ([i,i+1],0). Since all edges starting at the endpoints of χ(i,[0,1]) and ξ(i-1, [1,2]) end in reachable vertices of  and there exists no edge starting in a reachable vertex of  and ending in χ(i+2, 0), we have ∂^1_1∂^1_2x = χ(i+1,1), ∂^1_rx= χ(i+1,[0,1]), ∂^0_rx= χ(i,[0,1]), and ∂^1_3-rx = χ([i,i+1],1). Since  satisfies HM3 and < is asymmetric, it follows that x = χ([i,i+1],[0,1]) ∈ (P_)_2. 
	
	Suppose that there exists an element y ∈ (P_)_3 such that at least one face of y, say ∂^l_jy, does not belong to . Then ∂^l_jy = χ([r,r+1],[0,1]) for some i ≤ r ≤ k. Since, for some s ∈{1,2}, 
	
    χ([r,r+1],0)    = ∂^0_sχ([r,r+1],[0,1]) = ∂^0_s∂^l_jy = ∂^l_j-1∂^0_sy,     s <j,
    ∂^l_j∂^0_s+1y,     s ≥ j,

	Lemma <ref> implies that (χ([r,r+1],0) is an edge of two distinct faces of y. Since χ([r,r+1],[0,1]) is the only 2-cube of  having (χ([r,r+1],0) as an edge, this is impossible. 
	
	A simple induction now shows that (P_)_m = (P_)_m for all m ≥ 3. It follows that  satisfies HM4. 








§ SHARED-VARIABLE SYSTEMS
 

In this section, we consider shared-variable systems given by program graphs and establish our main result:

 
	There exists a shared-variable system such that the geometric realization of its HDA model has the homotopy type of the polyhedron |K|.




 §.§ Program graphs and shared-variable systems
 

Let V be a set of variables. The domain of a variable x, i.e., the set of its possible values, will be denoted by D_x. A program graph over V is a tuple 
    (L, A, T, g, 
    )

where L is a set of locations or local states, A is a finite set of actions, i.e., functions ∏_x ∈ V D_x →∏_x ∈ V D_x, T⊆ L × A  × L is a set of transitions, g is a function that specifies a guard condition, i.e., a subset of  ∏_x ∈ V D_x, for each transition, and ∈ L is an initial location (cf. <cit.>). A shared-variable system over V is a tuple (_1, …, _n, η) consisting of program graphs _i and an initial evaluation η∈∏_x ∈ V D_x. 





 §.§ The HDA model of a shared-variable system


Consider a shared-variable system (_1, …, _n, η) over a set of variables V, and write  
_i = (L_i, A_i, T_i, g_i, _i). The state graph of (_1, …, _n, η) is the 1-truncated   precubical set Q where 

    Q_0 = L_1 ×⋯× L_n ×∏_x ∈ V D_x,
 

    Q_1 = ⋃_i∈{1,…,n}
    t ∈ T_i L_1 ×⋯×  L_i-1×{t}× L_i+1×⋯× L_n × g_i(t),

and for y = (l_1,…, l_i-1,t,l_i+1, …, l_n,γ)∈ Q_1 with t = (l^0_t, a_t, l^1_t), 
    d^0_1y = (l_1,…, l_i-1,l^0_t,l_i+1, …, l_n,γ)
 and  
    d^1_1y = (l_1,…, l_i-1,l^1_t,l_i+1, …, l_n,a_t(γ)).

The initial state of the system is the state
I  = (_1, … , _n, η). 
The transition system model of  (_1, …, _n, η) is the transition system  where P_ is the largest precubical subset of Q such that all states are reachable from the initial state I, I_ = I, Σ_ = ⋃_i= 1^n {i}× A_i, and the label of an edge y = (l_1,…, l_i-1,t,l_i+1, …, l_n,γ) ∈ (P_)_1 with t = (l^0_t, a_t, l^1_t) is given by λ_(y) = (i,a_t). The HDA model of (_1, …, _n, η) is the HDA model of  with respect to the relation R on Σ_ given by 
    (i,a)  R  (j,b)  i < j.
 



	In practice, the transition system model of a shared-variable system can be constructed without handling unreachable states using a procedure such as the one described in the reference manual of the Spin model checker <cit.>. HDA models of shared-variable systems written in Promela, the process description language of Spin, can be computed using the tool pg2hda <cit.>.




 §.§ Proof of Theorem <ref>


Since K is connected and |K| ≈ |P| = |P_| by Theorem <ref>, the HDA  is also connected. By Proposition <ref> and Theorems <ref> and  <ref>, there exists an accessible and deterministic HDA  which is the HDA model of its 1-skeleton with respect to a total order on Σ_ and satisfies |P_| ≃ |P_| ≈ |K|. 

Suppose that Σ_ = {a_1 < … < a_n}. Consider a single variable x with domain D_x = (P_)_0, and let (_1, …, _n, η) be the shared-variable system over V = {x} where η = I_ and the program graphs _i = (L_i,A_i, T_i, g_i, _i) are defined by

    
  * L_i = {0};
    
  * A_i = {a̅_i} where a̅_i(v) = {[                                  d^1_1y, ∃  y ∈ (P_)_1 : d^0_1y = v, λ_(y) = a_i,;                                       v,                                          ].
    
  * T_i = {(0,a̅_i,0)};
    
  * g_i(0,a̅_i,0) = {d^0_1y |  y ∈ (P_)_1, λ_(y) = a_i};
    
  * _i = 0.		

Since  is deterministic, the action a̅_i is well defined. Let Q be the state graph of (_1, …, _n, η). We have 
    (P_)_0 ≅ L_1 ×…× L_n × D_x = Q_0.

Since  is deterministic, the map 

    d^0_1{y ∈ (P_)_1 | λ_(y) = a_i}   →{d^0_1y |  y ∈ (P_)_1, λ_(y) = a_i} = g_i(0,a̅_i,0)

is a bijection for each i. Hence	

    (P_)_1    = ⋃_i∈{1,…,n}{y ∈ (P_)_1 | λ_(y) = a_i}
       ≅⋃_i∈{1,…,n} L_1 ×⋯×  L_i-1×{(0,a̅_i,0)}× L_i+1×⋯× L_n × g_i(0,a̅_i, 0)
       = Q_1.

Since for y∈ (P_)_1 with λ_(y) = a_i we have 

    d^0_1(0, …, 0, (0,a̅_i,0), 0, …, 0, d^0_1y) = (0, …, 0, d^0_1y)

and 

    d^1_1(0, …, 0, (0,a̅_i,0), 0, …, 0, d^0_1y) = (0, …, 0, a̅_i(d^0_1y)) = (0, …, 0, d^1_1y),

the precubical sets (P_)_≤ 1 and Q are isomorphic.

Let  be the transition system model of (_1, …, _n, η). Since the initial state of the system, I = (0, …, 0, I_), corresponds to I_ under the isomorphism (P_)_≤ 1≅ Q and  is accessible, all states of Q are reachable from I. Hence P_ = Q. We have 

    Σ_ = {a_1, …, a_n}≅{(1, a̅_1), … , (n,a̅_n)} = Σ_.
 
Since for an edge y ∈ (P_)_1 with λ_(y) = a_i we have 

    λ_(0,…, 0, (0, a̅_i, 0),0, …, 0, d^0_1y) = (i, a̅_i),
 
it follows that the transition systems _≤ 1 and  are isomorphic.

Let  be the HDA model of (_1, …, _n, η). Then  is the HDA model of  with respect to the relation 
R on Σ_ given by 
    (i,a̅_i)  R  (j,a̅_j)  i < j  a_i < a_j.

By <cit.>, it follows that the HDAs  and  are isomorphic. In particular, |P_| ≈ |P_| ≃ |K|. 0pt


apalike
	


