Thi Thieu

Hoa Le

Roberto Passerone

Uli Fahrenberg

Axel Legay

A Tag Contract Framework for Heterogeneous Systems

In the distributed development of modern IT systems, contracts play a vital role in ensuring interoperability of components and adherence to specifications. The design of embedded systems, however, is made more complex by the heterogeneous nature of components, which are often described using different models and interaction mechanisms. Composing such components is generally not well-defined, making design and verification difficult. Several frameworks, both operational and denotational, have been proposed to handle heterogeneity using a variety of approaches. However, the application of heterogeneous operational models to contract-based design has not yet been investigated. In this work, we adopt the operational mechanism of tag machines to represent heterogeneous systems and construct a full contract model. We introduce heterogeneous composition, refinement, dominance, and compatibility between contracts, altogether enabling a formalized and rigorous design process for heterogeneous systems.

Introduction

Modern computing systems are increasingly being built by composing components which are developed concurrently by different design teams. In such a paradigm, the distinction between what is constrained on environments, and what must be guaranteed by a system given the constraint satisfaction, reflects the different roles and responsibilities in the system design procedure. Such distinction can be captured by a component model called contract [START_REF] Sangiovanni-Vincentelli | Taming Dr. Frankenstein: Contractbased design for cyber-physical systems[END_REF]. Formally, a contract is a pair of assumptions and guarantees which intuitively are properties that must be satisfied by all inputs and outputs of a design, respectively. The separation between assumptions and guarantees supports the distributed development of complex systems and allows subsystems to synchronize by relying on associated contracts.

In the particular context of embedded systems, heterogeneity is a typical characteristic since these systems are usually composed from parts developed using different methods, time models and interaction mechanisms. To deal with heterogeneity, several modeling frameworks have been proposed oriented towards the representation and simulation of heterogeneous systems, such as the Ptolemy framework [START_REF] Brooks | Heterogeneous concurrent modeling and design in Java (Volume 1: Introduction to Ptolemy II)[END_REF], or towards the unification of their interaction paradigms, such as those based on tagged events [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]. The latter can capture different notions of time, e.g., physical time, logical time, and relate them by mapping tagged events over a common tag structure. However, due to the significant inherent complexity of heterogeneity, there have been only very few attempts at addressing heterogeneity in contract-based models. For instance, the HRC model from the SPEEDS project 3 was designed to deal with different viewpoints (functional, time, safety, etc.) of a single component [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF][START_REF] Damm | Using contract-based component specifications for virtual integration testing and architecture design[END_REF]. However, the notion of heterogeneity in general is much broader than that between multiple viewpoints, and must take into account diverse interaction paradigms. Meanwhile, heterogeneous modeling frameworks have not been related to contract-based design flows. This has motivated us to study a methodology which allows heterogeneous systems to be modeled and interconnected in a contract-based fashion. To this end, we advocate using Tag Machines [START_REF] Benveniste | Tag machines[END_REF] (TMs) to represent sets of tagged events or tag systems. The original notion of TMs was homogeneous [START_REF] Benveniste | Tag machines[END_REF] and was only recently extended to become heterogeneous [START_REF] Le | Tag machines for modeling heterogeneous systems[END_REF]. Our main contribution in this paper is a tag contract framework built on top of heterogeneous TMs and the definition of a full set of contract operations such as implementation satisfaction, contract refinement, contract dominance and contract compatibility.

The rest of the paper is organized as follows. In Sect. 2, we recall basic notions of tag behaviors and tag machines. Section 3 presents our tag contract methodology for heterogeneous systems built on top of TM operations such as composition, quotient, conjunction and refinement. In the same section, we discuss an application of our methodology to a simplified water control problem and model it using incrementing TMs. Finally we concludes in Sect. 4. Related Work. The notion of contract was first introduced by Bertrand Meyer in his design-by-contract method [START_REF] Meyer | Applying "Design by contract[END_REF], based on ideas by Dijkstra [START_REF] Dijkstra | Guarded commands, non-determinancy and a calculus for the derivation of programs[END_REF], Lamport [START_REF] Lamport | win and sin: Predicate transformers for concurrency[END_REF], and others, where systems are viewed as abstract boxes achieving their common goal by verifying specified contracts. De Alfaro and Henzinger subsequently introduced interface automata [START_REF] De Alfaro | Interface automata[END_REF] for documenting components and establish a more general notion of contract, where pre-conditions and post-conditions, which originally appeared in the form of predicates, are generalized to behavioral interfaces. The differentiation between assumptions and guarantees, which is somewhat implicit in interface automata, is made explicit in the contract framework of the SPEEDS HRC model [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF][START_REF] Benvenuti | A contractbased formalism for the specification of heterogeneous systems[END_REF]. The relationship between specifications of component behaviors and contracts is further studied by Bauer et al. [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF] where a contract framework can be built on top of any specification theory equipped with a composition operator and a refinement relation which satisfy certain properties. Trace-based contract theories [START_REF] Benveniste | Multiple viewpoint contract-based specification and design[END_REF][START_REF] Benvenuti | A contractbased formalism for the specification of heterogeneous systems[END_REF] are also demonstrated to be instances of such framework. We take advantage of this formalization in this work to construct our contract theory.

Heterogeneity theory has been evolving in parallel with contract theory, to assist designers in dealing with heterogeneous composition of components with various Models of Computation and Communication (MoCC). Handling heterogeneous MoCC can be done strictly hierarchically in the pioneering framework of Ptolemy II [START_REF] Brooks | Heterogeneous concurrent modeling and design in Java (Volume 1: Introduction to Ptolemy II)[END_REF], meaning that each level of the hierarchy is homogeneous while different interacting mechanisms are allowed to be specified at different levels in the hierarchy. The metroII framework [START_REF] Davare | METROII: A design environment for cyber-physical systems[END_REF] relaxes this limitation, and allows designers to build direct model adapters. However, metroII treats components mostly as black boxes using a wrapping mechansim to guarantee flexibility in the system integration, making the development of an underlying theory complex. These and other similar frameworks are mainly focused on handling heterogeneity at the level of simulation. Another body of work is instead oriented to-3 www.speeds.eu.com wards the formal representation, verification and analysis of these system. In particular, Benveniste et al. [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF] propose a heterogeneous denotational semantics inspired by the Lee and Sangiovanni-Vincentelli formalism of tag signal models [START_REF] Lee | A framework for comparing models of computation[END_REF], which has been long advocated as a unified modeling framework capable of capturing heterogeneous MoCC. In both models, tags play an important role in capturing various notions of time, where each tag system has its own tag structure expressing an MoCC. Composing such system is thus done by applying mappings between different tag structures. Tag machines (TM) [START_REF] Benveniste | Tag machines[END_REF] are subsequently introduced as finite representations of homogeneous tag systems. We have chosen to use this formalism for our work, as it provides an operational representation based on rigorous and proven semantics, and extended their definition to encompass heterogeneous components [START_REF] Le | Tag machines for modeling heterogeneous systems[END_REF]. TMs are quite expressive, e.g., they have been applied to model a job-shop specification [START_REF] Dey | A tag machine based performance evaluation method for job-shop schedules[END_REF] where any trace of the composite tag machine from the start to the final state results in a valid job-shop schedule. Alternatively, tag systems can be represented by functional actors forming a Kleene algebra [START_REF] Dey | A Kleene algebra of tagged system actors[END_REF]. The approach is similar to that of Ptolemy II in that both use actors to represent basic components.

Background

We consider a component to be a set of behaviors in terms of sets of events that take place at its interface, intended as a collection of visible ports. Tags, which are associated to every event, characterize the temporal evolution of the behaviors. By changing the structure of tags, one can choose among different notions of time. Formally, a tag structure T is a pair (T, ≤) where T is a set of tags and ≤ is a partial order on the tags. The tag ordering is used to resolve the ordering among events at the system interface. For instance, using the set of real numbers as tags with their usual ordering, one can place events anywhere in real time. Conversely, a set of partially ordered symbolic tags can be used to express precedence between events in a branching-time setting.

Tag Behaviors

Events occur at the interface of a component. A component exposes a set V of variables (or ports) which can take values from a set D. An event is a snapshot of a variable state, capturing the variable value at some point in time. Formally, an event e on a variable v ∈ V is a pair (τ, d) of a tag τ ∈ T and a value d ∈ D. The simplest way of characterizing a behavior is as a collection of events for each variable. To construct behaviors incrementally, the events of a variable are indexed into a sequence, with the understanding that events later in the sequence have larger tags [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]. A behavior for a variable v is therefore a function N → (T × D). A behavior σ for a component assigns a sequence of events to every variable in V , and is thus a function:

σ ∈ V → (N → (T × D)).
Each event of behavior σ is identified by a tuple (v, n, τ, d), capturing the n-th occurrence of variable v as a pair of a tag τ and a value d. In the following, we denote with Σ(V, T ) the universe of all behaviors over a set of variables V and tag structure T .

Combining behaviors over the same tag structure, or homogeneous behaviors, amounts to computing their intersection provided that they are consistent, or unifiable, with each other on the shared variables. Two behaviors σ 1 and σ 2 are considered unifiable, written

σ 1 ⊲⊳ σ 2 , if σ 1 | V1∩V2 = σ 2 | V1∩V2
, where σ| W denotes the restriction of behavior σ to the variables in set W . When unifiable, we may construct a unified behavior σ = σ 1 ⊔σ 2 on the set of variables V 1 ∪ V 2 as the combination of the two behaviors:

σ(v) = (σ 1 ⊔ σ 2 )(v) def = σ 1 (v) for v ∈ V 1 , σ 2 (v) for v ∈ V 2 .
When the behaviors are defined on different tag structures, before unifying them, the set of tags must be equalized by mapping them onto a third tag structure that functions as a common domain. The mappings are called tag morphisms and must preserve the order.

Definition 1 ([3]

). Let T and T ′ be two tag structures. A tag morphism from T to T ′ is a total map ρ : T → T ′ such that ∀τ 1 , τ 2 ∈ T :

τ 1 ≤ τ 2 ⇒ ρ(τ 1 ) ≤ ρ(τ 2 ).
Here, the tag orders must be taken on the respective domains. Using tag morphisms, we can turn a T -behavior

σ ∈ V → (N → (T × D)) into a T ′ -behavior σ • ρ ∈ V → (N → (T ′ × D))
by simply replacing all tags τ in σ with the image ρ(τ ). Unification of heterogeneous behaviors can be done on the common tag structure. Let ρ 1 : T 1 → T and ρ 2 : T 2 → T be two tag morphisms into a tag structure T . Two behaviors σ 1 and σ 2 defined on T 1 and T 2 respectively are unifiable in the heterogeneous sense, written σ 1 ⊲⊳ ρ1 ρ2 σ 2 , if and only if

(σ 1 • ρ 1 ) ⊲⊳ (σ 2 • ρ 2 ). The unified behavior σ over T is then σ = (σ 1 • ρ 1 ) ⊔ (σ 2 • ρ 2 ).
It is convenient, however, to retain some information of the original tag structures in the composition, since they are often referred to in the heterogeneous composition, as we will see in the sequel. To do so, we construct the behavior composition over the fibered product [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]

T 1 × ρ1 ρ2 T 2 = (T 1 × ρ1 ρ2 T 2 , ≤)
of the original tag structures, extending the order component-wise as follows:

