Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

On the homology language of HDA models of transition systems

On the homology language of HDA models of transition systems Given a transition system with an independence relation on the alphabet of labels, one can associate with it a usually very large symmetric higher-dimensional automaton. The purpose of this paper is to show that by choosing an acyclic relation whose symmetric closure is the given independence relation, it is possible to construct a much smaller nonsymmetric HDA with the same homology language. Keywords Higher-dimensional automata · Transition system · Homology language Mathematics Subject Classification 55N35 · 68Q85 1 Introduction Higher-dimensional automata are a powerful combinatorial-topological model for con- current systems. A higher-dimensional automaton (HDA) is a precubical set (i.e., a cubical set without degeneracies) with an initial state, a set of final states, and a label- ing on 1-cubes such that opposite edges of 2-cubes have the same label (van Glabbeek 2006;Pratt 1991). An HDA is thus a (labeled) transition system (or an ordinary automa- ton) with a supplementary structure consisting of two- and higher-dimensional cubes. The transition system represents the states and transitions of a concurrent system. An n-cube in an HDA indicates that the n transitions starting at its origin are indepen- dent in the sense that they may occur in any order, or even simultaneously, without any observable difference. It has been shown in van Glabbeek (2006) that higher- dimensional automata are more expressive than the principal traditional models of concurrency. B Thomas Kahl kahl@math.uminho.pt Centro de Matemática, Universidade do Minho, Campus de Gualtar, 4710-057 Braga, Portugal 123 T. Kahl The fact that the two- and higher-dimensional cubes in an HDA represent inde- pendence of transitions suggests that the higher-dimensional topology of an HDA contains global information on independence of processes and components of the modeled concurrent system. In Kahl (2021), the homology language has been devised as a homological tool to describe this global independence structure of an HDA. The homology language of an HDA is defined to be the image of the homomorphism induced in homology by a certain labeling chain map that leads from the cubical chain complex of the HDA to the exterior algebra on the alphabet of labels (see Sect. 3). The homology language can be computed and analyzed using software (Kahl 2018). Transition systems are arguably the most fundamental model for concurrent sys- tems. A natural way to turn a transition system into an HDA is to fill in empty squares and higher-dimensional cubes (van Glabbeek 2006; Gaucher 2010; Goubault and Mimram 2012; Kahl 2019). This approach requires some concept of independence in order to decide which cubes to fill in. Such a concept of independence may be given by an independence relation—i.e., an irreflexive and symmetric relation—on the alpha- bet of action labels. Independence relations play a fundamental role in trace theory in the sense of Mazurkiewicz (1987). Asynchronous transition systems (Winskel and Nielsen 1995) are an important example of transition systems that come equipped with an independence relation on the set of labels. HDAs constructed from transition systems using a cube filling procedure based on a symmetric concept of independence, such as an independence relation on the set of labels, are usually very large because an empty n-cube representing the execution of n independent actions is filled in n! times. From a computational point of view, it is therefore desirable to have a way to produce smaller HDA models of transition systems. It has been shown in Kahl (2019) that using a cube filling rule based on an asymmetric rather than an independence relation on the alphabet, one can construct an HDA model of a transition system where the independence of n actions in a state is represented by a single n-cube (at least if the transition system under consideration is deterministic). It is, of course, not to be expected that two HDAs constructed using different filling rules from the same transition system will be equivalent in a meaningful sense. Every independence relation on an alphabet is the symmetric closure of an acyclic relation, i.e., a relation that is acyclic when seen as a graph (see Sect. 4). The purpose of this paper is to establish that the HDAs constructed from a transition system using cube filling rules based, respectively, on an independence relation on the alphabet and a generating acyclic relation have the same homology language. The two HDAs may therefore be regarded as equivalent from the point of view of their independence structures. As we will show in Sect. 5, the HDA constructed using the independence relation is the free symmetric HDA generated by the one constructed using the acyclic relation. The latter is thus a significantly smaller HDA model of the given transition system than the former. 123 On the homology language of HDA models of transition systems 2 Precubical sets and HDAs This section presents fundamental material on precubical sets, higher-dimensional automata, and their symmetric variants. 2.1 Precubical sets A precubical set is a graded set P = (P ) with face maps n n≥0 d : P → P (n > 0, k = 0, 1, i = 1,..., n) n n−1 satisfying the cubical identities k l l k d d = d d (k, l = 0, 1, i < j ). i j j −1 i If x ∈ P , we say that x is of degree or dimension n. The elements of degree n are called the n-cubes of P. The elements of degree 0 are also called the vertices of P, and the 1-cubes are also called the edges of P.The ith starting edge of a cube x of degree n > 0 is the edge 0 0 0 0 e x = d ... d d ... d x . 1 i −1 i +1 n A precubical subset of a precubical set is a graded subset that is stable under the face maps. The n-skeleton of a precubical set P is the precubical subset P defined ≤n by (P ) = P for m ≤ n and P =∅ else. ≤n m m m A morphism of precubical sets is a morphism of graded sets that is compatible with the face maps. The category of precubical sets can be seen as the presheaf category of op functors  → Set where  is the small subcategory of the category of topological spaces whose objects are the standard n-cubes [0, 1] (n ≥ 0) and whose nonidentity k n n+1 morphisms are composites of the coface maps δ :[0, 1] →[0, 1] (k ∈{0, 1}, n ≥ 0, i ∈{1,..., n + 1}) given by δ (u ,..., u ) = (u ,..., u , k, u ..., u ). 1 n 1 i −1 i n The geometric realization of a precubical set P is the quotient space ⎛ ⎞ ⎝ ⎠ |P|= P ×[0, 1] / ∼ n≥0 where the sets P are given the discrete topology and the equivalence relation is generated by k k n (d x , u) ∼ (x,δ (u)), x ∈ P , u ∈[0, 1] , i ∈{1,..., n + 1}, k ∈{0, 1}. n+1 i i The geometric realization of a morphism of precubical sets f : P → Q is the continuous map | f |: |P|→|Q| given by | f |([x , u]) =[ f (x ), u]. 123 T. Kahl 2.2 The precubical set of permutations The family of symmetric groups S = (S ) (with S ={id }) is a precubical set n n≥0 0 ∅ with respect to the face maps given by −1 θ( j ), j <θ (i ), θ ( j)< i , −1 θ( j ) − 1, j <θ (i ), θ ( j)> i , d θ( j ) = −1 ⎪ θ( j + 1), j ≥ θ (i ), θ ( j + 1)< i , −1 θ( j + 1) − 1, j ≥ θ (i ), θ ( j + 1)> i (see Kahl (2022) and compare Krasauskas (1987), and Fiedorowicz and Loday (1991)). 0 1 Since, by definition, d θ = d θ, we may simplify the notation by setting i i 0 1 d θ = d θ = d θ. i i Since S ={id}, the two elements of S have the same faces. In degrees ≥ 3, 1 2 permutations are determined by their faces: Proposition 2.1 Let n ≥ 3, and let σ, θ ∈ S such that d σ = d θ for all i ∈{1,..., n}. n i i Then σ = θ. Proof It follows from Kahl (2022, Lemma 3.3) that it is enough to show that there −1 exists an r such that σ(r ) = θ(r ). Suppose that this is not the case. Set i = σ (n) −1 and j = θ (n). Then i , j < n. Indeed, suppose that i = n. Then for 1 ≤ r ≤ n − 1, −1 d σ(r ) = σ(r ) because r < n = σ (n), σ(r ) ≤ n, and σ(r ) = σ(n) = n. Since −1 θ(r ) = σ(r ) and θ(r ), θ (r + 1) ≤ n,wehave r ≥ θ (n), θ(r + 1)< n, and σ(r ) = d σ(r ) = d θ(r ) = θ(r + 1). n n −1 −1 In particular, j = θ (n) ≤ 1. Hence j = 1 and θ(1) = n. Set s = σ (1). Since −1 σ(s) = σ(n), s < n. Since θ(s + 1) = σ(s) = 1, θ (1) = s + 1. Since the values of σ are ≥ 1, we have −1 σ(1) − 1, 1 <σ (1) = s, d σ(1) = σ(2) − 1, 1 = s. Since n > 2, we have σ(1), σ (2) = σ(n) = n and therefore d σ(1) ≤ n − 2. On the −1 other hand, 1 < s + 1 = θ (1) and θ(1) = n > 1 and therefore n − 2 ≥ d σ(1) = d θ(1) = θ(1) − 1 = n − 1, 1 1 which is impossible. It follows that i < n. An analogous argument shows that j < n. −1 Hence 1 ≤ i , j ≤ n − 1. We show that i < j. Since i ≥ i = σ (n), σ(i + 1) ≤ n, and σ(i + 1) = σ(i ) = n,wehave d σ(i ) = σ(i + 1). Hence d θ(i ) = σ(i + 1) = n n θ(i + 1). Since θ(i + 1) ≤ n, it follows that i < j. Analogously, j < i. Since this is impossible, there must exist an r such that σ(r ) = θ(r ). 123 On the homology language of HDA models of transition systems For later use, we state the following fact from Kahl (2022): Proposition 2.2 (Kahl 2022, Prop. 3.6(i)) Let P be a precubical set, and let n ≥ 2, 1 ≤ i < j ≤ n, k, l ∈{0, 1},x ∈ P , and θ ∈ S . Then n n k l l k d d x = d d x . d θ(i ) θ( j ) d θ( j −1) θ(i ) θ( j ) θ(i ) 2.3 Symmetric precubical sets A symmetric precubical set is a precubical set P equipped with a crossed action of S on P, i.e., a morphism of graded sets S × P − → P, (θ , x ) → θ · x such that • for all n ≥ 0 and x ∈ P , id · x = x; • for all n ≥ 0, σ, θ ∈ S , and x ∈ P , (σ · θ) · x = σ · (θ · x ); n n • for all n ≥ 1, θ ∈ S , x ∈ P , i ∈{1,..., n}, and k ∈{0, 1}, n n k k d (θ · x ) = d θ · d x . i −1 θ (i ) Symmetric precubical sets form a category, in which the morphisms are morphisms of precubical sets that are compatible with the crossed actions. We remark that the op category of symmetric precubical sets is isomorphic to the presheaf category Set where  is the subcategory of the category of topological spaces whose objects are the standard n-cubes [0, 1] (n ≥ 0) and whose morphisms are composites of the coface maps δ defined above and the permutation maps n n t :[0, 1] →[0, 1] ,(u ,..., u ) → (u ..., u )(n ≥ 0,θ ∈ S ) θ 1 n θ(1) θ(n) n (cf. Grandis and Mauri (2003); Fahrenberg (2005); Gaucher (2010); Goubault and Mimram (2012)). The free symmetric precubical set generated by a precubical set P is the symmetric precubical set SP defined by • SP = S × P (n ≥ 0); n n n k k • d (θ , x ) = (d θ, d x)(n ≥ 1,θ ∈ S , x ∈ P , 1 ≤ i ≤ n, k ∈{0, 1}); i n n −1 θ (i ) • σ · (θ , x ) = (σ · θ, x)(n ≥ 0,σ,θ ∈ S , x ∈ P ). n n The free symmetric precubical set is functorial, and the functor P → SP from the category of precubical sets to the category of symmetric precubical sets is left adjoint to the forgetful functor. 2.4 Higher-dimensional automata Throughout this paper, we consider a fixed alphabet .A higher-dimensional automaton (HDA) over  is a tuple Q = (P, ı, F,λ) 123 T. Kahl where P is a precubical set, ı ∈ P is a vertex, called the initial state, F ⊆ P is a 0 0 (possibly empty) set of final states, and λ : P →  is a map, called the labeling 0 1 function, such that λ(d x ) = λ(d x ) for all x ∈ P and i ∈{1, 2} (van Glabbeek i i 2006). We say that an HDA Q = (P , ı , F ,λ ) is a sub-HDA of Q and write Q ⊆ Q if P is a precubical subset of P, ı = ı, F = F ∩ Q , and λ = λ| .The n-skeleton of Q is the sub-HDA Q = (P , ı, F,λ| ). Higher-dimensional automata ≤n ≤n (P ) ≤n 1 form a category, in which a morphism from an HDA Q = (P, ı, F,λ) to an HDA Q = (P , ı , F ,λ ) is a morphism of precubical sets f : P → P such that f (ı ) = ı , f (F ) ⊆ F , and λ ( f (x )) = λ(x ) for all x ∈ P . A symmetric HDA is an HDA Q = (P, ı, F,λ) equipped with a crossed action of S on P. Symmetric HDAs form a category, in which the morphisms are mor- phisms of HDAs that also are morphisms of symmetric precubical sets. The free symmetric HDA generated by an HDA Q = (P, ı, F,λ) is the symmetric HDA SQ = (SP,(id, ı ), S × F,μ) where μ(id, x ) = λ(x)(x ∈ P ) and the crossed 0 1 action is the one of SP. The assignment Q → SQ defines a functor from the category of HDAs to the category of symmetric HDAs, which is left adjoint to the forgetful functor. 3 The homology language and free symmetric HDAs In this section, we recall the definition of the homology language of an HDA from Kahl (2021) and show, as a first contribution of this paper, that an HDA and the free symmetric HDA generated by it have the same homology language. We work over a fixed principal ideal domain, which we suppress from the notation. 3.1 Cubical chains and cubical homology The cubical chain complex of a precubical set P is the nonnegative chain complex C (P) where C (P) is the free module generated by P and the boundary operator ∗ n n d : C (P) → C (P) is given by n n−1 i 0 1 dx = (−1) (d x − d x ), x ∈ P (n > 0). i i i =1 The cubical homology of P, denoted by H (P), is the homology of C (P). ∗ ∗ 3.2 The homology language of an HDA Let Q = (P, ı, F,λ) be an HDA over . Consider the exterior algebra on the free module generated by , (). Recall that this is the quotient of the tensor algebra on the free module on  by the two-sided ideal generated by all elements of the form x ⊗ x where x runs through the free module on  (see Bourbaki (1974)for more details). The exterior algebra () is canonically graded by the exterior powers of the free module generated by . We view the graded module () as a chain complex 123 On the homology language of HDA models of transition systems with d = 0 and define the labeling chain map l : C (P) → () on basis elements x ∈ P by 1 , n = 0, () l(x ) = λ(e x ) ∧ ··· ∧ λ(e x ), n > 0. 1 n By Kahl (2018, Prop. 4.4.5), the labeling chain map is indeed a chain map, and therefore it induces a labeling homomorphism in homology: l : H (P) → H (()) = () ∗ ∗ ∗ The homology language of Q is then defined to be the graded module HL(Q) = im l ={l (α) | α ∈ H (P)}. ∗ ∗ ∗ The term reflects an analogy with the ordinary language of an automaton, which is a set of labels of paths. Some fundamental properties of the homology language have been established in Kahl (2021). 3.3 Simple cubical dimaps A simple cubical dimap from a precubical set P to a precubical set P is a continuous map f :|P|→|P | such that for all n ≥ 0 and x ∈ P , there exist elements y ∈ P and θ ∈ S such that for all u ∈[0, 1] , f ([x , u]) =[y, t (u)]. By Kahl (2018, Prop. 6.2.4), y and θ are uniquely determined by f and x.Wemay therefore slightly abuse notation and write f (x ) to denote y. Obviously, the geometric realization of a morphism of precubical sets is a simple cubical dimap. In Kahl (2018), a more general concept of cubical dimap has been defined, hence the adjective simple. A simple cubical dimap from an HDA Q = (P, ı, F,λ) to an HDA Q = (P , ı , F ,λ ) is a simple cubical dimap of precubical sets f : P → P that pre- serves the initial and the final states and that satisfies λ ( f (x )) = λ(x ) for all x ∈ P . Our interest in simple cubical dimaps is motivated by the following fact: Proposition 3.1 (Kahl 2021, Prop. 5.7.2) Let Q and Q be HDAs such that there exists a simple cubical dimap Q → Q . Then H L(Q) ⊆ HL(Q ). 123 T. Kahl 3.4 The homology language of a free symmetric HDA Let Q = (P, ı, F,λ) be an HDA. Since there exists the morphism of HDAs Q → SQ, x → (id, x ), by Proposition 3.1, HL(Q) ⊆ HL(SQ). We show in Theorem 3.3 below that actually equality holds. Lemma 3.2 Let θ ∈ S (n ≥ 1), and let i ∈{1,..., n} and k ∈{0, 1}. Then k k n−1 n δ ◦ t = t ◦ δ :[0, 1] →[0, 1] . −1 d θ θ i i θ (i ) n−1 Proof Let (u ,..., u ) ∈[0, 1] .Wehave 1 n−1 δ (u ,..., u ) = (u ,..., u , k, u ..., u ). 1 n−1 1 i −1 i n−1 For j ∈{1,..., n},set u , 1 ≤ j < i , v = k, j = i , u , i < j ≤ n. j −1 Then we have t ◦ δ (u ,..., u ) = t (v ,...,v ) θ 1 n−1 θ 1 n = (v ,...,v ) θ(1) θ(n) = (v ,...,v −1 , k,v −1 ,...,v ) θ(1) θ(n) θ(θ (i )−1) θ(θ (i )+1) = δ (v ,...,v −1 ,v −1 ,...,v ). θ(1) θ(n) −1 θ(θ (i )−1) θ(θ (i )+1) θ (i ) We have k k δ ◦ t (u ,..., u ) = δ (u ,..., u ). −1 d θ 1 n−1 −1 d θ(1) d θ(n−1) i i i θ (i ) θ (i ) Since for j ∈{1,..., n − 1}, −1 u , j <θ (i ), θ ( j)< i , ⎪ θ( j ) −1 −1 u , j <θ (i ), θ ( j)> i , v , j <θ (i ), θ( j )−1 θ( j ) u = = d θ( j ) i −1 −1 u , j ≥ θ (i ), θ ( j + 1)< i , v , j ≥ θ (i ), θ( j +1) θ( j +1) −1 u , j ≥ θ (i ), θ ( j + 1)> i θ( j +1)−1 the result follows. Theorem 3.3 HL(Q) = HL(SQ). Proof We only have to show the inclusion HL(SQ) ⊆ HL(Q). By Proposition 3.1,it suffices to construct a simple cubical dimap SQ → Q. Consider the continuous map f :|SP|→|P| defined by f ([(θ , x ), u]) =[x , t (u)] ((θ , x ) ∈ (SP) , u ∈[0, 1] ). θ n 123 On the homology language of HDA models of transition systems n−1 This is well defined because, by Lemma 3.2,for (θ , x ) ∈ (SP) , u ∈[0, 1] , i ∈{1,..., n}, and k ∈{0, 1}, k k k [x , t ◦ δ (u)]=[x,δ ◦ t (u)]=[d x , t (u)]. θ −1 d θ −1 d θ i i i θ (i ) θ (i ) By construction, f is a simple cubical dimap of precubical sets. We have f (θ , x ) = x for all (θ , x ) ∈ SP. Hence f preserves the initial and the final states. Moreover, for every edge x ∈ P , λ( f (id, x )) = λ(x ). It follows that f is a simple cubical dimap of HDAs. 4 HDA models of transition systems The purpose of this section is to define HDA models of transition systems. An HDA model can be constructed with respect to an arbitrary relation on the alphabet of labels. In this paper, we are interested in the case where this relation is an independence or an acyclic relation. Except for the subsection on acyclic relations, the material of this section is taken from Kahl (2019). 4.1 Transition systems and independence relations A transition system is a 1-truncated extensional HDA, i.e., an HDA with no cubes of dimension ≥ 2 and no two edges with the same label and the same start and end vertices. An independence relation is an irreflexive and symmetric relation on the alphabet of action labels . An independence relation equips the alphabet with a notion of concurrency: two actions are independent if they may be executed sequen- tially or simultaneously without any relevant difference. Independence relations play a fundamental role in trace theory (Mazurkiewicz 1987, 1995). The results of this paper apply, in particular, to asynchronous transition systems, which are transition systems over an alphabet with an independence relation satisfying certain conditions (see Winskel and Nielsen (1995)). 4.2 Acyclic relations A relation  on a set X is called acyclic if for all n ≥ 1 and x ,..., x ∈ X, 1 n x  x , x  x , ..., x  x ⇒ x  x . 1 2 2 3 n−1 n n 1 Note that an acyclic relation is irreflexive (n = 1) and, moreover, asymmetric (n = 2). Proposition 4.1 Let I be an independence relation on . Consider a totally ordered set (Z , ≤) and a map f :  → Z such that ∀ a, b ∈  : aI b ⇒ f (a) = f (b). 123 T. Kahl Define a relation  ⊆  ×  by a  b :⇔ aI b, f (a) ≤ f (b). Then  is acyclic and its symmetric closure is I . Proof Let x ,..., x ∈  such that x  x , x  x , ..., x  x . Then 1 n 1 2 2 3 n−1 n f (x ) ≤ f (x ) ≤ ··· ≤ f (x ) 1 2 n and therefore f (x ) ≤ f (x ).If f (x )  f (x ), then x  x .If f (x ) ≤ f (x ), 1 n n 1 n 1 n 1 then f (x ) = f (x ). Therefore we do not have x Ix . Hence x  x in this case n 1 n 1 n 1 too. Thus,  is acyclic. Let a, b ∈ . Since ≤ is a total order, we have f (a) ≤ f (b) or f (b) ≤ f (a). Hence if aI b (⇔ bI a),wehave a  b or b  a. If, conversely, a  b or b  a, then aI b by definition of . Thus, I is the symmetric closure of . Example 4.2 (i) Consider an independence relation I ⊆  × , and let ≤ be a total order on . Then an acyclic relation  whose symmetric closure is I is given by a  b :⇔ aI b, a ≤ b. (ii) Let I be an independence relation on , and let pid :  → N be a function associating with each label a process ID. If no two actions of the same process are independent, an acyclic relation  whose symmetric closure is I is given by a  b :⇔ aI b, pid(a) ≤ pid(b). 4.3 HDA models Let T = (X , ı, F,λ) be a transition system, and let R bearelationon . The relation R does not have to satisfy any condition. We say that an HDA Q = (Q,j, G,μ) is an HDA model of T with respect to R if the following conditions hold: HM1 Q = T , i.e., Q = X, j = ı, G = F, and μ = λ. ≤1 ≤1 0 0 HM2 For all x ∈ Q , λ(d x ) R λ(d x ). 2 1 k k HM3 For all m ≥ 2 and x , y ∈ Q ,if d x = d y for all r ∈{1,..., m} and r r k ∈{0, 1}, then x = y. HM4 Q is maximal with respect to the properties HM1-HM3, i.e., Q is not a proper sub-HDA of any HDA satisfying HM1-HM3. Condition HM1 says that Q is built on top of T 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. It has been shown in Kahl (2019, Thm. 4.2, Cor. 4.5) that an HDA model of a transition system with respect to a given relation always exists and that its isomorphism class only depends on the isomorphism class of the transition system. 123 On the homology language of HDA models of transition systems For later use, we state two propositions from Kahl (2019). The first deals with the filling of shells in the sense of Brown and Higgins (1981): Proposition 4.3 (Kahl 2019, Prop. 4.3) Let T = (X , ı, F,λ) be a transition system, and let Q = (Q, ı, F,λ) be an HDA model of T with respect to a relation R on . Consider an integer n ≥ 2 and 2n (not necessarily distinct) elements x ∈ Q n−1 k l l k (k ∈{0, 1}, i ∈{1,..., n}) such that d x = d x for all 1 ≤ i < j ≤ n and i j j −1 i 0 1 k, l ∈{0, 1}.Ifn = 2, suppose also that λ(x ) = λ(x ) for i ∈{1, 2} and that i i 0 0 k k λ(x ) R λ(x ). Then there exists a unique element x ∈ Q such that d x = x for all 2 1 i i i ∈{1,..., n} and k ∈{0, 1}. Proposition 4.4 (Kahl 2019, Prop. 4.7) Let T = (X , ı, F,λ) be a transition system, and let Q = (Q, ı, F,λ) be an HDA satisfying HM1 and HM2 with respect to T and a relation R on . Then λ(e x ) R λ(e x ) for all n ≥ 2,x ∈ Q , and 1 ≤ i < j ≤ n. i j n 5 The homology language of HDA models Throughout this section, let T = (X , ı, F,λ) be a transition system, and let I be an independence relation on  that is the symmetric closure of an acyclic relation . Let furthermore A = (P, ı, F,λ) and Q = (Q, ı, F,λ) be HDA models of T with respect to I and , respectively. By the main result of this paper, Q is a much smaller HDA model of T than A with the same homology language: Theorem 5.1 A = SQ and H L(A) = HL(Q). By Theorem 3.3, it is enough to prove that A SQ. Since T and ST are canonically isomorphic transition systems, this is an immediate consequence of the fact that SQ is an HDA model of ST with respect to I , which will be established in Proposition 5.6 below after a number of preparatory results. The labeling function of ST and SQ will be denoted by μ. Recall that μ is defined by μ(id, x ) = λ(x ). Lemma 5.2 Let B = (B,(id, ı ), S × F,μ) be an HDA satisfying HM1 and HM2 with respect to ST and I . Then for each b ∈ B (n ≥ 2), there exists a unique permutation ϑ ∈ S such that for all 1 ≤ i < j ≤ n, b n μ(e b)  μ(e b). ϑ (i ) ϑ ( j ) b b Moreover, setting ϑ = id for b ∈ B ,the map ϑ : B → S is a morphism of b ≤1 precubical sets. Proof Let b ∈ B (n ≥ 2). By Proposition 4.4,wehave μ(e b) I μ(e b) for all n i j 1 ≤ i < j ≤ n. Since I is irreflexive, it follows that the set M ={μ(e b) | i ∈{1,..., n}} has n elements. Moreover, since I is the symmetric closure of ,wehave μ(e b) μ(e b) or μ(e b)  μ(e b) for all i = j. Since  is acyclic, this implies that it is j j i 123 T. Kahl transitive on M. Indeed, if μ(e b)  μ(e b) and μ(e b)  μ(e b), then k = i and i j j k μ(e b)  μ(e b), which implies μ(e b)  μ(e b). Hence  is a strict total order on k i i k M. Since M has n elements, it follows that there exists a unique permutation ϑ ∈ S b n such that μ(e b)  μ(e b) ϑ (i ) ϑ ( j ) b b for all 1 ≤ i < j ≤ n. It remains to check that ϑ is a morphism of precubical sets. Let b ∈ B (n ≥ 1), i ∈{1,..., n}, and k ∈{0, 1}.If n ≤ 2, then d ϑ = id = ϑ k . Suppose that n ≥ 3. i b d b We have e b, 1 ≤ j < i , e d b = e b, i ≤ j < n. j +1 Since parallel edges of a cube have the same label (see, e.g., Kahl (2019, Lemma 4.6)), 1 0 we have μ(e d b) = μ(e d b) for all j ∈{1,..., n − 1}. Hence for k ∈{0, 1}, j j i i μ(e b), 1 ≤ j < i , μ(e d b) = μ(e b), i ≤ j < n. j +1 We therefore have −1 μ(e d b), j <ϑ (i ), ϑ ( j)< i , ⎪ ϑ ( j ) b i b k −1 μ(e d b), j <ϑ (i ), ϑ ( j)> i , k ϑ ( j )−1 b b i b μ(e d b) = d ϑ ( j ) i b i k −1 ⎪ μ(e d b), j ≥ ϑ (i ), ϑ ( j + 1)< i , ϑ ( j +1) b ⎪ b i b k −1 μ(e d b), j ≥ ϑ (i ), ϑ ( j + 1)> i ϑ ( j +1)−1 b b i b −1 μ(e b), j <ϑ (i ), ϑ ( j ) b b −1 μ(e b), j ≥ ϑ (i ). ϑ ( j +1) b b −1 Let 1 ≤ j < r ≤ n − 1. If j < r <ϑ (i ),wehave k k μ(e d b) = μ(e b)  μ(e b) = μ(e d b). d ϑ ( j ) ϑ ( j ) ϑ (r ) d ϑ (r ) i b i b b i b i −1 If j <ϑ (i ) ≤ r,wehave k k μ(e d b) = μ(e b)  μ(e b) = μ(e d b). d ϑ ( j ) ϑ ( j ) ϑ (r +1) d ϑ (r ) i b i b b i b i −1 If ϑ (i ) ≤ j < r,wehave k k μ(e d b) = μ(e b)  μ(e b) = μ(e d b). d ϑ ( j ) ϑ ( j +1) ϑ (r +1) d ϑ (r ) i b i b b i b i Thus, ϑ = d ϑ . i b d b 123 On the homology language of HDA models of transition systems Lemma 5.3 Let B = (B,(id, ı ), S × F,μ) be an HDA satisfying HM1 and HM2 with respect to ST and I . Then there exists a unique morphism of graded sets φ : B → Q such that φ : B → Q is the isomorphism given by (id, x ) → x and such that ≤1 ≤1 ≤1 k k d φ(b) = φ(d b) for all b ∈ B (n ≥ 1),i ∈{1,..., n}, and k ∈{0, 1}. i ϑ (i ) Proof We construct φ inductively. Let n ≥ 2, and suppose we have constructed φ up k k to degree n − 1. Let b ∈ B . Consider the elements y = φ(d b) ∈ Q . Suppose n n−1 i ϑ (i ) that 1 ≤ i < j ≤ n. By Lemma 5.2, ϑ l = d ϑ and ϑ k = d ϑ . ϑ ( j ) b ϑ (i ) b b b d b d b ϑ ( j ) ϑ (i ) b b Hence, by the inductive hypothesis and Proposition 2.2, k l k l k l d y = d φ(d b) = φ(d d b) i j i ϑ ( j ) d ϑ (i ) ϑ ( j ) b b b ϑ ( j ) l k l k = φ(d d b) = d φ(d b) j −1 d ϑ ( j −1) ϑ (i ) ϑ (i ) ϑ (i ) b b b l k = d y . j −1 i If n = 2, we also have 0 0 0 1 1 1 λ(y ) = λ(φ (d b)) = μ(d b) = μ(d b) = λ(φ (d b)) = λ(y ) i ϑ (i ) ϑ (i ) ϑ (i ) ϑ (i ) i b b b b for all i ∈{1, 2}. Moreover, by Lemma 5.2, 0 0 0 λ(y ) = λ(φ (d b)) = μ(d b) = μ(e b) ϑ (1) 2 ϑ (2) ϑ (2) b b b 0 0 0 μ(e b) = μ(d b) = λ(φ (d b)) = λ(y ). ϑ (2) b ϑ (1) ϑ (1) 1 b b k k By Proposition 4.3, there exists a unique cube y ∈ Q such that d y = y for all i i k ∈{0, 1} and i ∈{1,..., n}.Weset φ(b) = y. This defines φ in degree n. Lemma 5.4 SQ satisfies HM1 and HM2 with respect to ST and I . Proof HM1: We have (SQ) = ((SQ) ,(id, ı ), S × F,μ) = (SQ ,(id, ı ), S × F,μ) ≤1 ≤1 0 ≤1 0 = (SX,(id, ı ), S × F,μ) = ST . HM2: Let (θ , x ) ∈ (SQ) = S × Q .For i ∈{1, 2}, 2 2 2 0 0 0 0 μ(d (θ , x )) = μ(d θ, d x ) = μ(id, d x ) = λ(d x ). i −1 −1 −1 θ (i ) θ (i ) θ (i ) Thus if θ = id, 0 0 0 0 μ(d (θ , x )) = λ(d x )  λ(d x ) = μ(d (θ , x )). 2 2 1 1 If θ is the transposition (21), 0 0 0 0 μ(d (θ , x )) = λ(d x )  λ(d x ) = μ(d (θ , x )). 1 2 1 2 0 0 In both cases, μ(d (θ , x )) I μ(d (θ , x )). 2 1 123 T. Kahl Lemma 5.5 In SQ, ϑ = θ for all elements (θ , x ). (θ ,x ) Proof Let (θ , x ) ∈ (SQ) . We may suppose that n ≥ 2. By Kahl (2022, Prop. 4.3), e (θ , x ) = (id, e x ). Hence −1 θ (i ) μ(e (θ , x )) = μ(id, e −1 x ) = λ(e −1 x ). θ (i ) θ (i ) Thus, μ(e (θ , x )) = λ(e x ). By Proposition 4.4, θ(i ) i μ(e (θ , x )) = λ(e x )  λ(e x ) = μ(e (θ , x )) θ(i ) i j θ( j ) for all 1 ≤ i < j ≤ n. Consequently, by Lemma 5.2, ϑ = θ. (θ ,x ) Proposition 5.6 SQ is an HDA model of ST with respect to I . Proof By Lemma 5.4, we only have to show HM3 and HM4. HM3: Let m ≥ 2, and let (σ, x ), (θ , y) ∈ (SQ) = S × Q such that d (σ, x ) = m m m k k k d (θ , y) for all r ∈{1,..., m} and k ∈{0, 1}. Then (d σ, d x ) = (d θ, d y) r r −1 −1 σ (r ) θ (r ) for all r and k.If m ≥ 3, this implies (σ, x ) = (θ , y) by Proposition 2.1. In the case m = 2, it is enough to show that σ = θ. Suppose that this is not the case. Then we may assume that σ = id and θ = (21). But then 0 0 0 0 λ(d y) = λ(d x )  λ(d x ) = λ(d y), 1 2 1 2 which is impossible because  is asymmetric. HM4: Suppose that B = (B,(id, ı ), S × F,μ) is an HDA satisfying conditions HM1–HM3 with respect to ST and I that contains SQ as a sub-HDA. We have to show that B = SQ. Since SQ ⊆ B, the maps ϑ : B → S and ϑ : SQ → S coincide on SQ.Let φ : B → Q be the map of graded sets of Lemma 5.3. The corresponding map for SQ is the map ψ : SQ → Q given by ψ(θ, x ) = x. Indeed, by Lemma 5.5, k k k k k d ψ(θ, x ) = d x = ψ(d θ, d x ) = ψ(d θ, d x ) = ψ(d (θ , x )) = θ(i ) θ(i ) −1 i i i θ(i ) θ (θ (i )) ψ(d (θ , x )). Since SQ ⊆ B, the restriction of φ to SQ is ψ. ϑ (i ) (θ ,x ) By HM1, B = (SQ) .Let m ≥ 2, and suppose inductively that B = (SQ) . ≤1 ≤1 <m <m k k Let b ∈ B . By the inductive hypothesis, d b ∈ (SQ) . Write d b = (θ , x ).We m m−1 i i have k k k k d (ϑ ,φ(b)) = (d ϑ , d φ(b)) = (ϑ k ,φ(d b)) = (ϑ k ,ψ(d b)) b i b −1 i d b i d b i ϑ (i ) i i = (ϑ ,ψ(θ, x )) = (θ , x ) = d b. (θ ,x ) By HM3, it follows that b = (ϑ ,φ(b)) ∈ (SQ) . b m Funding Open access funding provided by FCT|FCCN (b-on). This research was supported by FCT (Fun- dação para a Ciência e a Tecnologia, Portugal) through projects UIDB/00013/2020 and UIDP/00013/2020. Declarations Conflict of interest The author declares that there is no conflict of interest. 123 On the homology language of HDA models of transition systems Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. References Bourbaki, N.: Algebra I. Addison-Wesley (1974) Brown, R., Higgins, P.J.: On the algebra of cubes. J. Pure Appl. Algebra 21(3), 233–260 (1981) Fahrenberg, U.: Higher-dimensional automata from a topological viewpoint, Ph.D. thesis, Aalborg University, Denmark, (2005) Fiedorowicz, Z., Loday, J.-L.: Crossed simplicial groups and their associated homology. Trans. Am. Math. Soc. 326(1), 57–87 (1991) Gaucher, P.: Combinatorics of labelling in higher-dimensional automata. Theor. Comput. Sci. 411, 1452– 1483 (2010) Goubault, E., Mimram, S.: Formal relationships between geometrical and classical models for concurrency. Electr. Notes Theor. Comput. Sci. 283, 77–109 (2012) Grandis, M., Mauri, L.: Cubical sets and their site. Theory Appl. Categories 11(8), 185–211 (2003) Kahl, T.: pg2hda [Computer software], http://w3.math.uminho.pt/~kahl/, 2018–2022 Kahl, T.: Labeled homology of higher-dimensional automata. J. Appl. Comput. Topol. 2(3–4), 271–300 (2018) Kahl, T.: Higher-dimensional automata modeling shared-variable systems. Log. Methods Comput. Sci. 15(3), 28:1-28:21 (2019) Kahl, T.: Weak equivalence of higher-dimensional automata. Discrete Math. Theor. Comput. Sci. 23(1), 1–31 (2021) Kahl, T.: On symmetric higher-dimensional automata and bisimilarity. Theor. Comput. Sci. 935, 47 (2022) Krasauskas, R.: Skew-simplicial groups. Lith. Math. J. 27, 47–54 (1987) Mazurkiewicz, A.: Introduction to trace theory, the book of traces (V. Diekert and G. Rozenberg, eds.), World Scientific, 3–41 (1995) Mazurkiewicz, A.: Trace theory, petri nets: applications and relationships to other models of concurrency (W. Brauer, W. Reisig, and G. Rozenberg, eds.), Lecture Notes in Computer Science, vol. 255, Springer, pp. 279–324 (1987) Pratt, V.: Modeling Concurrency with Geometry, POPL ’91, Proceedings of the 18th ACM SIGPLAN- SIGACT symposium on Principles of programming languages, ACM New York, NY, USA, 311–322 (1991) van Glabbeek, R.J.: On the expressiveness of higher dimensional automata. Theor. Comput. Sci. 356(3), 265–290 (2006) Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, S.S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science: Semantic Modelling, pp. 1–148. Oxford University Press (1995) Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Applied and Computational Topology Springer Journals