(τ 1 , τ 2 ) ≤ (τ ′ 1 , τ ′ 2 ) ⇐⇒ τ 1 ≤ τ ′ 1 ∧ τ 2 ≤ τ ′ 2 ,
where

T 1 × ρ1 ρ2 T 2 = {(τ 1 , τ 2 ) ∈ T 1 × T 2 : ρ 1 (τ 1 ) = ρ 2 (τ 2 )}.
Example 1. We consider a simplified version of the water controlling system proposed by Benvenuti et al. [START_REF] Benvenuti | A contractbased formalism for the specification of heterogeneous systems[END_REF]. It consists of two components: a water tank and a water level controller, connected in a closed-loop fashion, c.f. Fig. 1. We assume that the water level x(t) is changed linearly as follows:

x(t) def = ∆ t * (f i -f o ) when command is Open h -∆ t * f o when command is Close (1)
where f i and f o denote the constant inlet and outlet flow respectively, h denotes the height when the tank is full of water and ∆ t denotes the time elapsed since t 0 at which the tank reaches the maximum/minimum water level H, i.e., ∆ t = tt 0 . The tank behaviors are naturally defined on tag structure T 1 = (R + ∪ {ǫ 1 }, ≤) and the controller

f i = 2, f o = 1, h = 1:
σ 1 : m : 0.5;p 1.5;l 2.5;p 3.5;l 4.5;p . . . x : 0;0 0.5;0 1;0.5 1.5;1 2;0.5 2.5;0 3;0.5 3.5;1 4;0.5 4.5;0 . . . σ 2 : m 1;p 3;l 5;p 7;l 9;p . . . x : 0;0 1;0 2;0.5 3;1 4;0.5 5;0 6;0.5 7;1 8;0.5 9;0 10;0.5 . . .

These are different behaviors whose composition is only possible under the presence of morphisms such as ρ

i : T i → T 1 given by ρ 1 (τ 1 ) = τ 1 , ρ 2 (τ 2 ) = 0.5 * τ 2 .

Operational Tag Machines

Tag machines were first introduced to represent sets of behaviors in a homogeneous context [START_REF] Benveniste | Tag machines[END_REF] and have been recently extended to encompass the heterogeneous context [START_REF] Le | Tag machines for modeling heterogeneous systems[END_REF]. In order to construct behaviors, the TM transitions must be able to increment time, i.e., to update the tags of the events. An operation of tag concatenation on a tag structure is used to accomplish this.

Definition 2 ([6]

). An algebraic tag structure is a tag structure T = (T, ≤, •) where • is a binary operation on T called concatenation, such that:

1. (T, •) is a monoid with identity element îT 2. ∀τ 1 , τ ′ 1 , τ 2 , τ ′ 2 ∈ T : τ 1 ≤ τ ′ 1 ∧ τ 2 ≤ τ ′ 2 ⇒ τ 1 • τ 2 ≤ τ ′ 1 • τ ′ 2 3. ∃ǫ T ∈ T : ∀τ ∈ T : ǫ T ≤ τ ∧ ǫ T • τ = τ • ǫ T = ǫ T
Tags can be organized as tag vectors τ = (τ v1 , . . . , τ vn ), where n is the number of variables in V . During transition, tag vectors evolve according to a matrix µ : V × V → T called a tag piece [START_REF] Benveniste | Tag machines[END_REF]. The new tag vector is

τ µ = τ • µ where τ v µ def = max(τ u • µ(u, v))
u∈V and the maximum is taken with respect to the tag ordering. As the order is partial, the maximum may not exist, in which case the operation is not defined.

Intuitively, a tag piece µ represents increments in all variable tags over a transition and provides a way to operationally renew them. To represent also changes in variable values, µ can be labeled with a partial assignment ν : V → D, which assigns new values to the variables. Tag piece µ is said to specify an event for all variables for which ν is defined. In the following, we denote by dom(ν) the domain of ν and by L(V, T ) the universe of all labels over a variable set V and tag structure T .

Example 2. The algebraic tag structure (N ∪ {-∞}, ≤, +) can be used to capture logical time by structuring tag pieces µ so that they represent an integer increment of 1. For instance, 1 4 ]. The tag of the second variable is increased by 1 while that of the first variable remains since the least element -∞ = ǫ is used to cancel the contribution of an entry in the tag vector.

[ 1 3 ] • 0 1 -∞ 1 = [
A tag machine M is a finite automaton where transitions are marked by labeled tag pieces, or simply labels.

Definition 3. [7]

A tag machine is a tuple (V, T , S, s 0 , F, E) where:

-V is a set of variables, -T is an algebraic tag structure, -S is a finite set of states and s 0 ∈ S is the initial state, -F ⊆ S is a set of accepting states, -E ⊆ S × L(V, T ) × S is the transition relation.
A run r of a TM is a sequence of states and transitions r :

s 0 µ0 → s 1 µ1 → s 2 . . . s m-1 µm-1 → s m such that s m ∈ F and for all i, 1 ≤ i ≤ m, (s i-1 , µ i-1 , s i ) ∈ E.
Intuitively, a TM is used to construct a behavior by following its labeled transitions over a run, and applying the tag pieces sequentially to the initial tag vector τ = (î T , . . . , îT ). A new event is added to the behavior whenever a new value is assigned by the label function ν i . Run r is valid if the concatenation is always defined along the run and s m ∈ F . The language L(M ) of tag machine M is given by the behaviors of all its valid runs.

Tag Machine Composition

As TMs are used to represent sets of behaviors, combining TMs amounts to considering only behaviors which are consistent with every TMs. In particular, over every transition, the TMs involved in the composition must agree on the tag increment and the value of the shared variables, i.e., their labels are unifiable. While TMs defined on the same tag structure, or homogeneous TMs, can always be composed, TMs on different tag structures, or heterogeneous TMs, can be composed if there exists a pair of algebraic tag morphisms mapping the tag structures T 1 , T 2 to a common tag structure T and preserving the concatenation operator. The homogeneous composition can thus be regarded as a special case of the heterogeneous one when tag morphisms are identity functions mapping a tag to itself.

Definition 4. [7] A tag morphism

ρ : T → T ′ is algebraic if ρ(î T ) = îT ′ and ρ(ǫ T ) = ǫ T ′ and ρ(τ 1 • τ 2 ) = ρ(τ 1 ) • ρ(τ 2 ) for all τ 1 , τ 2 ∈ T .
The newly-composed TM will be defined on a unified tag structure and a unified label set. Referring to the previous notation, two labels µ 1 and µ 2 are unifiable under morphisms ρ 1 and ρ 2 , written µ 1 ⊲⊳ ρ1 ρ2 µ 2 , whenever for all pairs (w, v) ∈ W × W where

W = V 1 ∩ V 2 : ρ 1 (µ 1 (w, v)) = ρ 2 (µ 2 (w, v)), ν 1 (v) = ν 2 (v).
Their unification µ = µ 1 ⊔ ρ1 ρ2 µ 2 is defined over the tag structure T 1 × ρ1 ρ2 T 2 is a set of pieces given by

µ(w, v) =                (µ 1 (w, v), µ 2 (w, v)) if (w, v) ∈ W × W (µ 1 (w, v), τ 2 ) if w ∈ V 1 , v ∈ V 1 \ V 2 (µ 1 (w, v), τ 2 ) if w ∈ V 1 \ V 2 , v ∈ V 1 (τ 1 , µ 2 (w, v)) if w ∈ V 2 \ V 1 , v ∈ V 2 (τ 1 , µ 2 (w, v)) if w ∈ V 2 , v ∈ V 2 \ V 1 (ǫ T1 , ǫ T2 ) otherwise where τ 2 ∈ T 2 is such that ρ 2 (τ 2 ) = ρ 1 (µ 1 (w, v)), and similarly τ 1 ∈ T 1 is such that ρ 1 (τ 1 ) = ρ 2 (µ 2 (w, v)).
The unified labeling function agrees with individual functions on the shared variables:

ν(v) = ν 1 (v) if v ∈ V 1 ν 2 (v) if v ∈ V 2
The composition M = M 1 ρ1 ρ2 M 2 of heterogeneous TMs can then be defined over the unification of heterogeneous tag structures and labels. Definition 5. [START_REF] Le | Tag machines for modeling heterogeneous systems[END_REF] The parallel composition of two tag machines M 1 and M 2 under two algebraic tag morphisms ρ 1 and ρ 2 is the tag machine

M = M 1 ρ1 ρ2 M 2 = (V, T 1 × ρ1 ρ2 T 2 , S, s 0 , F, E) such that -V = V 1 ∪ V 2 , -S = S 1 × S 2 , s 0 = (s 01 , s 02 ), F = F 1 × F 2 , -E = {((s 1 , s 2 ), µ 1 ⊔ ρ1 ρ2 µ 2 , (s ′ 1 , s ′ 2 )) : µ 1 ⊲⊳ ρ1 ρ2 µ 2 ∧ (s i , µ i , s ′ i ) ∈ E i , i = 1, 2}
Since the homogeneous composition is a special case of the heterogeneous one with identity morphisms, we shall omit the morphisms in the homogeneous notations in the sequel.

A Contract Framework for Heterogeneous Systems

Our goal is to use TMs as an operational means for modeling heterogeneous systems in contract-based design flows. To this end, we equip TMs with essential binary operators such as composition to combine two TMs [START_REF] Le | Tag machines for modeling heterogeneous systems[END_REF] and refinement, quotient and conjunction to relate their sets of behaviors. Moreover, we limit TMs to their deterministic form where labeled tag pieces annotated on transitions going out of a state are all different. On top of these TM operators, we propose a heterogeneous contract theory for TMbased specifications with universal contract operators such as composition, refinement and compatibility.

Tag Machine Operators

Two TMs can be related in a refinement relation when the behavior set of one machine is included in that of the other under the morphisms. In the operational point of view, the refined TM can always take a transition unifiable with that taken by the refining TM. Let M i = (V i , T i , S i , s 0i , F i , E i ) be TMs and ρ i : T i → T be algebraic tag morphisms, where i ∈ {1, 2}. The TM refinement is defined as follows.

Definition 6. M 1 refines M 2 , written M 1 ρ1 ρ2 M 2 ,
∃(s 2 , µ 2 , s ′ 2 ) ∈ E 2 : µ 1 ⊲⊳ ρ1 ρ2 µ 2 ∧ (s ′ 1 , s ′ 2 ) ∈ R ∧ (s ′ 1 ∈ F 1 ⇒ s ′ 2 ∈ F 2 )
The following theorem shows that our TM theory supports (homogenous) independent implementability: refinement is preserved when composing components.

Theorem 1. Let M ′ i be TMs defined on T i and

V i . If M 1 M ′ 1 and M 2 M ′ 2 then M 1 ρ1 ρ2 M 2 M ′ 1 ρ1 ρ2 M ′ 2 .
We remark that Theorem 1 only holds for homogenous TM refinement, and note that heterogeneous refinement in general is not preserved even by homogeneous composition. The reason is that the morphisms involved in the former are generally many-to-one functions and can map two different tags into the same tag.

Example 3. We consider an example where:

-

T 1 = {τ 1 }, T 2 = {τ 2 , τ ′ 2 } -V 1 = V 2 = {z}, D z = {⊤} -ρ 1 (τ 1 ) = ρ 2 (τ 2 ) = ρ 2 (τ ′ 2 ) = τ
Let M i , M ′ i be defined on T i and V i where i ∈ {1, 2}. For the sake of simplicity, assume all TMs have a single state which is both initial and accepting state. In addition, there is only one self-loop at this state annotated with µ i for machine M i and µ ′ i for machine

M ′ i such that µ 1 = µ ′ 1 = [τ 1 ], µ 2 = [τ 2 ], µ ′ 2 = [τ ′ 2 ], ν 1 (z) = ν ′ 1 (z) = ν 2 (z) = ν ′ 2 (z) = ⊤. It is easy to see that M 1 ρ1 ρ2 M 2 since µ 1 ⊲⊳ ρ1 ρ2 µ 2 and M ′ 1 ρ1 ρ2 M ′ 2 since µ ′ 1 ⊲⊳ ρ1 ρ2 µ ′ 2 . However, (M 1 M ′ 1 ) ρ1 ρ2 (M 2 M ′ 2 )
since the right composition is empty while the left is not.

While the refinement operator enables us to compare two TMs in terms of sets of behaviors, the composition and quotient operators allow us to synthesize specifications. The TM composition computes the most general specification that retains all unifiable behaviors of two TMs. The dual operator to TM composition is TM quotient which computes the maximal specification as follows.

Definition 7. The quotient M 1 / ρ1 ρ2 M 2 is a machine M = (V, T 12 , S, s 0 , F, E), where

-V = V 1 ∪ V 2 , T 12 = T 1 × ρ1 ρ2 T 2 , s 0 = (s 01 , s 02 ), -S = (S 1 × S 2 ) ∪ {u}, where u is a new universal state, -F = ((S 1 × S 2 ) \ ((S 1 \ F 1 ) × F 2 )) ∪ {u} = (F 1 × F 2 ) ∪ (S 1 × (S 2 \ F 2 )) ∪ {u}, and
E = {((s 1 , s 2 ), µ 1 ⊔ ρ1 ρ2 µ 2 , (s ′ 1 , s ′ 2 )) | (µ 1 ⊲⊳ ρ1 ρ2 µ 2 ) ∧ ((s 1 , µ 1 , s ′ 1 ) ∈ E 1 ) ∧ ((s 2 , µ 2 , s ′ 2 ) ∈ E 2 )} ∪ {((s 1 , s 2 ), µ 1 ⊔ ρ1 ρ2 µ 2 , u) | (∀s ′ 2 ∈ S 2 : (s 2 , µ 2 , s ′ 2 ) / ∈ E 2 ) ∧ (∃µ 1 ∈ L(V 1 , T 1 ) : µ 1 ⊲⊳ ρ1 ρ2 µ 2 )} ∪ {(u, µ, u) | µ ∈ L(V, T 12 )}.
We give an example of a quotient construction in Fig. 4. The dual relation between composition and quotient is presented in the next theorem.

Theorem 2. The quotient M satisfies refinement (M 2 id2 proj 2 M ) proj ′ 1 id1 M 1 where: ∀i ∈ {1, 2}, ∀τ i ∈ T i : id i (τ i ) = τ i ∀i ∈ {1, 2}, ∀(τ 1 , τ 2 ) ∈ T 12 : proj i ((τ 1 , τ 2 )) = τ i ∀(τ 2 , τ 12 ) ∈ T 2 × id2 proj 2 T 12 : proj ′ 1 ((τ 2 , τ )) = proj 1 (τ 12 ) ∀(τ 1 , τ 12 ) ∈ T 1 × id1 proj 1 T 12 : proj ′ 2 ((τ 1 , τ 12 )) = proj 2 (τ 12 )
Moreover, for M ′ defined on T 12 and V :

(M 2 id2 proj 2 M ′ ) proj ′ 1 id1 M 1 ⇒ M ′ M
Thus, the quotient M is the greatest, in the (homogeneous) refinement preorder, of all TMs M ′ defined in Theorem 2. This universal property is generally expected of quotients [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF], and it alone implies that the quotient is uniquely defined up to two-sided homogeneous refinement [START_REF] Fahrenberg | Make a difference! (semantically)[END_REF]. As an example, Fig. 3(c) shows a homogeneous quotient and Fig. 4(b) shows a heterogeneous quotient using the morphisms of Example 1.

Finally, the operator of heterogeneous conjunction, denoted ρ1 ρ2 , is defined as the greatest lower bound of the refinement order. Conjunction, therefore, amounts to computing the intersection of the behavior sets, in order to find the largest common refinement. Thus, for tag machines, conjunction can be computed similarly to composition. The two operators, however, serve very different purposes, and must not therefore be confused.

Tag Contracts

We use the term tag contract to mean that in our framework each contract is coupled with an algebraic tag structure, thereby allowing the contract assumption and guarantee to be represented as TMs. Definition 8. A tag contract C is a homogeneous pair of TMs (M A , M G ) defined over an algebraic tag structure T and variable set V :

M A def = (V, T , S A , s 0A , F A , E A ) M G def = (V, T , S G , s 0G , F G , E G )
Example 4. We consider the simplified water controlling system in Example 1 and present a contract for each component. To simplify the behavioral construction, we rely on a special clock inc added to the variable set of both components. Tag pieces µ are then structured to represent an increment of δ by always assigning δ to µ(inc, inc) and assigning δ to all entries µ(inc, v) where v ∈ dom(µ), and the least element -∞ to other entries. The tags of x and m are thus renewed to the tag of clock inc over every transition. To keep the figures readable we represent tag pieces as [δ]. In addition, the clock value is always equal to its tag and thus is omitted from the labeling function. Figure 2 depicts the tank contract C t = (M At , M Gt ) which guarantees a linear evolution of the water level x(t) (Fig. 2(b)) given the assumption satisfaction (Fig. 2(a)). That is, the water level will evolve linearly as specified in Example 1, provided that the controlling command is received at the right time (i.e., open when the tank is empty and close when it is full). For the sake of simplicity, the events described by the tank contract are timestamped periodically every 0.5 time unit. The controller contract is shown Fig. 3, where it assumes the tank to be empty initially (Fig. 3(a)), i.e., x = 0 and places no requirement on its output which is the command signal. As long as such assumption is satisfied, the controller guarantees (Fig. 3(b)) to send a proper command upon knowing of the tank emptiness or fullness. Intuitively, the controller behaviors ensure timely control over the water evolution while the tank behaviors accept untimely control and allow water spillages or shortages. While the tank system uses physical time to stamp its behaviors, the controller system instead timestamps its events logically, which can be described by the integer tag set N. In both figures, the initial states are marked with short arrows arriving at them and all states are accepting states. For the sake of expressiveness, some of the labeled tag pieces can be represented symbolically. For example, to capture any event of variable x happening at a specific time point within an interval, we label with the tag piece expressions such as x ∈ (0, 1), meaning that in such an event x can take any value between 0 and 1. Similarly, m ∈ {p, l, -} means the command value can either be open, close or undefined. In addition, we use µ t 0 to denote the universe set of labels L(V 1 , T 1 ) and µ c 0 the set of labels L(V 2 , T 2 ).

The tag contract semantics is subsequently defined through the notions of contract environments and implementations. Let M I and M E be TMs defined over tag structure T and variable set V in Def. 8. We call

M E an environment of contract C when M E refines M A . Let [[C]
] e be the set of all such environments, we call

M I an implementa- tion of contract if it holds that ∀M E ∈ [[C]] e : M I M E M G M E .
The set of implementations is similarly denoted by [[C]] p . Hence, the implementation checking is done based on instantiating all possible environments of a contract. Such operation can be performed independently of the assumption instantiation only when the contract is in a special normalized form.

Definition 9. A tag contract C = (M A , M G ) is in normalized form if

and only if:

∀M I : M I ∈ [[C]] p ⇔ M I M G .
Example 5. We use the tag contracts in Example 4 and perform the quotient between the guarantees and assumptions in order to normalize them. Since the tank assumption is the universe of all possible behaviors, i.e., Σ(V 1 , T 1 ), normalizing the tank guarantee adds no more behaviors to the guarantee, i.e., M Gt /M At = M Gt . Figure 3(c), on the other hand, shows the normalized controller guarantee having more behaviors than the un-normalized one. It is easy to see that the behavior σ 1 in Example 1 is included in M Gt and σ 2 is in M Gc /M Ac .

The following theorem states the preservation of tag contract semantics under the normalization operation.

Theorem 3. Normalizing a tag contract C = (M A , M G ) can be done by replacing M G with M G /M A without affecting its semantics.

With Theorem 3, whenever a tag contract is in a normalized form, checking contract satisfaction is reduced to finding a refinement relation between two TMs. As we will see later, working with normalized tag contracts can simplify the formalization of contract operators as well as provide a unique representation for equivalent contracts, thus we will often assume contracts to be in normalized form.

Like other contract frameworks, our tag contract one can identify the refinement and dominance relations between two tag contracts whenever they exist.

Tag Contract Refinement. The refinement relation between two tag contracts is subject to the tag morphisms and is determined by that between their sets of implementations and environments as follows. Let C i = (M Ai , M Gi ) be tag contracts defined on T i and V i and ρ i : T i → T be algebraic tag morphisms where i ∈ {1, 2} Definition 10. Contract C 1 refines contract C 2 under morphisms ρ 1 and ρ 2 , written C 1 ρ1 ρ2 C 2 , if the following two conditions hold:

1. ∀M E2 ∈ [[C 2 ]] e : ∃M E1 ∈ [[C 1 ]] e : M E2 ρ2 ρ1 M E1 2. ∀M I1 ∈ [[C 1 ]] p : ∃M I2 ∈ [[C 2 ]] p : M I1 ρ1 ρ2 M I2
The following theorem shows that when two tag contracts are in normalized form, checking refinement can be done at the syntactic level, i.e., by finding a TM refinement relation between their assumptions and guarantees. Theorem 4. For two normalized tag contracts C 1 and C 2 :

C 1 ρ1 ρ2 C 2 ⇔ (M A2 ρ2 ρ1 M A1 ) ∧ (M G1 ρ1 ρ2 M G2 )
Tag Contract Composition and Dominance. In composing two heterogeneous tag contracts, it is essential to guarantee that composing implementations of each tag contract remains meaningful and results in a new implementation of the newly-composed contract. In addition, every environment of the composite contract should be able to work with any implementation of an individual contract in a way that their composition does not violate the other contract assumption. In fact, there exists a class of contracts, including the composite contract, able to provide such desirable consequences. We refer to them as dominating contracts [START_REF] Bauer | Moving from specifications to contracts in component-based design[END_REF].

Definition 11. A contract C = (M A , M G ) is said to dominate the tag contract pair (C 1 , C 2 ) under morphisms ρ i if : 1. C is defined over tag structure T 12 def = T 1 × ρ1 ρ2 T 2 and variable set V = V 1 ∪ V 2 2. ∀M I1 ∈ [[C 1 ]] p , ∀M I2 ∈ [[C 2 ]] p : M I1 ρ1 ρ2 M I2 ∈ [[C]] p 3. ∀M E ∈ [[C]] e : ∀M I1 ∈ [[C 1 ]] p : (M I1 id1 proj 1 M E ) proj ′ 2 id2 M A2 ∧ ∀M I2 ∈ [[C 2 ]] p : (M I2 id2 proj 2 M E ) proj ′ 1 id1 M A1
where the morphisms are defined as in Theorem 2.

The composition of heterogeneous tag contracts can then be defined as follows.

Definition 12. The composition of tag contracts C 1 and C 2 , written

C 1 ρ1 ρ2 C 2 , is another tag contract ((M A1 / ρ1 ρ2 M G2 ) (M A2 / ρ2 ρ1 M G1 ) swap , M G1 ρ1 ρ2 M G2 ) where swap : T 2 × ρ2 ρ1 T 1 → T 1 × ρ1 ρ2 T 2 is such that swap((τ 2 , τ 1 )) = ((τ 1 , τ 2 )
) and M swap is M where all pieces µ are replaced with µ • swap.

The following theorem states important results for normalized tag contracts. Namely, their contract composition dominates the individual contracts and is the least, in the homogeneous refinement order, of all contracts dominating them under the same morphisms. The next theorem is another of independent implementability: homogeneous tag contract refinement is preserved under the heterogeneous contract composition. Theorem 6. Let C ′ i be normalized tag contracts defined on T i and V i such that C ′ i C i where i ∈ {1, 2}.

1. If C dominates (C 1 , C 2 ) under morphisms ρ 1 and ρ 2 then it also dominates (C ′ 1 , C ′ 2 ) under the same morphisms. 2. (C ′ 1 ρ1 ρ2 C ′ 2 ) (C 1 ρ1 ρ2 C 2 ).
Tag Contract Compatibility. Of particular interest is the notion of compatibility between contracts. This notion depends critically on the particular partition of the variables into inputs and outputs, called profile.

Definition 13. A profile is a tuple π = (i, o) where i/o denotes a set of input/output ports, respectively. Moreover these sets have to be disjoint, i.e., i ∩ o = ∅.

A tag contract defined on some variable set V has profile π = (V i , V o ) if and only if

V = V i ∪ V o .
When composing contracts C i with profiles π i , we enforce the property that each output port should be controlled by at most one contract, i.e., V o 1 ∩ V o 2 = ∅. The composite contract is defined as in Def. 12 and with profile π = ((

V i 1 ∪ V i 2 ) \ (V o 1 ∪ V o 2 ), V o 1 ∪ V o 2
). Example 6. The tank and controller contracts in Example 4 are naturally associated respectively with profiles π 1 = ({x}, {cmd}) and π 2 = ({cmd}, {x}). The profile of their composition is then π 1 = (∅, {x, cmd}).

Intuitively, a contract can only constrain its inputs provided by its environment and provide certain guarantees on its outputs. This is visualized by enforcing the contract assumption to be output-enabled and the contract guarantee to be input-enabled. A tag machine is said to be input(output)-enabled when it accepts all possible combinations of the input(output) values.

When composing different contracts, it is often desirable to ensure that there exists some environment which can discharge all assumptions made by the composition. The contract compatibility is therefore essential in caring for such a need. Two tag contracts C 1 and C 2 are said to be compatible if there exists a contract C e defined over the composite tag structure

T 12 = T 1 × ρ1 ρ2 T 2 and variable set V = V 1 ∪ V 2 with profile π e = (V o 1 ∪ V o 2 , (V i 1 ∪ V i 2 ) \ (V o 1 ∪ V o 2
)) such that: -M Ae ≡ M u , meaning that C e makes no assumptions on its inputs and accepts all possible behaviors defined on L(V, T 12 ). In addition, the composition of C e and

C 1 ρ1 ρ2 C 2 = (M A , M G ) = ((M A1 / ρ1 ρ2 M G2 ) (M A2 / ρ2 ρ1 M G1 ) swap , M G1 ρ1 ρ2 M G2
) should also weaken the assumption made on its environment to the greatest extent. That is (M Ae /M G ) (M A /M Ge ) ≡ M u as well.

-M Ge is input-enabled so as to make contract C e consistent.

In looking for such contract, it is important to notice that M Ae ≡ M u , therefore the condition of (M Ae /M G ) (M A /M Ge ) ≡ M u holds when M Ge is a refinement of M A . Therefore, the compatibility check is reduced to finding a refinement of M A such that it is input-enabled. Since it is easy to verify that both quotients are equivalent to M u , therefore an inputenabled refinement of the composite assumption exists and we can take for example (M A1 / ρ1 ρ2 M G2 ) or (M A2 / ρ2 ρ1 M G1 ) swap . Consequently the two contracts are compatible.

a) Mu (b) MA t / ρ 1 ρ 2 MG c (c) (MA c / ρ 2 ρ 1 MG t )swap