On the homology language of HDA models of transition systems

Kahl, Thomas
Journal of Applied and Computational Topology , Volume OnlineFirst – May 4, 2023
Download PDF
15 pages

Loading next page...
 
/lp/springer-journals/on-the-homology-language-of-hda-models-of-transition-systems-yCA8sLIBHu

References (12)

Publisher
Springer Journals
Copyright
Copyright © The Author(s) 2023
ISSN
2367-1726
eISSN
2367-1734
DOI
10.1007/s41468-023-00120-1
Publisher site
See Article on Publisher Site

Abstract

Given a transition system with an independence relation on the alphabet of labels, one can associate with it a usually very large symmetric higher-dimensional automaton. The purpose of this paper is to show that by choosing an acyclic relation whose symmetric closure is the given independence relation, it is possible to construct a much smaller nonsymmetric HDA with the same homology language. Keywords Higher-dimensional automata · Transition system · Homology language Mathematics Subject Classification 55N35 · 68Q85 1 Introduction Higher-dimensional automata are a powerful combinatorial-topological model for con- current systems. A higher-dimensional automaton (HDA) is a precubical set (i.e., a cubical set without degeneracies) with an initial state, a set of final states, and a label- ing on 1-cubes such that opposite edges of 2-cubes have the same label (van Glabbeek 2006;Pratt 1991). An HDA is thus a (labeled) transition system (or an ordinary automa- ton) with a supplementary structure consisting of two- and higher-dimensional cubes. The transition system represents the states and transitions of a concurrent system. An n-cube in an HDA indicates that the n transitions starting at its origin are indepen- dent in the sense that they may occur in any order, or even simultaneously, without any observable difference. It has been shown in van Glabbeek (2006) that higher- dimensional automata are more expressive than the principal traditional models of concurrency. B Thomas Kahl kahl@math.uminho.pt Centro de Matemática, Universidade do Minho, Campus de Gualtar, 4710-057 Braga, Portugal 123 T. Kahl The fact that the two- and higher-dimensional cubes in an HDA represent inde- pendence of transitions suggests that the higher-dimensional topology of an HDA contains global information on independence of processes and components of the modeled concurrent system. In Kahl (2021), the homology language has been devised as a homological tool to describe this global independence structure of an HDA. The homology language of an HDA is defined to be the image of the homomorphism induced in homology by a certain labeling chain map that leads from the cubical chain complex of the HDA to the exterior algebra on the alphabet of labels (see Sect. 3). The homology language can be computed and analyzed using software (Kahl 2018). Transition systems are arguably the most fundamental model for concurrent sys- tems. A natural way to turn a transition system into an HDA is to fill in empty squares and higher-dimensional cubes (van Glabbeek 2006; Gaucher 2010; Goubault and Mimram 2012; Kahl 2019). This approach requires some concept of independence in order to decide which cubes to fill in. Such a concept of independence may be given by an independence relation—i.e., an irreflexive and symmetric relation—on the alpha- bet of action labels. Independence relations play a fundamental role in trace theory in the sense of Mazurkiewicz (1987). Asynchronous transition systems (Winskel and Nielsen 1995) are an important example of transition systems that come equipped with an independence relation on the set of labels. HDAs constructed from transition systems using a cube filling procedure based on a symmetric concept of independence, such as an independence relation on the set of labels, are usually very large because an empty n-cube representing the execution of n independent actions is filled in n! times. From a computational point of view, it is therefore desirable to have a way to produce smaller HDA models of transition systems. It has been shown in Kahl (2019) that using a cube filling rule based on an asymmetric rather than an independence relation on the alphabet, one can construct an HDA model of a transition system where the independence of n actions in a state is represented by a single n-cube (at least if the transition system under consideration is deterministic). It is, of course, not to be expected that two HDAs constructed using different filling rules from the same transition system will be equivalent in a meaningful sense. Every independence relation on an alphabet is the symmetric closure of an acyclic relation, i.e., a relation that is acyclic when seen as a graph (see Sect. 4). The purpose of this paper is to establish that the HDAs constructed from a transition system using cube filling rules based, respectively, on an independence relation on the alphabet and a generating acyclic relation have the same homology language. The two HDAs may therefore be regarded as equivalent from the point of view of their independence structures. As we will show in Sect. 5, the HDA constructed using the independence relation is the free symmetric HDA generated by the one constructed using the acyclic relation. The latter is thus a significantly smaller HDA model of the given transition system than the former. 123 On the homology language of HDA models of transition systems 2 Precubical sets and HDAs This section presents fundamental material on precubical sets, higher-dimensional automata, and their symmetric variants. 2.1 Precubical sets A precubical set is a graded set P = (P ) with face maps n n≥0 d : P → P (n > 0, k = 0, 1, i = 1,..., n) n n−1 satisfying the cubical identities k l l k d d = d d (k, l = 0, 1, i < j ). i j j −1 i If x ∈ P , we say that x is of degree or dimension n. The elements of degree n are called the n-cubes of P. The elements of degree 0 are also called the vertices of P, and the 1-cubes are also called the edges of P.The ith starting edge of a cube x of degree n > 0 is the edge 0 0 0 0 e x = d ... d d ... d x . 1 i −1 i +1 n A precubical subset of a precubical set is a graded subset that is stable under the face maps. The n-skeleton of a precubical set P is the precubical subset P defined ≤n by (P ) = P for m ≤ n and P =∅ else. ≤n m m m A morphism of precubical sets is a morphism of graded sets that is compatible with the face maps. The category of precubical sets can be seen as the presheaf category of op functors  → Set where  is the small subcategory of the category of topological spaces whose objects are the standard n-cubes [0, 1] (n ≥ 0) and whose nonidentity k n n+1 morphisms are composites of the coface maps δ :[0, 1] →[0, 1] (k ∈{0, 1}, n ≥ 0, i ∈{1,..., n + 1}) given by δ (u ,..., u ) = (u ,..., u , k, u ..., u ). 1 n 1 i −1 i n The geometric realization of a precubical set P is the quotient space ⎛ ⎞ ⎝ ⎠ |P|= P ×[0, 1] / ∼ n≥0 where the sets P are given the discrete topology and the equivalence relation is generated by k k n (d x , u) ∼ (x,δ (u)), x ∈ P , u ∈[0, 1] , i ∈{1,..., n + 1}, k ∈{0, 1}. n+1 i i The geometric realization of a morphism of precubical sets f : P → Q is the continuous map | f |: |P|→|Q| given by | f |([x , u]) =[ f (x ), u]. 123 T. Kahl 2.2 The precubical set of permutations The family of symmetric groups S = (S ) (with S ={id }) is a precubical set n n≥0 0 ∅ with respect to the face maps given by −1 θ( j ), j <θ (i ), θ ( j)< i , −1 θ( j ) − 1, j <θ (i ), θ ( j)> i , d θ( j ) = −1 ⎪ θ( j + 1), j ≥ θ (i ), θ ( j + 1)< i , −1 θ( j + 1) − 1, j ≥ θ (i ), θ ( j + 1)> i (see Kahl (2022) and compare Krasauskas (1987), and Fiedorowicz and Loday (1991)). 0 1 Since, by definition, d θ = d θ, we may simplify the notation by setting i i 0 1 d θ = d θ = d θ. i i Since S ={id}, the two elements of S have the same faces. In degrees ≥ 3, 1 2 permutations are determined by their faces: Proposition 2.1 Let n ≥ 3, and let σ, θ ∈ S such that d σ = d θ for all i ∈{1,..., n}. n i i Then σ = θ. Proof It follows from Kahl (2022, Lemma 3.3) that it is enough to show that there −1 exists an r such that σ(r ) = θ(r ). Suppose that this is not the case. Set i = σ (n) −1 and j = θ (n). Then i , j < n. Indeed, suppose that i = n. Then for 1 ≤ r ≤ n − 1, −1 d σ(r ) = σ(r ) because r < n = σ (n), σ(r ) ≤ n, and σ(r ) = σ(n) = n. Since −1 θ(r ) = σ(r ) and θ(r ), θ (r + 1) ≤ n,wehave r ≥ θ (n), θ(r + 1)< n, and σ(r ) = d σ(r ) = d θ(r ) = θ(r + 1). n n −1 −1 In particular, j = θ (n) ≤ 1. Hence j = 1 and θ(1) = n. Set s = σ (1). Since −1 σ(s) = σ(n), s < n. Since θ(s + 1) = σ(s) = 1, θ (1) = s + 1. Since the values of σ are ≥ 1, we have −1 σ(1) − 1, 1 <σ (1) = s, d σ(1) = σ(2) − 1, 1 = s. Since n > 2, we have σ(1), σ (2) = σ(n) = n and therefore d σ(1) ≤ n − 2. On the −1 other hand, 1 < s + 1 = θ (1) and θ(1) = n > 1 and therefore n − 2 ≥ d σ(1) = d θ(1) = θ(1) − 1 = n − 1, 1 1 which is impossible. It follows that i < n. An analogous argument shows that j < n. −1 Hence 1 ≤ i , j ≤ n − 1. We show that i < j. Since i ≥ i = σ (n), σ(i + 1) ≤ n, and σ(i + 1) = σ(i ) = n,wehave d σ(i ) = σ(i + 1). Hence d θ(i ) = σ(i + 1) = n n θ(i + 1). Since θ(i + 1) ≤ n, it follows that i < j. Analogously, j < i. Since this is impossible, there must exist an r such that σ(r ) = θ(r ). 123 On the homology language of HDA models of transition systems For later use, we state the following fact from Kahl (2022): Proposition 2.2 (Kahl 2022, Prop. 3.6(i)) Let P be a precubical set, and let n ≥ 2, 1 ≤ i < j ≤ n, k, l ∈{0, 1},x ∈ P , and θ ∈ S . Then n n k l l k d d x = d d x . d θ(i ) θ( j ) d θ( j −1) θ(i ) θ( j ) θ(i ) 2.3 Symmetric precubical sets A symmetric precubical set is a precubical set P equipped with a crossed action of S on P, i.e., a morphism of graded sets S × P − → P, (θ , x ) → θ · x such that • for all n ≥ 0 and x ∈ P , id · x = x; • for all n ≥ 0, σ, θ ∈ S , and x ∈ P , (σ · θ) · x = σ · (θ · x ); n n • for all n ≥ 1, θ ∈ S , x ∈ P , i ∈{1,..., n}, and k ∈{0, 1}, n n k k d (θ · x ) = d θ · d x . i −1 θ (i ) Symmetric precubical sets form a category, in which the morphisms are morphisms of precubical sets that are compatible with the crossed actions. We remark that the op category of symmetric precubical sets is isomorphic to the presheaf category Set where  is the subcategory of the category of topological spaces whose objects are the standard n-cubes [0, 1] (n ≥ 0) and whose morphisms are composites of the coface maps δ defined above and the permutation maps n n t :[0, 1] →[0, 1] ,(u ,..., u ) → (u ..., u )(n ≥ 0,θ ∈ S ) θ 1 n θ(1) θ(n) n (cf. Grandis and Mauri (2003); Fahrenberg (2005); Gaucher (2010); Goubault and Mimram (2012)). The free symmetric precubical set generated by a precubical set P is the symmetric precubical set SP defined by • SP = S × P (n ≥ 0); n n n k k • d (θ , x ) = (d θ, d x)(n ≥ 1,θ ∈ S , x ∈ P , 1 ≤ i ≤ n, k ∈{0, 1}); i n n −1 θ (i ) • σ · (θ , x ) = (σ · θ, x)(n ≥ 0,σ,θ ∈ S , x ∈ P ). n n The free symmetric precubical set is functorial, and the functor P → SP from the category of precubical sets to the category of symmetric precubical sets is left adjoint to the forgetful functor. 2.4 Higher-dimensional automata Throughout this paper, we consider a fixed alphabet .A higher-dimensional automaton (HDA) over  is a tuple Q = (P, ı, F,λ) 123 T. Kahl where P is a precubical set, ı ∈ P is a vertex, called the initial state, F ⊆ P is a 0 0 (possibly empty) set of final states, and λ : P →  is a map, called the labeling 0 1 function, such that λ(d x ) = λ(d x ) for all x ∈ P and i ∈{1, 2} (van Glabbeek i i 2006). We say that an HDA Q = (P , ı , F ,λ ) is a sub-HDA of Q and write Q ⊆ Q if P is a precubical subset of P, ı = ı, F = F ∩ Q , and λ = λ| .The n-skeleton of Q is the sub-HDA Q = (P , ı, F,λ| ). Higher-dimensional automata ≤n ≤n (P ) ≤n 1 form a category, in which a morphism from an HDA Q = (P, ı, F,λ) to an HDA Q = (P , ı , F ,λ ) is a morphism of precubical sets f : P → P such that f (ı ) = ı , f (F ) ⊆ F , and λ ( f (x )) = λ(x ) for all x ∈ P . A symmetric HDA is an HDA Q = (P, ı, F,λ) equipped with a crossed action of S on P. Symmetric HDAs form a category, in which the morphisms are mor- phisms of HDAs that also are morphisms of symmetric precubical sets. The free symmetric HDA generated by an HDA Q = (P, ı, F,λ) is the symmetric HDA SQ = (SP,(id, ı ), S × F,μ) where μ(id, x ) = λ(x)(x ∈ P ) and the crossed 0 1 action is the one of SP. The assignment Q → SQ defines a functor from the category of HDAs to the category of symmetric HDAs, which is left adjoint to the forgetful functor. 3 The homology language and free symmetric HDAs In this section, we recall the definition of the homology language of an HDA from Kahl (2021) and show, as a first contribution of this paper, that an HDA and the free symmetric HDA generated by it have the same homology language. We work over a fixed principal ideal domain, which we suppress from the notation. 3.1 Cubical chains and cubical homology The cubical chain complex of a precubical set P is the nonnegative chain complex C (P) where C (P) is the free module generated by P and the boundary operator ∗ n n d : C (P) → C (P) is given by n n−1 i 0 1 dx = (−1) (d x − d x ), x ∈ P (n > 0). i i i =1 The cubical homology of P, denoted by H (P), is the homology of C (P). ∗ ∗ 3.2 The homology language of an HDA Let Q = (P, ı, F,λ) be an HDA over . Consider the exterior algebra on the free module generated by , (). Recall that this is the quotient of the tensor algebra on the free module on  by the two-sided ideal generated by all elements of the form x ⊗ x where x runs through the free module on  (see Bourbaki (1974)for more details). The exterior algebra () is canonically graded by the exterior powers of the free module generated by . We view the graded module () as a chain complex 123 On the homology language of HDA models of transition systems with d = 0 and define the labeling chain map l : C (P) → () on basis elements x ∈ P by 1 , n = 0, () l(x ) = λ(e x ) ∧ ··· ∧ λ(e x ), n > 0. 1 n By Kahl (2018, Prop. 4.4.5), the labeling chain map is indeed a chain map, and therefore it induces a labeling homomorphism in homology: l : H (P) → H (()) = () ∗ ∗ ∗ The homology language of Q is then defined to be the graded module HL(Q) = im l ={l (α) | α ∈ H (P)}. ∗ ∗ ∗ The term reflects an analogy with the ordinary language of an automaton, which is a set of labels of paths. Some fundamental properties of the homology language have been established in Kahl (2021). 3.3 Simple cubical dimaps A simple cubical dimap from a precubical set P to a precubical set P is a continuous map f :|P|→|P | such that for all n ≥ 0 and x ∈ P , there exist elements y ∈ P and θ ∈ S such that for all u ∈[0, 1] , f ([x , u]) =[y, t (u)]. By Kahl (2018, Prop. 6.2.4), y and θ are uniquely determined by f and x.Wemay therefore slightly abuse notation and write f (x ) to denote y. Obviously, the geometric realization of a morphism of precubical sets is a simple cubical dimap. In Kahl (2018), a more general concept of cubical dimap has been defined, hence the adjective simple. A simple cubical dimap from an HDA Q = (P, ı, F,λ) to an HDA Q = (P , ı , F ,λ ) is a simple cubical dimap of precubical sets f : P → P that pre- serves the initial and the final states and that satisfies λ ( f (x )) = λ(x ) for all x ∈ P . Our interest in simple cubical dimaps is motivated by the following fact: Proposition 3.1 (Kahl 2021, Prop. 5.7.2) Let Q and Q be HDAs such that there exists a simple cubical dimap Q → Q . Then H L(Q) ⊆ HL(Q ). 123 T. Kahl 3.4 The homology language of a free symmetric HDA Let Q = (P, ı, F,λ) be an HDA. Since there exists the morphism of HDAs Q → SQ, x → (id, x ), by Proposition 3.1, HL(Q) ⊆ HL(SQ). We show in Theorem 3.3 below that actually equality holds. Lemma 3.2 Let θ ∈ S (n ≥ 1), and let i ∈{1,..., n} and k ∈{0, 1}. Then k k n−1 n δ ◦ t = t ◦ δ :[0, 1] →[0, 1] . −1 d θ θ i i θ (i ) n−1 Proof Let (u ,..., u ) ∈[0, 1] .Wehave 1 n−1 δ (u ,..., u ) = (u ,..., u , k, u ..., u ). 1 n−1 1 i −1 i n−1 For j ∈{1,..., n},set u , 1 ≤ j < i , v = k, j = i , u , i < j ≤ n. j −1 Then we have t ◦ δ (u ,..., u ) = t (v ,...,v ) θ 1 n−1 θ 1 n = (v ,...,v ) θ(1) θ(n) = (v ,...,v −1 , k,v −1 ,...,v ) θ(1) θ(n) θ(θ (i )−1) θ(θ (i )+1) = δ (v ,...,v −1 ,v −1 ,...,v ). θ(1) θ(n) −1 θ(θ (i )−1) θ(θ (i )+1) θ (i ) We have k k δ ◦ t (u ,..., u ) = δ (u ,..., u ). −1 d θ 1 n−1 −1 d θ(1) d θ(n−1) i i i θ (i ) θ (i ) Since for j ∈{1,..., n − 1}, −1 u , j <θ (i ), θ ( j)< i , ⎪ θ( j ) −1 −1 u , j <θ (i ), θ ( j)> i , v , j <θ (i ), θ( j )−1 θ( j ) u = = d θ( j ) i −1 −1 u , j ≥ θ (i ), θ ( j + 1)< i , v , j ≥ θ (i ), θ( j +1) θ( j +1) −1 u , j ≥ θ (i ), θ ( j + 1)> i θ( j +1)−1 the result follows. Theorem 3.3 HL(Q) = HL(SQ). Proof We only have to show the inclusion HL(SQ) ⊆ HL(Q). By Proposition 3.1,it suffices to construct a simple cubical dimap SQ → Q. Consider the continuous map f :|SP|→|P| defined by f ([(θ , x ), u]) =[x , t (u)] ((θ , x ) ∈ (SP) , u ∈[0, 1] ). θ n 123 On the homology language of HDA models of transition systems n−1 This is well defined because, by Lemma 3.2,for (θ , x ) ∈ (SP) , u ∈[0, 1] , i ∈{1,..., n}, and k ∈{0, 1}, k k k [x , t ◦ δ (u)]=[x,δ ◦ t (u)]=[d x , t (u)]. θ −1 d θ −1 d θ i i i θ (i ) θ (i ) By construction, f is a simple cubical dimap of precubical sets. We have f (θ , x ) = x for all (θ , x ) ∈ SP. Hence f preserves the initial and the final states. Moreover, for every edge x ∈ P , λ( f (id, x )) = λ(x ). It follows that f is a simple cubical dimap of HDAs. 4 HDA models of transition systems The purpose of this section is to define HDA models of transition systems. An HDA model can be constructed with respect to an arbitrary relation on the alphabet of labels. In this paper, we are interested in the case where this relation is an independence or an acyclic relation. Except for the subsection on acyclic relations, the material of this section is taken from Kahl (2019). 4.1 Transition systems and independence relations A transition system is a 1-truncated extensional HDA, i.e., an HDA with no cubes of dimension ≥ 2 and no two edges with the same label and the same start and end vertices. An independence relation is an irreflexive and symmetric relation on the alphabet of action labels . An independence relation equips the alphabet with a notion of concurrency: two actions are independent if they may be executed sequen- tially or simultaneously without any relevant difference. Independence relations play a fundamental role in trace theory (Mazurkiewicz 1987, 1995). The results of this paper apply, in particular, to asynchronous transition systems, which are transition systems over an alphabet with an independence relation satisfying certain conditions (see Winskel and Nielsen (1995)). 4.2 Acyclic relations A relation  on a set X is called acyclic if for all n ≥ 1 and x ,..., x ∈ X, 1 n x  x , x  x , ..., x  x ⇒ x  x . 1 2 2 3 n−1 n n 1 Note that an acyclic relation is irreflexive (n = 1) and, moreover, asymmetric (n = 2). Proposition 4.1 Let I be an independence relation on . Consider a totally ordered set (Z , ≤) and a map f :  → Z such that ∀ a, b ∈  : aI b ⇒ f (a) = f (b). 123 T. Kahl Define a relation  ⊆  ×  by a  b :⇔ aI b, f (a) ≤ f (b). Then  is acyclic and its symmetric closure is I . Proof Let x ,..., x ∈  such that x  x , x  x , ..., x  x . Then 1 n 1 2 2 3 n−1 n f (x ) ≤ f (x ) ≤ ··· ≤ f (x ) 1 2 n and therefore f (x ) ≤ f (x ).If f (x )  f (x ), then x  x .If f (x ) ≤ f (x ), 1 n n 1 n 1 n 1 then f (x ) = f (x ). Therefore we do not have x Ix . Hence x  x in this case n 1 n 1 n 1 too. Thus,  is acyclic. Let a, b ∈ . Since ≤ is a total order, we have f (a) ≤ f (b) or f (b) ≤ f (a). Hence if aI b (⇔ bI a),wehave a  b or b  a. If, conversely, a  b or b  a, then aI b by definition of . Thus, I is the symmetric closure of . Example 4.2 (i) Consider an independence relation I ⊆  × , and let ≤ be a total order on . Then an acyclic relation  whose symmetric closure is I is given by a  b :⇔ aI b, a ≤ b. (ii) Let I be an independence relation on , and let pid :  → N be a function associating with each label a process ID. If no two actions of the same process are independent, an acyclic relation  whose symmetric closure is I is given by a  b :⇔ aI b, pid(a) ≤ pid(b). 4.3 HDA models Let T = (X , ı, F,λ) be a transition system, and let R bearelationon . The relation R does not have to satisfy any condition. We say that an HDA Q = (Q,j, G,μ) is an HDA model of T with respect to R if the following conditions hold: HM1 Q = T , i.e., Q = X, j = ı, G = F, and μ = λ. ≤1 ≤1 0 0 HM2 For all x ∈ Q , λ(d x ) R λ(d x ). 2 1 k k HM3 For all m ≥ 2 and x , y ∈ Q ,if d x = d y for all r ∈{1,..., m} and r r k ∈{0, 1}, then x = y. HM4 Q is maximal with respect to the properties HM1-HM3, i.e., Q is not a proper sub-HDA of any HDA satisfying HM1-HM3. Condition HM1 says that Q is built on top of T 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. It has been shown in Kahl (2019, Thm. 4.2, Cor. 4.5) that an HDA model of a transition system with respect to a given relation always exists and that its isomorphism class only depends on the isomorphism class of the transition system. 123 On the homology language of HDA models of transition systems For later use, we state two propositions from Kahl (2019). The first deals with the filling of shells in the sense of Brown and Higgins (1981): Proposition 4.3 (Kahl 2019, Prop. 4.3) Let T = (X , ı, F,λ) be a transition system, and let Q = (Q, ı, F,λ) be an HDA model of T with respect to a relation R on . Consider an integer n ≥ 2 and 2n (not necessarily distinct) elements x ∈ Q n−1 k l l k (k ∈{0, 1}, i ∈{1,..., n}) such that d x = d x for all 1 ≤ i < j ≤ n and i j j −1 i 0 1 k, l ∈{0, 1}.Ifn = 2, suppose also that λ(x ) = λ(x ) for i ∈{1, 2} and that i i 0 0 k k λ(x ) R λ(x ). Then there exists a unique element x ∈ Q such that d x = x for all 2 1 i i i ∈{1,..., n} and k ∈{0, 1}. Proposition 4.4 (Kahl 2019, Prop. 4.7) Let T = (X , ı, F,λ) be a transition system, and let Q = (Q, ı, F,λ) be an HDA satisfying HM1 and HM2 with respect to T and a relation R on . Then λ(e x ) R λ(e x ) for all n ≥ 2,x ∈ Q , and 1 ≤ i < j ≤ n. i j n 5 The homology language of HDA models Throughout this section, let T = (X , ı, F,λ) be a transition system, and let I be an independence relation on  that is the symmetric closure of an acyclic relation . Let furthermore A = (P, ı, F,λ) and Q = (Q, ı, F,λ) be HDA models of T with respect to I and , respectively. By the main result of this paper, Q is a much smaller HDA model of T than A with the same homology language: Theorem 5.1 A = SQ and H L(A) = HL(Q). By Theorem 3.3, it is enough to prove that A SQ. Since T and ST are canonically isomorphic transition systems, this is an immediate consequence of the fact that SQ is an HDA model of ST with respect to I , which will be established in Proposition 5.6 below after a number of preparatory results. The labeling function of ST and SQ will be denoted by μ. Recall that μ is defined by μ(id, x ) = λ(x ). Lemma 5.2 Let B = (B,(id, ı ), S × F,μ) be an HDA satisfying HM1 and HM2 with respect to ST and I . Then for each b ∈ B (n ≥ 2), there exists a unique permutation ϑ ∈ S such that for all 1 ≤ i < j ≤ n, b n μ(e b)  μ(e b). ϑ (i ) ϑ ( j ) b b Moreover, setting ϑ = id for b ∈ B ,the map ϑ : B → S is a morphism of b ≤1 precubical sets. Proof Let b ∈ B (n ≥ 2). By Proposition 4.4,wehave μ(e b) I μ(e b) for all n i j 1 ≤ i < j ≤ n. Since I is irreflexive, it follows that the set M ={μ(e b) | i ∈{1,..., n}} has n elements. Moreover, since I is the symmetric closure of ,wehave μ(e b) μ(e b) or μ(e b)  μ(e b) for all i = j. Since  is acyclic, this implies that it is j j i 123 T. Kahl transitive on M. Indeed, if μ(e b)  μ(e b) and μ(e b)  μ(e b), then k = i and i j j k μ(e b)  μ(e b), which implies μ(e b)  μ(e b). Hence  is a strict total order on k i i k M. Since M has n elements, it follows that there exists a unique permutation ϑ ∈ S b n such that μ(e b)  μ(e b) ϑ (i ) ϑ ( j ) b b for all 1 ≤ i < j ≤ n. It remains to check that ϑ is a morphism of precubical sets. Let b ∈ B (n ≥ 1), i ∈{1,..., n}, and k ∈{0, 1}.If n ≤ 2, then d ϑ = id = ϑ k . Suppose that n ≥ 3. i b d b We have e b, 1 ≤ j < i , e d b = e b, i ≤ j < n. j +1 Since parallel edges of a cube have the same label (see, e.g., Kahl (2019, Lemma 4.6)), 1 0 we have μ(e d b) = μ(e d b) for all j ∈{1,..., n − 1}. Hence for k ∈{0, 1}, j j i i μ(e b), 1 ≤ j < i , μ(e d b) = μ(e b), i ≤ j < n. j +1 We therefore have −1 μ(e d b), j <ϑ (i ), ϑ ( j)< i , ⎪ ϑ ( j ) b i b k −1 μ(e d b), j <ϑ (i ), ϑ ( j)> i , k ϑ ( j )−1 b b i b μ(e d b) = d ϑ ( j ) i b i k −1 ⎪ μ(e d b), j ≥ ϑ (i ), ϑ ( j + 1)< i , ϑ ( j +1) b ⎪ b i b k −1 μ(e d b), j ≥ ϑ (i ), ϑ ( j + 1)> i ϑ ( j +1)−1 b b i b −1 μ(e b), j <ϑ (i ), ϑ ( j ) b b −1 μ(e b), j ≥ ϑ (i ). ϑ ( j +1) b b −1 Let 1 ≤ j < r ≤ n − 1. If j < r <ϑ (i ),wehave k k μ(e d b) = μ(e b)  μ(e b) = μ(e d b). d ϑ ( j ) ϑ ( j ) ϑ (r ) d ϑ (r ) i b i b b i b i −1 If j <ϑ (i ) ≤ r,wehave k k μ(e d b) = μ(e b)  μ(e b) = μ(e d b). d ϑ ( j ) ϑ ( j ) ϑ (r +1) d ϑ (r ) i b i b b i b i −1 If ϑ (i ) ≤ j < r,wehave k k μ(e d b) = μ(e b)  μ(e b) = μ(e d b). d ϑ ( j ) ϑ ( j +1) ϑ (r +1) d ϑ (r ) i b i b b i b i Thus, ϑ = d ϑ . i b d b 123 On the homology language of HDA models of transition systems Lemma 5.3 Let B = (B,(id, ı ), S × F,μ) be an HDA satisfying HM1 and HM2 with respect to ST and I . Then there exists a unique morphism of graded sets φ : B → Q such that φ : B → Q is the isomorphism given by (id, x ) → x and such that ≤1 ≤1 ≤1 k k d φ(b) = φ(d b) for all b ∈ B (n ≥ 1),i ∈{1,..., n}, and k ∈{0, 1}. i ϑ (i ) Proof We construct φ inductively. Let n ≥ 2, and suppose we have constructed φ up k k to degree n − 1. Let b ∈ B . Consider the elements y = φ(d b) ∈ Q . Suppose n n−1 i ϑ (i ) that 1 ≤ i < j ≤ n. By Lemma 5.2, ϑ l = d ϑ and ϑ k = d ϑ . ϑ ( j ) b ϑ (i ) b b b d b d b ϑ ( j ) ϑ (i ) b b Hence, by the inductive hypothesis and Proposition 2.2, k l k l k l d y = d φ(d b) = φ(d d b) i j i ϑ ( j ) d ϑ (i ) ϑ ( j ) b b b ϑ ( j ) l k l k = φ(d d b) = d φ(d b) j −1 d ϑ ( j −1) ϑ (i ) ϑ (i ) ϑ (i ) b b b l k = d y . j −1 i If n = 2, we also have 0 0 0 1 1 1 λ(y ) = λ(φ (d b)) = μ(d b) = μ(d b) = λ(φ (d b)) = λ(y ) i ϑ (i ) ϑ (i ) ϑ (i ) ϑ (i ) i b b b b for all i ∈{1, 2}. Moreover, by Lemma 5.2, 0 0 0 λ(y ) = λ(φ (d b)) = μ(d b) = μ(e b) ϑ (1) 2 ϑ (2) ϑ (2) b b b 0 0 0 μ(e b) = μ(d b) = λ(φ (d b)) = λ(y ). ϑ (2) b ϑ (1) ϑ (1) 1 b b k k By Proposition 4.3, there exists a unique cube y ∈ Q such that d y = y for all i i k ∈{0, 1} and i ∈{1,..., n}.Weset φ(b) = y. This defines φ in degree n. Lemma 5.4 SQ satisfies HM1 and HM2 with respect to ST and I . Proof HM1: We have (SQ) = ((SQ) ,(id, ı ), S × F,μ) = (SQ ,(id, ı ), S × F,μ) ≤1 ≤1 0 ≤1 0 = (SX,(id, ı ), S × F,μ) = ST . HM2: Let (θ , x ) ∈ (SQ) = S × Q .For i ∈{1, 2}, 2 2 2 0 0 0 0 μ(d (θ , x )) = μ(d θ, d x ) = μ(id, d x ) = λ(d x ). i −1 −1 −1 θ (i ) θ (i ) θ (i ) Thus if θ = id, 0 0 0 0 μ(d (θ , x )) = λ(d x )  λ(d x ) = μ(d (θ , x )). 2 2 1 1 If θ is the transposition (21), 0 0 0 0 μ(d (θ , x )) = λ(d x )  λ(d x ) = μ(d (θ , x )). 1 2 1 2 0 0 In both cases, μ(d (θ , x )) I μ(d (θ , x )). 2 1 123 T. Kahl Lemma 5.5 In SQ, ϑ = θ for all elements (θ , x ). (θ ,x ) Proof Let (θ , x ) ∈ (SQ) . We may suppose that n ≥ 2. By Kahl (2022, Prop. 4.3), e (θ , x ) = (id, e x ). Hence −1 θ (i ) μ(e (θ , x )) = μ(id, e −1 x ) = λ(e −1 x ). θ (i ) θ (i ) Thus, μ(e (θ , x )) = λ(e x ). By Proposition 4.4, θ(i ) i μ(e (θ , x )) = λ(e x )  λ(e x ) = μ(e (θ , x )) θ(i ) i j θ( j ) for all 1 ≤ i < j ≤ n. Consequently, by Lemma 5.2, ϑ = θ. (θ ,x ) Proposition 5.6 SQ is an HDA model of ST with respect to I . Proof By Lemma 5.4, we only have to show HM3 and HM4. HM3: Let m ≥ 2, and let (σ, x ), (θ , y) ∈ (SQ) = S × Q such that d (σ, x ) = m m m k k k d (θ , y) for all r ∈{1,..., m} and k ∈{0, 1}. Then (d σ, d x ) = (d θ, d y) r r −1 −1 σ (r ) θ (r ) for all r and k.If m ≥ 3, this implies (σ, x ) = (θ , y) by Proposition 2.1. In the case m = 2, it is enough to show that σ = θ. Suppose that this is not the case. Then we may assume that σ = id and θ = (21). But then 0 0 0 0 λ(d y) = λ(d x )  λ(d x ) = λ(d y), 1 2 1 2 which is impossible because  is asymmetric. HM4: Suppose that B = (B,(id, ı ), S × F,μ) is an HDA satisfying conditions HM1–HM3 with respect to ST and I that contains SQ as a sub-HDA. We have to show that B = SQ. Since SQ ⊆ B, the maps ϑ : B → S and ϑ : SQ → S coincide on SQ.Let φ : B → Q be the map of graded sets of Lemma 5.3. The corresponding map for SQ is the map ψ : SQ → Q given by ψ(θ, x ) = x. Indeed, by Lemma 5.5, k k k k k d ψ(θ, x ) = d x = ψ(d θ, d x ) = ψ(d θ, d x ) = ψ(d (θ , x )) = θ(i ) θ(i ) −1 i i i θ(i ) θ (θ (i )) ψ(d (θ , x )). Since SQ ⊆ B, the restriction of φ to SQ is ψ. ϑ (i ) (θ ,x ) By HM1, B = (SQ) .Let m ≥ 2, and suppose inductively that B = (SQ) . ≤1 ≤1 <m <m k k Let b ∈ B . By the inductive hypothesis, d b ∈ (SQ) . Write d b = (θ , x ).We m m−1 i i have k k k k d (ϑ ,φ(b)) = (d ϑ , d φ(b)) = (ϑ k ,φ(d b)) = (ϑ k ,ψ(d b)) b i b −1 i d b i d b i ϑ (i ) i i = (ϑ ,ψ(θ, x )) = (θ , x ) = d b. (θ ,x ) By HM3, it follows that b = (ϑ ,φ(b)) ∈ (SQ) . b m Funding Open access funding provided by FCT|FCCN (b-on). This research was supported by FCT (Fun- dação para a Ciência e a Tecnologia, Portugal) through projects UIDB/00013/2020 and UIDP/00013/2020. Declarations Conflict of interest The author declares that there is no conflict of interest. 123 On the homology language of HDA models of transition systems Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/. References Bourbaki, N.: Algebra I. Addison-Wesley (1974) Brown, R., Higgins, P.J.: On the algebra of cubes. J. Pure Appl. Algebra 21(3), 233–260 (1981) Fahrenberg, U.: Higher-dimensional automata from a topological viewpoint, Ph.D. thesis, Aalborg University, Denmark, (2005) Fiedorowicz, Z., Loday, J.-L.: Crossed simplicial groups and their associated homology. Trans. Am. Math. Soc. 326(1), 57–87 (1991) Gaucher, P.: Combinatorics of labelling in higher-dimensional automata. Theor. Comput. Sci. 411, 1452– 1483 (2010) Goubault, E., Mimram, S.: Formal relationships between geometrical and classical models for concurrency. Electr. Notes Theor. Comput. Sci. 283, 77–109 (2012) Grandis, M., Mauri, L.: Cubical sets and their site. Theory Appl. Categories 11(8), 185–211 (2003) Kahl, T.: pg2hda [Computer software], http://w3.math.uminho.pt/~kahl/, 2018–2022 Kahl, T.: Labeled homology of higher-dimensional automata. J. Appl. Comput. Topol. 2(3–4), 271–300 (2018) Kahl, T.: Higher-dimensional automata modeling shared-variable systems. Log. Methods Comput. Sci. 15(3), 28:1-28:21 (2019) Kahl, T.: Weak equivalence of higher-dimensional automata. Discrete Math. Theor. Comput. Sci. 23(1), 1–31 (2021) Kahl, T.: On symmetric higher-dimensional automata and bisimilarity. Theor. Comput. Sci. 935, 47 (2022) Krasauskas, R.: Skew-simplicial groups. Lith. Math. J. 27, 47–54 (1987) Mazurkiewicz, A.: Introduction to trace theory, the book of traces (V. Diekert and G. Rozenberg, eds.), World Scientific, 3–41 (1995) Mazurkiewicz, A.: Trace theory, petri nets: applications and relationships to other models of concurrency (W. Brauer, W. Reisig, and G. Rozenberg, eds.), Lecture Notes in Computer Science, vol. 255, Springer, pp. 279–324 (1987) Pratt, V.: Modeling Concurrency with Geometry, POPL ’91, Proceedings of the 18th ACM SIGPLAN- SIGACT symposium on Principles of programming languages, ACM New York, NY, USA, 311–322 (1991) van Glabbeek, R.J.: On the expressiveness of higher dimensional automata. Theor. Comput. Sci. 356(3), 265–290 (2006) Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, S.S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science: Semantic Modelling, pp. 1–148. Oxford University Press (1995) Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Journal

Journal of Applied and Computational Topology – Springer Journals

Published: May 4, 2023

Keywords: Higher-dimensional automata; Transition system; Homology language; 55N35; 68Q85

There are no references for this article.