Conclusions

We have presented a modeling methodology based on contracts for designing heterogeneous distributed systems. Heterogeneous systems are usually characterized by their heterogeneity of components which can be of very different nature, e.g. real-time component or logical control component. Without a heterogeneous mechanism, modeling the interaction between components may not be feasible, thereby making it difficult to do verification and analysis based on the known properties of the components. This problem is further complicated for distributed systems where components are developed concurrently by different design teams and are synchronized by relying on their associated contracts. To deal with such problem, we adopt the TM formalism [START_REF] Benveniste | Tag machines[END_REF][START_REF] Le | Tag machines for modeling heterogeneous systems[END_REF] for specifying components in terms of operational behaviors. We subsequently propose a contract methodology for synchronizing heterogeneous components based on a set of useful operations on TMs such as composition, quotient and refinement.

Our next step is to demonstrate our methodology through a prototype tool and validate it through case studies. The development of such a tool is therefore included in our future work.

Proof of Theorem 3.

Let M Ḡ = M G /M A and M q = M Ḡ /M A , then the refinement M q M Ḡ must hold.

Indeed, assume that there exists some run r q in M q and r Ḡ in M Ḡ where the last transition of r q cannot be simulated by r Ḡ : r q : s 0q →, contradicting the assumption. So, every run r q ∈ M q can always be matched by some run r Ḡ ∈ M Ḡ . In addition, if s nq ∈ F q , then one of the following cases can happen:

1. s nq ≡ u q : this implies s n Ḡ ≡ u Ḡ since all possible transitions of the former must be matched by the latter, 2. s nq ∈ F Ḡ × F A : then s n Ḡ ∈ F Ḡ since r q is matched by r Ḡ , 3. s nq ∈ S Ḡ ×(S A \F A ) : then s n Ḡ ∈ F Ḡ since s n Ḡ = (s nG , s nA ) ∈ S G ×(S A \F A ).

((M G1 id1 proj 1 M A ′ ) proj ′ 2 id2 M A2 ) ∧ ((M G2 id2 proj 2 M A ′ ) proj ′ 1 id1 M A1 )
which by Theorem 2 implies:

(M A ′ (M A2 / ρ2 ρ1 M G1 ) swap ) ∧ (M A ′ (M A1 / ρ1 ρ2 M G2 ))
or equivalently M A ′ M A . To prove the second condition of Definition 10, it is sufficient to show that every implementation of C is also an implementation of C ′ . By definition:

M I ∈ [[C]] p ⇔ ∀M E ∈ [[C]] e : M I M E M G M E . By M A ′ M A ,
∀M E ∈ [[C ′ ]] e : M I M E M G M E M G ′ M E . Consequently, M I ∈ [[C ′ ]] p . ⊓ ⊔
Proof of Theorem 6.

The first property holds because the satisfaction of two conditions in Def. 11 can be deduced from the fact that [

[C ′ 1 ]] p ⊆ [[C 1 ]] p , [[C ′ 2 ]] p ⊆ [[C 2 ]] p , M A1 M A ′ 1 , M A2 M A ′

Fig. 1 .

 1 Fig. 1. Water controlling system

Fig. 2 .

 2 Fig. 2. The tank contract

Fig. 3 .

 3 Fig. 3. The controller contract

Theorem 5 .

 5 Let C i be normalized tag contracts and C = C 1 ρ1 ρ2 C 2 . Then: 1. C dominates the contract pair (C 1 , C 2 ) under morphisms ρ 1 and ρ 2 . 2. If C ′ dominates (C 1 , C 2 ) under morphisms ρ 1 and ρ 2 then C C ′ .

(

Fig. 4 . 2 C2Example 7 .

 427 Fig. 4. Quotient components of the composite assumption of C1 ρ 1 ρ 2 C2

→

  By the quotient construction of M Ḡ , r Ḡ implies the existence of runs r A in M A and r G in M G such that:r A : s 0A µ0 → . . . s nA µn → r G : s 0G µ0 → . . . s nG µnBy the quotient construction of M q , r q and r A imply the existence of r ′ Ḡ : in M Ḡ . By determinism, s k Ḡ ≡ s ′ k Ḡ for 0 ≤ k ≤ n and so s n Ḡ µn

2 .

 2 We next show that C = (M A , M Ḡ ) is in a normalized form by showing thatM I ∈ [[ C]] p ⇔ M I M Ḡ . -⇒: Because M I is an implementation of C, it implies that ∀M E ∈ [[ C]] e : (M I M E ) (M Ḡ M E ).Since they are defined on the same tag structure and variable set, we can infer the refinement (M Ḡ M E ) M Ḡ . Thus, ∀M E ∈ [[ C]] e : (M I M E ) M Ḡ . By the quotient definition, we can then infer ∀M E ∈ [[ C]] e : M I (M Ḡ /M E ) from which it follows that:M I ∀M E ∈[[ C]]e (M Ḡ /M E )(2)Since the right side of refinement 2 refines M Ḡ /M A which refines M Ḡ , the refinement M I M Ḡ then follows.-⇐: Because M I M Ḡ , we can infer ∀M E ∈ [[ C]] e : (M I M E ) (M Ḡ M E ). Thus, M I ∈ [[ C]] p .We finally show that C and C have the same set of environments as well as implementations. The former holds since they have the same assumption. The latter holds because of two facts. First,(M G M E ) (M Ḡ M E ) as M G (M G /M A ). Second, (M Ḡ M E ) (M G M E )since any sequence of labels ω = µ 0 . . . µ n of M E also exists in M A and if it exists in M Ḡ as well, it does in M G , too, by the quotient construction of M Ḡ . ⊓ ⊔ Since C and C ′ are defined on the same tag structure and variable set, to prove C C ′ , we first show that M A ′ M A . Since C ′ dominates (C 1 , C 2 ) w.r.t. the same morphisms, the last condition of Definition 11 is satisfied for any environment ME ∈ [[C ′ ]] e : (∀M I1 ∈ [[C 1 ]] p : (M I1 id1 proj 1 M E ) proj ′ 2 id2 M A2 )∧ (∀M I2 ∈ [[C 2 ]] p : (M I2 id2 proj 2 M E ) proj ′ 1 id1 M A1 ) Since M A ′ ∈ [[C ′ ]]e and M Gi ∈ [[C i ]] p , we can infer:

  we can infer [[C ′ ]] e ⊆ [[C]] e . By the second condition of Definition 11, we can infer(M G1 ρ1 ρ2 M G2 ) ∈ [[C ′ ]] p or M G ∈ [[C ′ ]] p . Thus:

2 and

 2 C dominates (C 1 , C 2 ) w.r.t. ρ 1 and ρ 2 . The second property follows directly from the first property of this theorem and the second property of Theorem 5.⊓ ⊔

  if there exists a binary relation R ⊆ S 1 × S 2 such that R contains the initial composite state (s 01 , s 02 ) and for all transitions (s 1 , µ 1 , s ′ 1 ) ∈ E 1 going out of the first component of any state (s 1 , s 2 ) ∈ R :

Thi Thieu Hoa Le, Roberto Passerone, Uli Fahrenberg, and Axel Legay

Appendix

Proof of Theorem 1.

For every run r : s 0 µ1 → s 1 . . . µn → s n in the composition M = M 1 ρ1 ρ2 M 2 , there exists a run r i :

i and M i , M ′ i are defined on the same variable set V i , there must exist another run r ′ i :

i matching r i on all the labels and accepting states. Composing runs r ′ 1 and r ′ 2 results in a run r ′ :

We first construct a refinement relation R and then show that the quotient is the most general TM defined on the T 12 and V satisfying the refinement.

-Initially, R contains the state ((s 02 , (s 01 , s 02 )), s 01 ). If there is a transition from any state (s k2 , (s k1 , s k2 )) in the left TM of the refinement, i.e. the following holds:

By determinism, µ 1 is uniquely defined. This fact together with the existence of two unifiable transitions in M 2 and the quotient M implies there must exist a transition s k1 µ1

, the second refinement condition follows immediately and so

) is an accepting state, then s ′ k2 ∈ F 2 and (s ′ k1 , s ′ k2 ) ∈ F from which we can infer that s ′ k1 ∈ F 1 by construction of F . -Assuming there exists some runs r ′ in M ′ where the last transition s ′ n µn → cannot be matched by M . There are two cases that can happen, r ′ can unify fully with some run r 2 in M 2 or partially with every such run. In the first case, the composition of r ′ and r 2 then refines some run r 1 in M 1 . The existence of r 1 and r 2 together implies the existence of a run r which can fully match r ′ and contradicts the assumption. Similarly, in the second case, assume that r ′ is unifiable from the initial state s ′ 0 up to the k th state s ′ k . Then there exists some run r in M that can match the first k transitions of r ′ and also the rest transitions of r ′ since the (k + 1) th state of r is its universal state. This also contradicts the assumption. Hence the assumption is wrong and such r ′ can always be matched by M . We next assume that M ′ can reach an accepting state s ′ n in r ′ . As before, it can unify fully with some run r 2 in M 2 or partially with every such run. In the first case, the last state of r is (s n1 , s n2 ) where s ni is the last state of run r i . If s n2 ∈ F 2 then s n1 ∈ F 1 (since the composition of r ′ and r 2 refines r 1 by assumption) and so (s n1 , s n2 ) ∈ F . Else, i.e. s n2 / ∈ F 2 , by construction (s n1 , s n2 ) ∈ F . In the second case, the last state of run r is u which is also an accepting state. Therefore M ′ M .

⊓ ⊔

Proof of Theorem 4.

-

] p such that M G1 ρ1 ρ2 M I2 (by the first condition of Def. 10).

Since M I2 M G2 , we can infer that M G1 ρ1 ρ2 M G2 . Using a similar line of reasoning, we can also infer that

Using a similar line of reasoning, we can also deduce that

Proof of Theorem 5.

1. Contract C dominates (C 1 , C 2 ) w.r.t. ρ 1 and ρ 2 for:

(a) C is defined over

By the quotient construction, we know that:

where proj 1 (τ 21 ) = proj 1 • swap(τ 21 ) for τ 21 ∈ T 21 and proj

. We can then rewrite the above refinements:

Because of refinement 3, 4 and M Ii M Gi :

which due to refinement 5, 6 becomes:


Uli Fahrenberg

Axel Legay

History-Preserving Bisimilarity for Higher-Dimensional Automata via Open Maps

Keywords: higher-dimensional automaton, history-preserving bisimilarity, homotopy, unfolding, concurrency

We show that history-preserving bisimilarity for higher-dimensional automata has a simple characterization directly in terms of higher-dimensional transitions. This implies that it is decidable for finite higherdimensional automata. To arrive at our characterization, we apply the open-maps framework of Joyal, Nielsen and Winskel in the category of unfoldings of precubical sets.

Introduction

The dominant notion for behavioral equivalence of processes is bisimulation as introduced by Park [START_REF] David | Concurrency and automata on infinite sequences[END_REF] and Milner [START_REF] Milner | Communication and Concurrency[END_REF]. It is compelling because it enjoys good algebraic properties, admits several easy characterizations using modal logics, fixed points, or game theory, and generally has low computational complexity.

Bisimulation, or rather its underlying semantic model of transition systems, applies to a setting in which concurrency of actions is the same as non-deterministic interleaving; using CCS notation [START_REF] Milner | Communication and Concurrency[END_REF], a|b = a.b+b.a. For some applications however, a distinction between these two is necessary, which has led to development of socalled non-interleaving or truly concurrent models such as Petri nets [START_REF] Petri | Kommunikation mit Automaten[END_REF], event structures [START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF], asynchronous transition systems [START_REF] Marek | Categories of asynchronous systems[END_REF][START_REF] Shields | Concurrent machines[END_REF] and others; see [START_REF] Winskel | Models for concurrency[END_REF] for a survey.

One of the most popular notions of equivalence for non-interleaving systems is history-preserving bisimilarity (or hp-bisimilarity for short). It was introduced independently by Degano, De Nicola and Montanari in [START_REF] Degano | Partial orderings descriptions and observations of nondeterministic concurrent processes[END_REF] and by Rabinovich and Trakhtenbrot [START_REF] Rabinovich | Behavior structures and nets[END_REF] and then for event structures by van Glabbeek and Goltz in [START_REF] Van Glabbeek | Equivalence notions for concurrent systems and refinement of actions[END_REF] and for Petri nets by Best et.al. in [START_REF] Best | Concurrent bisimulations in Petri nets[END_REF]. One reason for its popularity is that it is a congruence under action refinement [START_REF] Best | Concurrent bisimulations in Petri nets[END_REF][START_REF] Van Glabbeek | Equivalence notions for concurrent systems and refinement of actions[END_REF], another its good decidability properties: it has been shown to be decidable for safe Petri nets by Montanari and Pistore [START_REF] Montanari | Minimal transition systems for history-preserving bisimulation[END_REF]. As a contrast, its cousin hereditary hp-bisimilarity is shown undecidable for 1-safe Petri nets by Jurdziński, Nielsen and Srba in [START_REF] Jurdziński | Undecidability of domino games and hhp-bisimilarity[END_REF].

Higher-dimensional automata (or HDA) is another non-interleaving formalism for reasoning about behavior of concurrent systems. Introduced by Pratt [START_REF] Pratt | Modeling concurrency with geometry[END_REF] and van Glabbeek [START_REF] Van Glabbeek | Bisimulations for higher dimensional automata[END_REF] in 1991 for the purpose of a geometric interpretation to the theory of concurrency, it has since been shown by van Glabbeek [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF] that HDA provide a generalization (up to hp-bisimilarity) to "the main models of concurrency proposed in the literature" [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], including the ones mentioned above. Hence HDA are useful as a tool for comparing and relating different models, and also as a modeling formalism by themselves.

HDA are geometric in the sense that they are very similar to the simplicial complexes used in algebraic topology, and research on HDA has drawn on a lot of tools and methods from geometry and algebraic topology such as homotopy [START_REF] Fajstrup | Algebraic topology and concurrency[END_REF][START_REF] Gaucher | Homotopy invariants of higher dimensional categories and concurrency in computer science[END_REF], homology [START_REF] Gaucher | About the globular homology of higher dimensional automata[END_REF][START_REF] Goubault | Homology of higher dimensional automata[END_REF], and model categories [START_REF] Gaucher | Homotopical interpretation of globular complex by multipointed d-space[END_REF][START_REF] Gaucher | Towards a homotopy theory of higher dimensional transition systems[END_REF], see also the survey [START_REF] Goubault | Geometry and concurrency: A user's guide[END_REF].

In this paper we give a geometric interpretation to hp-bisimilarity for HDA, using the open-maps approach introduced by Joyal, Nielsen and Winskel in [START_REF] Joyal | Bisimulation from open maps[END_REF] and results from a previous paper [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF] by the first author. Using this interpretation, we show that hp-bisimilarity for HDA has a characterization directly in terms of (higher-dimensional) transitions of the HDA, rather than in terms of runs as e.g. for Petri nets [START_REF] Fröschle | On plain and hereditary history-preserving bisimulation[END_REF].

Our results imply decidability of hp-bisimilarity for finite HDA. They also put hpbisimilarity firmly into the open-maps framework of [START_REF] Joyal | Bisimulation from open maps[END_REF] and tighten the connections between bisimilarity and weak topological fibrations [START_REF] Adámek | Weak factorization systems and topological functors[END_REF][START_REF] Kurz | Weak factorizations, fractions and homotopies[END_REF].

Due to lack of space, we have had to confer all proofs of this paper to a separate appendix.

Higher-Dimensional Automata

As a formalism for concurrent behavior, HDA have the specific feature that they can express all higher-order dependencies between events in a concurrent system. Like for transition systems, they consist of states and transitions which are labeled with events. Now if two transitions from a state, with labels a and b for example, are independent, then this is expressed by the existence of a two-dimensional transition with label ab. Fig. 1 shows two examples; on the left, transitions a and b are independent, on the right, they can merely be executed in any order. Hence for HDA, as indeed for any formalism employing the so-called true concurrency paradigm, the algebraic law a|b = a.b + b.a does not hold; concurrency is not the same as interleaving.

The above considerations can equally be applied to sets of more than two events: if three events a, b, c are independent, then this is expressed using a threedimensional transition labeled abc. Hence this is different from mutual pairwise independence (expressed by transitions ab, ac, bc), a distinction which cannot be made in formalisms such as asynchronous transition systems [START_REF] Marek | Categories of asynchronous systems[END_REF][START_REF] Shields | Concurrent machines[END_REF] or transition systems with independence [START_REF] Winskel | Models for concurrency[END_REF] which only consider binary independence relations.

An unlabeled HDA is essentially a pointed precubical set as defined below. For labeled HDA, one can pass to an arrow category; this is what we shall do in Section 6. Until then, we concentrate on the unlabeled case.

A precubical set is a graded set X = {X n } n∈◆ together with mappings δ ν k : X n → X n-1 , k ∈ {1, . . . , n}, ν ∈ {0, 1}, satisfying the precubical identity

δ ν k δ µ ℓ = δ µ ℓ-1 δ ν k (k < ℓ) . (1)
The mappings δ ν k are called face maps, and elements of X n are called n-cubes. As above, we shall usually omit the extra subscript (n) in the face maps. Faces δ 0 k x of an element x ∈ X are to be thought of as lower faces, δ 1 k x as upper faces. The precubical identity expresses the fact that (n-1)-faces of an n-cube meet in common (n -2)-faces, see Fig. 2 for an example of a 2-cube and its faces.

Morphisms f : X → Y of precubical sets are graded mappings f = {f n : X n → Y n } n∈◆ which commute with the face maps:

δ ν k • f n = f n-1 • δ ν k for all n ∈ ◆,
k ∈ {1, . . . , n}, ν ∈ {0, 1}. This defines a category pCub of precubical sets and morphisms.

A pointed precubical set is a precubical set X with a specified 0-cube i ∈ X 0 , and a pointed morphism is one which respects the point. This defines a category which is isomorphic to the comma category * ↓ pCub, where * ∈ pCub is the precubical set with one 0-cube and no other n-cubes. Note that * is not terminal in pCub (instead, the terminal object is the infinite-dimensional precubical set with one cube in every dimension).

Definition 2.1 The category of higher-dimensional automata is the comma cate-

x δ 0 1 x δ 1 1 x δ 0 2 x δ 1 2 x δ 0 1 δ 0 2 x = δ 0 1 δ 0 1 x δ 0 1 δ 1 2 x = δ 1 1 δ 0 1 x δ 1 1 δ 0 2 x = δ 0 1 δ 1 1 x δ 1 1 δ 1 2 x = δ 1 1 δ 1 1 x
Fig. 2. A 2-cube x with its four faces δ 0 1 x, δ 1 1 x, δ 0 2 x, δ 1 2 x and four corners.

gory HDA = * ↓ pCub, with objects pointed precubical sets and morphisms commutative diagrams

* } } { { { { { " " E E E E E X f / / Y .
Hence a one-dimensional HDA is a transition system; indeed, the category of transition systems [START_REF] Winskel | Models for concurrency[END_REF] is isomorphic to the full subcategory of HDA spanned by the one-dimensional objects. Similarly one can show [START_REF] Goubault | Labelled cubical sets and asynchronous transition systems: an adjunction[END_REF] that the category of asynchronous transition systems is isomorphic to the full subcategory of HDA spanned by the (at most) two-dimensional objects. The category HDA as defined above was used in [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF] to provide a categorical framework (in the spirit of [START_REF] Winskel | Models for concurrency[END_REF]) for parallel composition of HDA. In this article we also introduced a notion of bisimilarity which we will review in the next section.

Path Objects, Open Maps and Bisimilarity

With the purpose of introducing bisimilarity via open maps in the sense of [START_REF] Joyal | Bisimulation from open maps[END_REF], we identify here a subcategory of HDA consisting of path objects and path-extending morphisms. We say that a precubical set X is a precubical path object if there is a (necessarily unique) sequence (x 1 , . . . , x m ) of elements in X such that x i = x j for i = j,

• for each x ∈ X there is j ∈ {1, . . . , m} for which

x = δ ν 1 k 1 • • • δ νp kp x j for some indices ν 1 , . . . , ν p and a unique sequence k 1 < • • • < k p ,

and

• for each j = 1, . . . , m -1, there is k ∈ ◆ for which x j = δ 0 k x j+1 or x j+1 = δ 1 k x j . Note that precubical path objects are non-selflinked in the sense of [START_REF] Fajstrup | Algebraic topology and concurrency[END_REF]. If X and Y are precubical path objects with representations (x 1 , . . . , x m ), (y 1 , . . . , y p ), then a morphism f : X → Y is called a cube path extension if x j = y j for all j = 1, . . . , m (hence m ≤ p). Definition 3.1 The category HDP of higher-dimensional paths is the subcategory of HDA which as objects has pointed precubical paths, and whose morphisms are generated by isomorphisms and pointed cube path extensions.

A cube path in a precubical set X is a morphism P → X from a precubical path object P . In elementary terms, this is a sequence (x 1 , . . . , x m ) of elements of X such that for each j = 1, . . . , m -1, there is k ∈ ◆ for which x j = δ 0 k x j+1 (start of new part of a computation) or x j+1 = δ 1 k x j (end of a computation part). We show an example of a cube path in Fig. 3.

A cube path in a HDA i : * → X is pointed if x 1 = i, hence if it is a pointed morphism P → X from a higher-dimensional path P . We will say that a cube path (x 1 , . . . , x m ) is from x 1 to x m , and that a cube x ∈ X in a HDA X is reachable if there is a pointed cube path to x in X.

Cube paths can be concatenated if the end of one is compatible with the beginning of the other: If ρ = (x 1 , . . . , x m ) and σ = (y 1 , . . . , y p ) are cube paths with

y 1 = δ 1 k x m or x m = δ 0 k y 1
for some k, then their concatenation is the cube path ρ * σ = (x 1 , . . . , x m , y 1 , . . . , y p ). We say that ρ is a prefix of χ and write ρ ⊑ χ if there is a cube path ρ for which χ = ρ * σ.

Definition 3.2 A pointed morphism f : X → Y in HDA is an open map if it
has the right lifting property with respect to HDP, i.e. if it is the case that there is a lift r in any commutative diagram as below, for morphisms g : P → Q ∈ HDP, p : P → X, q : Q → Y ∈ HDA: (ii) for any reachable x 1 ∈ X and any y 2 ∈ Y with f (x 1 ) = δ 0 k y 2 for some k, there is x 2 ∈ X for which x 1 = δ 0 k x 2 and y 2 = f (x 2 ); (iii) for any reachable x 1 ∈ X and any cube path (y 1 , . . . , y m ) in Y with y 1 = f (x 1 ), there is a cube path (x 1 , . . . , x m ) in X for which y j = f (x j ) for all j = 1, . . . , m.

P p / / g X f Q q / /
Theorem 3.4 For HDA i : * → X, j : * → Y , the following are equivalent:

(i) X and Y are bisimilar;

(ii) there exists a precubical subset R ⊆ X × Y for which (i, j) ∈ R, and such that for all reachable x 1 ∈ X, y 1 ∈ Y with (x 1 , y 1 ) ∈ R,

• for any x 2 ∈ X for which x 1 = δ 0 k x 2 for some k, there exists y 2 ∈ Y for which y 1 = δ 0 k y 2 and (x 2 , y 2 ) ∈ R, • for any y 2 ∈ Y for which y 1 = δ 0 k y 2 for some k, there exists x 2 ∈ X for which (iii) there exists a precubical subset R ⊆ X × Y for which (i, j) ∈ R, and such that for all reachable x 1 ∈ X, y 1 ∈ Y with (x 1 , y 1 ) ∈ R,

x 1 = δ 0 k x 2 and (x 2 , y 2 ) ∈ R;
• for any cube path (x 1 , . . . , x m ) in X, there exists a cube path (y 1 , . . . , y m ) in Y with (x p , y p ) ∈ R for all p = 1, . . . , m, • for any cube path (y 1 , . . . , y m ) in Y , there exists a cube path (x 1 , . . . , x m ) in X with (x p , y p ) ∈ R for all p = 1, . . . , m.

Note that the requirement that R be a precubical subset, in items (ii) and (iii) above, is equivalent to saying that whenever (x, y) ∈ R, then also (δ ν k x, δ ν k y) ∈ R for any k and ν ∈ {0, 1}.

Homotopies and Unfoldings

In order to reason about hp-bisimilarity, we need to introduce in which cases different cube paths are equivalent due to independence of actions. Following [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], we model this equivalence by a combinatorial version of homotopy which is an extension of the equivalence defining Mazurkiewicz traces [START_REF] Mazurkiewicz | Concurrent program schemes and their interpretations[END_REF].

We say that cube paths (x 1 , . . . , x m ), (y 1 , . . . , y m ) are adjacent if x 1 = y 1 , x m = y m , there is precisely one index p ∈ {1, . . . , m} at which x p = y p , and

• x p-1 = δ 0 k x p , x p = δ 0 ℓ x p+1 , y p-1 = δ 0
ℓ-1 y p , and y p = δ 0 k y p+1 for some k < ℓ, or vice versa,

• x p = δ 1 k x p-1 , x p+1 = δ 1 ℓ x p , y p = δ 1 ℓ-1 y p-1
, and y p+1 = δ 1 k y p for some k < ℓ, or vice versa,

• x p = δ 0 k δ 1 ℓ y p , y p-1 = δ 0 k y p , and y p+1 = δ 1 ℓ y p for some k < ℓ, or vice versa, or • x p = δ 1 k δ 0 ℓ y p , y p-1 = δ 0 ℓ y p , and y p+1 = δ 1 k y p for some k < ℓ, or vice versa. Homotopy of cube paths is the reflexive, transitive closure of the adjacency relation. We denote homotopy of cube paths using the symbol ∼, and the homotopy class of a cube path (x 1 , . . . , x m ) is denoted [x 1 , . . . , x m ]. The intuition of adjacency is rather simple, even though the combinatorics may look complicated, see Fig. 4. Note that adjacencies come in two basic "flavors": the first two above in which the dimensions of x ℓ and y ℓ are the same, and the last two in which they differ by 2.

The following lemma shows that, as expected, cube paths entirely contained in one cube are homotopic (provided that they share endpoints). Lemma 4.1 Let x ∈ X n in a precubical set X and (k 1 , . . . , k n ), (ℓ 1 , . . . , ℓ n ) sequences of indices with k j , ℓ j ≤ j for all j = 1, . . . , n. Let

x j = δ 0 k j • • • δ 0 kn x, y j = δ 0 ℓ j • • • δ 0 ℓn x.
Then the cube paths (x 1 , . . . , x n , x) ∼ (y 1 , . . . , y n , x). We extend concatenation and prefix to homotopy classes of cube paths by defining [x 1 , . . . , x m ] * [y 1 , . . . , y p ] = [x 1 , . . . , x m , y 1 , . . . , y p ] and saying that x ⊑ z, for homotopy classes x, z of cube paths, if there are (x 1 , . . . , x m ) ∈ x and (z 1 , . . . , z q ) ∈ z for which (x 1 , . . . , x m ) ⊑ (z 1 , . . . , z q ). It is easy to see that concatenation is welldefined, and that x ⊑ z if and only if there is a homotopy class ỹ for which z = x * ỹ.

Using homotopy classes of cube paths, we can now define the unfolding of a HDA. Unfoldings of HDA are similar to unfoldings of transition systems [START_REF] Winskel | Models for concurrency[END_REF] or Petri nets [START_REF] Hayman | The unfolding of general Petri nets[END_REF][START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF], but also to universal covering spaces in algebraic topology. The intention is that the unfolding of a HDA captures all its computations, up to homotopy.

We say that a HDA X is a higher-dimensional tree if it holds that for any x ∈ X, there is precisely one homotopy class of pointed cube paths to x. The full subcategory of HDA spanned by the higher-dimensional trees is denoted HDT. Note that any higher-dimensional path is a higher-dimensional tree; indeed there is an inclusion HDP ֒→ HDT. Definition 4.2 The unfolding of a HDA i : * → X consists of a HDA ĩ : * → X and a pointed projection morphism π X : X → X, which are defined as follows:

• Xn = [x 1 , . . . , x m ] | (x 1 , . . . , x m ) pointed cube path in X, x m ∈ X n ; ĩ = [i] • δ0 k [x 1 , . . . , x m ] = σ = (y 1 , . . . , y p ) | y p = δ 0 k x m , σ * x m ∼ (x 1 , . . . , x m ) • δ1 k [x 1 , . . . , x m ] = [x 1 , . . . , x m , δ 1 k x m ] • π X [x 1 , . . . , x m ] = x m Proposition 4.3
The unfolding ( X, π X ) of a HDA X is well-defined, and X is a higher-dimensional tree. If X itself is a higher-dimensional tree, then the projection π X : X → X is an isomorphism. Lemma 4.4 If X is a higher-dimensional automaton and (x 1 , . . . , xm ) is a pointed cube path in X, then (π X x1 , . . . , π X xj ) ∈ xj for all j = 1, . . . , m. Lemma 4.5 For any HDA X there is a unique lift r in any commutative diagram as below, for morphisms g : P → Q ∈ HDP, p : P → X, q : Q → X ∈ HDA: 5. Two simple one-dimensional HDA as objects of HDA and HDA h . In HDA there is no morphism X → Y , in HDA h there is precisely one morphism f : X → Y .

P p / / g Xπ X Q q / /

History-Preserving Bisimilarity

In this section we recall history-preserving bisimilarity for HDA from [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF] and show the main result of this paper: that hp-bisimilarity and the bisimilarity of Def. 3.2 are the same. To do this, we first need to introduce morphisms of homotopy classes of paths and homotopy bisimilarity. Definition 5.1 The category of higher-dimensional automata up to homotopy HDA h has as objects HDA and as morphisms pointed precubical morphisms f : X → Ỹ of unfoldings.

Hence any morphism X → Y in HDA gives, by the unfolding functor, rise to a morphism X → Y in HDA h . The simple example in Fig. 5 shows that the converse is not the case. By restriction to higher-dimensional trees, we get a full subcategory HDT h ֒→ HDA h . Lemma 5.2 The natural projection isomorphisms π X : X → X for X ∈ HDT extend to an isomorphism of categories HDT h ∼ = HDT.

Restricting the above isomorphism to the subcategory HDP of HDT allows us to identify a subcategory HDP h of HDT h isomorphic to HDP.

Definition 5.3 A pointed morphism f : X → Y in HDA h is open if it
has the right lifting property with respect to HDP h , i.e. if it is the case that there is a lift r in any commutative diagram as below, for all morphism g :

P → Q ∈ HDP h , p : P → X, q : Q → Y ∈ HDA h : P p / / g X f Q q / / r ? ?
Y HDA X, Y are homotopy bisimilar if there is Z ∈ HDA h and a span of open maps

X ← Z → Y in HDA h .
The connections between open maps in HDA h and open maps in HDA are as follows.

Lemma 5.4 A morphism f : X → Y in HDA h is open if and only if f : X → Ỹ is open as a morphism of HDA. If g : X → Y is open in HDA, then so is g : X → Ỹ .
We also need a lemma on prefixes in unfoldings. Lemma 5.5 Let X be a HDA and x, z ∈ X. Then there is a cube path from x to z in X if and only if x ⊑ z. Proposition 5.6 For HDA i : * → X, j : * → Y , the following are equivalent:

(i) X and Y are homotopy bisimilar;

(ii) there exists a precubical subset R ⊆ X × Ỹ with ( ĩ, j) ∈ R, and such that for all (x 1 , ỹ1 ) ∈ R,

• for any x2 ∈ X for which x1 = δ 0 k x2 for some k, there exists ỹ2 ∈ Ỹ for which ỹ1 = δ 0 k ỹ2 and (x 2 , ỹ2 ) ∈ R, • for any ỹ2 ∈ Ỹ for which ỹ1 = δ 0 k ỹ2 for some k, there exists x2 ∈ X for which x1 = δ 0 k x2 and (x 2 , ỹ2 ) ∈ R; (iii) there exists a precubical subset R ⊆ X × Ỹ with ( ĩ, j) ∈ R, and such that for all (x 1 , ỹ1 ) ∈ R,

• for any cube path (x 1 , . . . , xn ) in X, there exists a cube path (ỹ 1 , . . . , ỹn ) in Ỹ with (x p , ỹp ) ∈ R for all p = 1, . . . , n,

• for any cube path (ỹ 1 , . . . , ỹn ) in Ỹ , there exists a cube path (x 1 , . . . , xn ) in X with (x p , ỹp ) ∈ R for all p = 1, . . . , n;

(iv) there exists a precubical subset R ⊆ X × Ỹ with ( ĩ, j) ∈ R, and such that for all

(x 1 , ỹ1 ) ∈ R, • for any x2 ⊒ x1 in X, there exists ỹ2 ⊒ ỹ1 in Ỹ for which (x 2 , ỹ2 ) ∈ R, • for any ỹ2 ⊒ ỹ1 in Ỹ , there exists x2 ⊒ x1 in X for which (x 2 , ỹ2 ) ∈ R.
Again, the requirement that R be a precubical subset is equivalent to saying that whenever (x, ỹ) ∈ R, then also (δ ν k x, δ ν k ỹ) ∈ R for any k and ν ∈ {0, 1}. The next result is what will allow us to relate hp-bisimilarity and bisimilarity. Theorem 5.7 HDA X, Y are homotopy bisimilar if and only if they are bisimilar.

The following is an unlabeled version of hp-bisimilarity for HDA as defined in [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF]: Definition 5.8 HDA i : * → X, j : * → Y are history-preserving bisimilar if there exists a relation R between pointed cube paths in X and pointed cube paths in Y for which ((i), (j)) ∈ R, and such that for all (ρ, σ) ∈ R,

• for all ρ ′ ∼ ρ, there exists σ ′ ∼ σ with (ρ ′ , σ ′ ) ∈ R,

• for all σ ′ ∼ σ, there exists ρ ′ ∼ ρ with (ρ ′ , σ ′ ) ∈ R,

• for all ρ ′ ⊒ ρ, there exists σ ′ ⊒ σ with (ρ ′ , σ ′ ) ∈ R,

• for all σ ′ ⊒ σ, there exists ρ ′ ⊒ ρ with (ρ ′ , σ ′ ) ∈ R.

We are ready to show the main result of this paper, which together with Theorem 5.7 gives our characterization for hp-bisimilarity. Theorem 5.9 HDA X, Y are homotopy bisimilar if and only if they are historypreserving bisimilar.

Corollary 5.10 History-preserving bisimilarity is decidable for finite HDA.

Labels

We finish this paper by showing how to introduce labels into the above framework of bisimilarity and homotopy bisimilarity. Also in the labeled case, we are able to show that the three notions of bisimilarity, homotopy bisimilarity and history-preserving bisimilarity agree.

For labeling HDA, we need a subcategory of pCub isomorphic to the category of sets and functions. Given a finite or countably infinite set S = {a 1 , a 2 , . . . }, we construct a precubical set !S = {!S n } by letting !S n = (a i 1 , . . . , a in ) | i k ≤ i k+1 for all k = 1, . . . , n -1 with face maps defined by δ ν k (a i 1 , . . . , a in ) = (a i 1 , . . . , a i k-1 , a i k+1 , . . . , a in ).

Definition 6.1 The category of higher-dimensional tori HDO is the full subcategory of pCub generated by the objects !S.

As any object in HDO has precisely one 0-cube, the pointed category * ↓ HDO is isomorphic to HDO. It is not difficult to see that HDO is indeed isomorphic to the category of finite or countably infinite sets and functions, cf. [START_REF] Goubault | Formal relationships between geometrical and classical models for concurrency[END_REF]. Next we establish a correspondence between split traces [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF] and cube paths in higher-dimensional tori. For us, a split trace over a finite or countably infinite set S is a pointed cube path in !S. Hence e.g. a split trace a + b + a -b + b -(in the notation of [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF]) corresponds to the cube path (i, a, ab, b, bb, b). Both indicate the start of an a event, followed by the start of a b event, the end of an a event, the start of a b event, and the end of a b event. Note that contrary to ST-traces [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], the split trace contains no information as to which of the two b events has terminated at the b -.

By definition, a torus !S on a finite or countably infinite set S = {a 1 , a 2 , . . . } contains all n-cubes (a i 1 , . . . , a in ). Hence we have the following lemma: Lemma 6.4 Let (x 1 , . . . , x m ), (y 1 , . . . , y m ) be pointed cube paths in !S with x m = y m . Then (x 1 , . . . , x m ) ∼ (y 1 , . . . , y m ). ✷ Homotopy classes of split traces are thus determined by their endpoint and length: Corollary 6.5 The unfolding of a higher-dimensional torus i : * → !S ∈ HDO is isomorphic to the pointed precubical set j : * → Y given as follows:

• Y n = {(x, m) | x ∈ !S n , m ≥ n, m ≡ n mod 2}, j = (i, 0) • δ 0 k (x, m) = (δ 0 k x, m -1), δ 1 k (x, m) = (δ 1 k x, m + 1) ✷
The definitions of open maps and bisimilarity in HDA h can now easily be extended to the labeled case. Again, we only need label-preserving morphisms. Definition 6.6 The category of labeled higher-dimensional automata up to homotopy LHDA h has as objects labeled HDA * → X → !S and as morphisms pairs of precubical morphisms (f, σ)

: ( * → X → ! S) → ( * → Ỹ → ! T ) of unfoldings. Definition 6.7 A morphism (f, id) : ( * → X → !S) → ( * → Y → !S) in LHDA h is open if its component f is open in HDA h . Labeled HDA * → X → !S, * → Y → !S are homotopy bisimilar if there is * → Z → !S ∈ LHDA h and a span of open maps X ← Z → Y in LHDA h .
The proof of the next theorem is exactly the same as the one for Theorem 5.7. Theorem 6.8 Labeled HDA X, Y are homotopy bisimilar if and only if they are bisimilar.

✷ Also for the labeled version, we can now show that homotopy bisimilarity agrees with history-preserving bisimilarity. We first recall the definition from [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], where we extend the labeling morphisms to cube paths by λ(x 1 , . . . , x m ) = (λx 1 , . . . , λx m ): Definition 6.9 Labeled HDA *

i - → X λ -→ !S, * j - → Y µ -→ !S
are history-preserving bisimilar if there exists a relation R between pointed cube paths in X and pointed cube paths in Y for which ((i), (j)) ∈ R, and such that for all (ρ, σ) ∈ R,

• λ(ρ) = µ(σ),

• for all ρ ′ ∼ ρ, there exists σ ′ ∼ σ with (ρ ′ , σ ′ ) ∈ R,

• for all σ ′ ∼ σ, there exists ρ ′ ∼ ρ with (ρ ′ , σ ′ ) ∈ R,

• for all ρ ′ ⊒ ρ, there exists σ ′ ⊒ σ with (ρ ′ , σ ′ ) ∈ R,

• for all σ ′ ⊒ σ, there exists ρ ′ ⊒ ρ with (ρ ′ , σ ′ ) ∈ R. Theorem 6.10 Labeled HDA X, Y are homotopy bisimilar if and only if they are history-preserving bisimilar.

Conclusion

We have shown that hp-bisimilarity for HDA can be characterized by spans of open maps in the category of pointed precubical sets, or equivalently by a zig-zag relation between cubes in all dimensions. Aside from implying decidability of hpbisimilarity for HDA, and together with the results of [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], this confirms that HDA is a natural formalism for concurrency: not only does it generalize the main models for concurrency which people have been working with, but it also is remarkably simple and natural.

One major question which remains is whether also hereditary hp-bisimilarity can fit into our framework. Because of its back-tracking nature, it seems that simple unfoldings of HDA are not the right tools to use; one should rather consider some form of back-unfoldings of forward-unfoldings. Given the undecidability result of [START_REF] Jurdziński | Undecidability of domino games and hhp-bisimilarity[END_REF], it seems doubtful, however, that any characterization as simple as the one we have for hp-bisimilarity can be obtained.

Another important question is how HDA relate to other models for concurrency which are not present in the spectrum presented in [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF]. One major such formalism is the one of history-dependent automata which have been introduced by Montanari and Pistore in [START_REF] Montanari | An introduction to history dependent automata[END_REF][START_REF] Montanari | Minimal transition systems for history-preserving bisimulation[END_REF] and have recently attracted attention in model learning [START_REF] Aarts | A theory of history dependent abstractions for learning interface automata[END_REF][START_REF] Aarts | Generating models of infinite-state communication protocols using regular inference with abstraction[END_REF]. We conjecture that up to hp-bisimilarity, HDA are equivalent to history-dependent automata.

With regard to the geometric interpretation of HDA as directed topological spaces, there are two open questions related to the work laid out in the paper: In [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF] we show that morphisms in HDA are open if and only if their geometric realizations lift pointed directed paths. This shows that there are some connections to weak factorization systems [START_REF] Adámek | Weak factorization systems and topological functors[END_REF] here which should be explored; see [START_REF] Kurz | Weak factorizations, fractions and homotopies[END_REF] for a related approach.

In [START_REF] Fahrenberg | Higher-Dimensional Automata from a Topological Viewpoint[END_REF] we relate homotopy of cube paths to directed homotopy of directed paths in the geometric realization. Based on this, one should be able to prove that the geometric realization of the unfolding of a higher-dimensional automaton is the same as the universal directed covering [START_REF] Fajstrup | A convenient category for directed homotopy[END_REF] of its geometric realization and hence that morphisms in HDA h are open if and only if their geometric realizations lift dihomotopy classes of pointed dipaths.

The precise relation of our HDA unfolding to the one for Petri nets [START_REF] Hayman | The unfolding of general Petri nets[END_REF][START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF] and other models for concurrency should also be worked out. A starting point for this research could be the work on symmetric event structures and their relation to presheaf categories in [START_REF] Staton | On the expressivity of symmetry in event structures[END_REF].

Fig. 1 .

 1 Fig. 1. HDA for the CCS expressions a|b (left) and a.b + b.a (right). In the left HDA, the square is filled in by a two-dimensional transition labeled ab, signifying independence of events a and b. On the right, a and b are not independent.

Fig. 3 .

 3 Fig.3. Graphical representation of the two-dimensional cube path (i, a, x, b, bc, c, z, d). Its computational interpretation is that a is executed first, then execution of b starts, and while b is running, c starts to execute. After this, b finishes, then c, and then execution of d is started. Note that the computation is partial, as d does not finish.

Y

  HDA X, Y are bisimilar if there is Z ∈ HDA and a span of open maps X ← Z → Y in HDA. It follows straight from the definition that composites of open maps are again open. By the next lemma, morphisms are open precisely when they have a zig-zag property similar to the one of [22]. Lemma 3.3 For a morphism f : X → Y ∈ HDA, the following are equivalent: (i) f is open;

Fig. 4 .

 4 Fig. 4. Graphical representation of the cube path homotopy (i, a, x, b, bc, c, z, d) ∼ (i, a, x, c, bc, c, z, d) ∼ (i, a, x, c, bc, b, z, d) ∼ (i, a, x, c, y, b, z, d).

Corollary 4 . 6

 46 Fig.5. Two simple one-dimensional HDA as objects of HDA and HDA h . In HDA there is no morphism X → Y , in HDA h there is precisely one morphism f : X → Y .

Definition 6 . 2 Definition 6 . 3

 6263 The category of labeled higher-dimensional automata is the pointed arrow category LHDA = * ↓ pCub → HDO, with objects * → X → !S labeled pointed precubical sets and morphisms commutative diagrams* | | y y y y y " " A morphism (f, id) : ( * → X → !S) → ( * → Y → !S) in LHDA is open if its component f is open in HDA. Labeled HDA * → X → !S, * → Y → !S are bisimilar if there is * → Z → !S ∈LHDA and a span of open maps X ← Z → Y in LHDA.

Appendix: Proofs

Proof of Lemma 3.3. For the implication (i) =⇒ (ii), let p : P → X be a pointed cube path with P represented by (p 1 , . . . , p m ) and p(p m ) = x 1 . Let p m+1 be a cube of dimension one higher than p m , set p m = δ 0 k p m+1 , and let Q be the higherdimensional path represented by (p 1 , . . . , p m , p m+1 ). Let g : P → Q be the inclusion, and define q : Q → Y by q(p j ) = f (p(p j )) for j = 1, . . . , m and q(p m+1 ) = y 2 . We have a lift r : Q → X and can set x 2 = r(p m+1 ).

The implication (ii) =⇒ (iii) can easily be shown by induction. The case y m = δ 0 k y m+1 follows directly from (ii), and the case

To finish the proof, we show the implication (iii) =⇒ (i). Let

Y be a commutative diagram, with P represented by (p 1 , . . . , p m ). Up to isomorphism we can assume that Q is represented by (p 1 , . . . , p m , p m+1 , . . . , p t ) and that g is the inclusion. The cube p(p m ) is reachable in X, and (q(p m ), . . . , q(p t )) is a cube path in Y which starts in q(p m ) = f (p(p m )). Hence we have a cube path (x m , . . . , x t ) in X with x m = p(p m ) and q(p j ) = f (x j ) for all j = m, . . . , t, and we can define a lift r : Q → X by r(p j ) = p(p j ) for j = 1, . . . , m and r(p j ) = x j for j = m + 1, . . . , t. ✷ Proof of Theorem 3.4. For the implication (i) =⇒ (ii), let

Then (i, j) ∈ R because f and g are pointed morphisms, and the other properties follow by Lemma 3.3. The implication (ii) =⇒ (iii) can be shown by a simple induction, and for the implication (iii) =⇒ (i), the projections give a span X

Hence a fan-shaped cube path is a one-dimensional path up to the point where it needs to build up to hit the possibly high-dimensional end cube x m .

Lemma A.1 Any pointed cube path in a higher-dimensional automaton i : * → X is homotopic to a fan-shaped one.

Proof. Let us first introduce some notation: For any pointed cube path (x 1 , . . . , x m ), let n 1 , . . . , n m ∈ ◆ be such that x j ∈ X n j (hence n j is the dimension of x j ), and let

An easy induction shows that jn j is odd for all j. Also, T (x 1 , . . . , x m ) ≥ 1 2 (n 2 m + m -1), with equality if and only if (x 1 , . . . , x m ) is fan-shaped.

Next we show that

By oddity of jn j we have m j=1 n j -m j=1 j ≡ m mod 2, and also

We can now finish the proof by showing how to convert a cube path (x 1 , . . . , x m ) with

, essentially by replacing one of its cubes, called x ℓ below, with another one of dimension n ℓ -2.

If (x 1 , . . . , x m ) is a cube path which is not fan-shaped, then there is an index ℓ ∈ {3, . . . , m -1} for which n ℓ ≥ 2, x ℓ-1 = δ 0 k 2 x ℓ for some k 2 , and x ℓ+1 = δ 1 k 3 x ℓ for some k 3 . Assuming ℓ to be the least such index, we must also have

x ℓ+1 , and we can let x ′ j = x j for j = ℓ and

For this new cube path, we have

, and as k 1 < k 3 , we can apply to the cube path (x ′′ 1 , . . . , x ′′ m ) the argument for the case

x ℓ by another application of the precubical identity (1). Hence we can let x ′′ j = x j for j = ℓ -1 and

We need to show the precubical identity δν

δν k for k < ℓ and ν, µ ∈ {0, 1}. For ν = µ = 1 this is clear, and for ν = µ = 0 one sees that (y 1 , . . . , y p ) ∈ δ0

, by adjacency. The cases ν = 1, µ = 0 and ν = 0, µ = 1 are similar to each other, we only show the former.

x m , and by adjacency,

. The proof that * → X is a higher-dimensional tree follows from Lemma 4.4: Let (x 1 , . . . , xm ), (ỹ 1 , . . . , ỹm ) be pointed cube paths in X with xm = ỹm , then we need to prove that (x 1 , . . . , xm ) ∼ (ỹ 1 , . . . , ỹm ). Let x j = π X xj , y j = π X ỹj for j = 1, . . . , m be the projections, then (x 1 , . . . , x m ), (y 1 , . . . , y m ) are pointed cube paths in X. By Lemma 4.4, (x 1 , . . . , x j ) ∈ xj and (y 1 , . . . , y j ) ∈ ỹj for all j = 1, . . . , m.

By xm = ỹm , we know that (x 1 , . . . , x m ) ∼ (y 1 , . . . , y m ). Let (x 1 , . . . , x m ) = (z Let ℓ ∈ {1, . . . , p -1}, and let α ∈ {1, . . . , m -1} be the index such that z ℓ α = z ℓ+1 α and z ℓ j = z ℓ+1 j for all j = α. Then (z ℓ 1 , . . . , z ℓ j ) = (z ℓ+1 1 , . . . , z ℓ+1 j ) for j < α and (z ℓ 1 , . . . , z ℓ j ) ∼ (z ℓ+1 1 , . . . , z ℓ+1 j ) for j > α, hence there is an adjacency (z ℓ 1 , . . . , zℓ m ) ∼ (z ℓ+1 1 , . . . , zℓ+1 m ). For the last claim of the proposition, if X itself is a higher-dimensional tree, then an inverse to π X is given by mapping x ∈ X to the unique equivalence class Proof of Lemma 4.5. Let (x 1 , . . . , xm ) be a pointed cube path in X, and write x j = π X xj for j = 1, . . . , m. Let (x 1 , . . . , x m , y 1 , . . . , y p ) be an extension in X and define ỹj = [x 1 , . . . , x m , y 1 , . . . , y j ] for j = 1, . . . , p. Then (x 1 , . . . , xm , ỹ1 , . . . , ỹp ) is the required extension in X, which is unique as X is a higher-dimensional tree. ✷ Proof of Lemma 5.2. Using the projection isomorphisms, any morphism Lemma 5.4. For the forward implication of the first claim, let

be a diagram in HDA with g : P → Q ∈ HDP; we need to find a lift Q → X.

Using the isomorphisms π P : P → P , π Q : Q → Q, we can extend this diagram to the left; note that g : P → Q is a morphism of HDP:

Hence we have a diagram

in HDA h , and as g : P → Q is a morphism of HDP h , we have a lift r : Q → X in HDA h . This gives a morphism r : Q → X ∈ HDA in Diagram (3), and by composition with the inverse of the isomorphism π

For the back implication in the first claim, assume f : X → Ỹ ∈ HDA open and let P

Transferring this diagram to the category HDA, we have

and as g : P → Q is a morphism of HDP, we get the required lift.

To prove the second claim, let

/ Ỹ be a diagram in HDA with h : P → Q ∈ HDP. We can extend it using the projection morphisms:

and Lemma 4.5 then gives the required lift r ′ in the diagram

Proof of Lemma 5.5. For the forward implication, let (x, ỹ1 , . . . , ỹp ) be a cube path in X with ỹp = z, let (x 1 , . . . , x m ) ∈ x, and write y j = π X ỹj for all j. By Lemma 4.4, (x 1 , . . . , x m , y 1 , . . . , y p ) ∈ z.

For the other direction, let (x 1 , . . . , x m , y 1 , . . . , y p ) ∈ z such that (x 1 , . . . , x m ) ∈ x, and define ỹj = [x 1 , . . . , x m , y 1 , . . . , y j ] for all j. Then (x, ỹ1 , . . . , ỹp ) is the required cube path from x to z in X. ✷ Proof of Proposition 5.6. The implication (i) =⇒ (ii) follows directly from Theorem 3.4, and (iii) can be proven from (ii) by induction. (We can omit the reachability condition from items (ii) and (iii) because any cube in an unfolding is reachable.) Equivalence of (iii) and (iv) is immediate from Lemma 5.5.

For the implication (iii) =⇒ (i), we can use Theorem 3.4 to get a span In HDA, this is a span X f ← -Z g -→ Ỹ , and composing with the projections yields

) ∈ R as was to be shown. The symmetric condition in Theorem 5.6(iv) can be shown analogously, and one easily sees that R is indeed a precubical set.

For the other implication, let R ⊆ X× Ỹ be a precubical set as in Theorem 5.