A Lemercier

L Bailly
email: lucie.bailly@irphe.univ-mrs.fr

C Geindreau

L Orgéas

V Deplano

ON THE DEVELOPMENT OF NEW ARTIFICIAL MATERIALS MIMICKING AORTIC TISSUE HISTOLOGICAL AND MECHANICAL FEATURES

The aim of this work is to develop a new hyperelastic and anisotropic material mimicking histological and mechanical features of healthy and aneurysmal arterial tissues. The target material is constituted by rhombic periodic lattices of hyperelastic fibres embedded into a soft elastomer membrane. Based on a previous theoretical work yielding to an optimized microstructural arrangement and mechanical behaviour, this study provides experimental advances concerning the manufacturing of new fibrous membranes. Their mechanical characterization under various loadings is presented.

1.

INTRODUCTION

Human abdominal aortic tissue is a complex cylindrical soft sandwich structure, arranged in three different concentric layers. Each layer is characterised by specific histological features, with different associated mechanical properties [START_REF] Holzapfel | A structural model for the viscoelastic behavior of arterial walls: Continuum formulation and finite element analysis[END_REF]. Previous tensile testings conducted on excised aortic specimens have evidenced the highly non-linear and anisotropic mechanical behaviour of human healthy abdominal aorta (AA) and aneurysmal (AAA) tissues [START_REF] Vande Geest | The effects of aneurysm on the biaxial mechanical behavior of human abdominal aorta[END_REF]. This behaviour is usually considered as essentially hyperelastic, the non-linearity of which is ascribed to the particular wavy architecture of the fibrous structures which tend to straighten along the loading direction when they are subjected to a mechanical loading: this provides the arterial tissues a macroscopic mechanical response exhibiting a typical J-shape. Besides, the preferred orientations of the fibrous architecture are responsible for the mechanical anisotropy of the arterial tissues.

During the last decades, several soft materials have been proposed in order to perform in vitro experiments using AAA synthetic analogues, either placed into vascular simulators [START_REF] Deplano | Flow behaviour in an asymmetric compliant experimental model for abdominal aortic aneurysm[END_REF] or inflated until rupture [START_REF] Doyle | Experimental modelling of aortic aneurysms: Novel applications of silicone rubbers[END_REF]. However, such materials are made up of homogeneous elastomers with isotropic material properties, which are very far from the anisotropic hyperelastic behaviour of aortic tissues [START_REF] Vande Geest | The effects of aneurysm on the biaxial mechanical behavior of human abdominal aorta[END_REF] and from their fibrous microstructure.

Therefore, the aim of the present study is to design and characterize the mechanical behaviour of new artificial materials, able to mimic (i) the macroscopic anisotropic properties of AA and AAA tissues, (ii) their hyperelastic J-shape mechanical response, (iii) and their main histological features (multi-layers fibrous structure with distinctive fibre orientations).

2.

METHODS

Optimal materials able to mimic human AA and AAA hyperelastic anisotropic behaviours have been identified in a previous theoretical work using a multi-scale homogenisation process combined with microstructure optimisation [START_REF] Bailly | Towards a biomimetism of abdominal healthy and aneurysmal arterial tissues[END_REF]. Target solutions consist of bi-layers fibrous structure composites, made up of two parallel fibrous lattices embedded into a soft hyperelastic membrane. Based on these results, several types of commercial fibres have been selected and their tensile mechanical behaviours were studied. A specific device dedicated to the manufacturing of periodic fibrous lattices and square composite membranes has been designed so as to control angle between fibres (  ), and fibre length (l0), as displayed on figure 1 (a). In order to validate the manufacturing processes as well as the micro-mechanical modelling developed in [START_REF] Bailly | Towards a biomimetism of abdominal healthy and aneurysmal arterial tissues[END_REF], three kinds of fibrous microstructure have been elaborated, comprising respectively:

(i) A one-layer lattice of straight fibres, able to generate a macroscopic anisotropy; (ii) A one-layer lattice of wavy fibres, able to generate a hyperelastic J-shape mechanical response; (iii) A bi-layers lattice of straight fibres, inspired from the multi-layered structure of biological tissues; The mechanical behaviours of these three types of composites have been characterized under various loadings using a uniaxial tensile-testing device. Microstructural architecture of each fibrous membrane was investigated by means of X-rays micro-tomography.

3.

RESULTS AND DISCUSSIONS

Mechanical behaviours of the matrix material and seven individual fibres will be firstly presented. A high strength RTV Silicone elastomer dispersion (Applied Silicone Corporation) has been first selected as matrix material, due to its transparency, high deformability and specific physical properties allowing liquid injection moulding and room-temperature curing. Among the different fibres, a fluorocarbon fibre has been selected as an appropriate candidate to the design of the intended periodic lattices due to its non-linear behaviour. It has been used to elaborate the three types of composites described above, whose typical microstructure arrangement is illustrated on figure 1 (a).

1 Mechanical behaviours of each composite will be presented and discussed with respect to the individual fibre constitutive law. Figure 1

4.

CONCLUSIONS

This experimental study presents several technical solutions to design one-layer and bi-layers fibrous structure composites. The control of a macroscopic mechanical anisotropy is allowed by changing two microstructural parameters only: the angle between fibres, and the fibre length. Particular cases of straight and wavy fibres are considered. These experiments represent an original database to validate model assumptions presented in previous work [START_REF] Bailly | Towards a biomimetism of abdominal healthy and aneurysmal arterial tissues[END_REF].

5.

  (b) shows a typical example of experimental Cauchy stresses measured as a function of elongation state, on four samples extracted from a one-layer fibrous structure composite with straight fibres. Two different stretching directions are displayed. The anisotropic behavior of the composite is demonstrated at the macroscale.

Figure 1 -

 1 Figure 1 -(a) Typical 3D reconstruction of different periodic fibrous lattices characterized by X-rays microtomography: (from left to right) one-layer lattice of straight fibres; one-layer lattice of wavy fibres; bi-layers lattice of straight fibres. (b) Mechanical behaviour of four samples extracted from a one-layer composite of straight fibres, stretched along two orthogonal directions.

ACKNOWLEDGEMENT

The authors would like to thank Dr. P. Latil and T. Cassigneul for their contribution to this work. They gratefully acknowledge CNRS and the University Joseph Fourier for financial support.

6.


Éric Goubault

Samuel Mimram

Formal Relationships Between Geometrical and Classical Models for Concurrency

A wide variety of models for concurrent programs has been proposed during the past decades, each one focusing on various aspects of computations: trace equivalence, causality between events, conflicts and schedules due to resource accesses, etc. More recently, models with a geometrical flavor have been introduced, based on the notion of cubical set. These models are very rich and expressive since they can represent commutation between any number of events, thus generalizing the principle of true concurrency. While they are emerging as a central tool in concurrency, which is very promising because they make possible the use of techniques from algebraic topology in order to study concurrent computations, they have not yet been precisely related to the previous models, and the purpose of this paper is to fill this gap. In particular, we describe an adjunction between Petri nets and cubical sets which extends the previously known adjunction between Petri nets and asynchronous transition systems by Nielsen and Winskel.

A great variety of models for concurrency was introduced in the last decades: transition systems (with independence), asynchronous automata, event structures, Petri nets, etc. Each of these models focuses on modeling a particular aspect of computations, and even though their nature are very different, they are tightly related to each other as witnessed in [START_REF] Winskel | Models for concurrency[END_REF]. More recently, models inspired by ideas coming from geometry, such as cubical sets (also sometimes called higher dimensional automata or HDA [START_REF] Pratt | Modeling concurrency with geometry[END_REF][START_REF] Goubault | Homology of higher-dimensional automata[END_REF]) or local po-spaces [START_REF] Fajstrup | Algebraic topology and concurrency[END_REF], have emerged as central tools to study concurrency: thanks to their nice algebraic structure, they allow one to carry on abstractly many computations, and they are very expressive because of their ability to represent commutations between multiple events. However, since their introduction, they have not been systematically and formally linked with the other models, such as transition systems, even though cubical sets contain a notion of generalized transition in their very definition.

From a scientific point of view, the mere observation that these models are different is not satisfactory and their links with other models have to be investigated in depth. However, it turns out that their relationship is often quite subtle: the various models are usually not isomorphic, nor even one is a retract of the other. Adjunctions between the categories of models, which generalize Galois connections to categories, are the right notion to relate and compare them. This was first studied in the context of operational models for concurrency by Winskel et al. [START_REF] Winskel | Models for concurrency[END_REF] and extended to geometrical models [START_REF] Goubault | The Geometry of Concurrency[END_REF], but only between fairly restricted categories. In this paper, we greatly improve previous work by extending it to the full categories of transition systems (operational model of "interleaving" concurrency) and of transition systems with independence (operational model of "true" concurrency). Another approach to compare these models, based on history-preserving bisimulations, is developed in [START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF]. The main motivation underlying this work is that, by relating these models, we can compare the semantics of concurrent languages given in different formalisms. This also allows for reusing specific methods for statically analyzing concurrent programs in one model (such as deadlock detection algorithms for cubical sets [START_REF] Fajstrup | Detecting deadlocks in concurrent systems[END_REF], invariant generation on Petri nets [START_REF] Sankaranarayanan | Petri net analysis using invariant generation[END_REF], state-space reduction techniques such as sleep sets and persistent sets in Mazurkiewicz traces [START_REF] Godefroid | Using partial orders for the efficient verification of deadlock freedom and safety properties[END_REF], or stubborn sets in Petri nets [START_REF] Valmari | A stubborn attack on state explosion[END_REF]) in the other. This paper constitutes a major step towards formally relating geometric models with other models for concurrency. The links might appear as intuitive, but the formal step we are making underlines subtle differences between the models: there are many variants of the models, all of which can be embedded in the model of HDA, which allows us to precisely characterize the outcomes of choosing one of the other variant of the models. We have done our best to express in categorical terms how to construct one variant from the other. In particular, most models admits the following variations:

-events can be labeled or not, -morphisms can be strict or partial, -the multiplicity of an event can be taken in account or not, -in the case where the events are labeled, morphisms between labels can be strict or not.

It turns out from this study that strongly labeled HDA seem to be the right notion of HDA, at least for comparing with most other common models of concurrency. This also unravels interesting phenomena (besides being necessary for being able to relate semantics given in different styles) such as the fact that persistent set types of methods for tackling the state-space explosion problem can be seen as searching for retracts of the state space, in the algebraic topological sense. We end this article by making some hypotheses on further relationships, with event structures and Petri nets in particular.

Related work. In this paper, we extend Winskel's results [START_REF] Winskel | Models for concurrency[END_REF], which include adjunctions between transition systems, event structures, trace languages, asynchronous transition systems and Petri nets which are still an active research area [START_REF] Staton | On the expressivity of symmetry in event structures[END_REF]. A first step towards comparing higher-dimensional automata (a form of geometric semantics we are considering here), Petri nets, and event structures is reported in [START_REF] Van Glabbeek | Petri nets, configuration structures and higher dimensional automata[END_REF]. Also, an investigation of the comparison between cubical sets (another form of geometric semantics) and transition systems, as well as transition systems with independence was started in [START_REF] Goubault | Cubical sets are generalized transition systems[END_REF], but never formally published.

We describe right adjoint functors from the categories of transition systems, asynchronous transition systems, Petri nets and prime event structures of [START_REF] Winskel | Models for concurrency[END_REF], to HDA. By general theorems, these functors transport limits onto limits, hence preserve classical parallel semantics based on pullbacks, by synchronized products [START_REF] Arnold | Systèmes de transitions finis et sémantique des processus communicants[END_REF], as the ones in transition systems or the ones of [START_REF] Winskel | Models for concurrency[END_REF]. Cubical sets (or more generally HDA) that we take as the primary model for geometric semantics here, have appeared in numerous previous works, in algebraic topology in particular [START_REF] Serre | Homologie Singulière des Espaces Fibrés[END_REF][START_REF] Brown | On the algebra of cubes[END_REF]. A monoidal presentation can also be found in [START_REF] Grandis | Cubical sets and their site[END_REF]. The basics of "directed algebraic topology" that is at the basis of the mathematics involved in the geometric semantics we use here can be found in [START_REF] Grandis | Directed Algebraic Topology; models of non-reversible worlds[END_REF].

Contents of the paper. We begin by recalling the geometric model provided by cubical sets in Section 1 and some well-known models for concurrent computations (transition systems, asynchronous automata, event structures and Petri nets) in Section 2. We then relate them by defining adjunctions in Section 3. HDA naturally "contain" transition systems (resp. asynchronous transition systems), which just encode the non-deterministic (resp. and pairwise independence) information. Event structures are also shown to be more abstract than HDA: they impose binary conflict relations and conjunctive dependencies (an event cannot depend on a disjunction of two events), and they do not distinguish different occurrences of the same event. Petri nets have a built-in notion of degree of parallelism, as is the case of HDA (given by cell dimension) but impose specific constraints on dynamics. We finally conclude on future works in Section 4.

Geometric models for concurrency

Precubical sets can be thought as some sort of generalized transition systems with higher-dimensional transitions. Similarly to transition systems there is a corresponding notion with "idle transitions", called cubical sets. These classical objects in combinatorial algebraic topology (see for instance [START_REF] Serre | Homologie Singulière des Espaces Fibrés[END_REF]) have been used as an alternative truly concurrent model for concurrency, in particular since the seminal papers [START_REF] Pratt | Modeling concurrency with geometry[END_REF] and [START_REF] Van Glabbeek | Bisimulation semantics for higher dimensional automata[END_REF]. More recently, they have been used in [START_REF] Fajstrup | Detecting deadlocks in concurrent systems[END_REF] and [START_REF] Fajstrup | Algebraic topology and concurrency[END_REF] for deriving new and interesting deadlock detection algorithms. More algorithms have been designed since then, see for instance [START_REF] Raussen | On the classification of dipaths in geometric models for concurrency[END_REF] and [START_REF] Fajstrup | Loops, ditopology, and deadlocks[END_REF]. In the following, we will be mostly using symmetric precubical sets. However, we have done our best to introduce here the notion gradually, and recall some variants as well as important properties.

Cubical sets

A cubical set consists of a family (C(n)) n∈N of sets, the elements of C(n) being called n-cells, together with for every pairs of integers n and i, such that 0 i n, maps

∂ - i , ∂ + i : C(n + 1) → C(n) and ι i : C(n) → C(n + 1)
respectively called source, target and degeneracy maps, satisfying

∂ β j ∂ α i = ∂ α i ∂ β j-1 ι i ι j = ι j-1 ι i (1)
with i < j and α, β ∈ {-, +} and, for every α ∈ {-, +},

∂ α j ι i =      ι i ∂ α j-1 if i < j id if i = j ι i-1 ∂ α j if i > j (2) A morphism κ : C → C ′ between two cubical sets C and C ′ consists of a family (κ n : C(n) → C ′ (n)) n∈N of
functions which is natural: for every index i and α ∈ {-, +},

κ n • ∂ α i = ∂ α i • κ n+1 and κ n+1 • ι i = ι i • κ n
and we write CSet for the category thus defined. The 0-source (resp. 0-target ) of an n-cell x ∈ C(n) is the 0-cell ∂ - 0 . . . ∂ - 0 (x) (resp. ∂ + 0 . . . ∂ + 0 (x)). More conceptually, a cubical set C is a presheaf on the cubical category , that is a functor C : op → Set, and a morphism of cubical sets is a natural transformation between the corresponding functors. Here, the cubical category is defined as the free category on the graph whose objects are natural integers n ∈ N and containing, for every integers i and n such that 0 i n and every α ∈ {-, +}, arrows

ε α i,n : n → n + 1 and η i,n : n + 1 → n (3)
quotiented by the relations expressing axioms dual to those given for cubical sets (1) and ( 2) -so that for every index n, the function C(ε α i,n ) corresponds to ∂ α i and C(η i,n ) corresponds to ι i :

ε β i,n+1 ε α j,n = ε α j-1,n ε β i,n+1 η j,n η i,n+1 = η i,n η j-1,n+1 (4)
with i < j and α, β ∈ {-, +}, and for every α ∈ {-, +},

η i,n ε α j,n =      ε α j-1,n-1 η i,n-1 if i < j id if i = j ε α j,n-1 η i-1,n-1 if i > j.
The precubical category ⊡ is defined similarly with only the ε α i,n as generators and the first equations of (4) as axioms, and a precubical set is a presheaf on the precubical category: a precubical set consists of a family (C(n)) n∈N of sets together with a family of maps ∂ - i , ∂ + i : C(n+1) → C(n) satisfying the equations on the left of (1). We write PCSet for the corresponding category.

Given an integer n, we write n for the full subcategory of whose objects are the integers k n. An n-dimensional cubical set is a presheaf on n and we write CSet n for the category of n-dimensional cubical sets. The inclusion functor n → induces by precomposition a functor U n : CSet → CSet n called the n-truncation functor (see Section 1.7).

Example 1. The geometric intuition underlying cubical sets is the following one. An n-cell x of a cubical set should be seen as an n-dimensional cube, the (n -1)-dimensional cubes ∂ - i (x) and ∂ + i (x) being respectively the source and target in dimension i of x, and the degeneracy maps ι i allowing us to see an n-dimensional cube as an (n + 1)-dimensional one, degenerated in dimension i. So for example, a "cylinder" can be described as a precubical set C with

C(0) = {x, y} C(1) = {f, g, h} C(2) = {α} C(n) = ∅ for n > 2
with the following sources and targets, given by ∂ -

0 (f ) = ∂ + 0 (f ) = ∂ - 0 (h) = x, ∂ - 0 (g) = ∂ + 0 (g) = ∂ + 0 (h) = y, ∂ - 0 (α) = ∂ + 0 (α) = h, ∂ - 1 (α) = f and ∂ + 1 (α) = g.

This cylinder can be pictured graphically as

y g d d α x f e e h c c ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ or x h G G f α y g x h G G y (in an unfold representation)
From a concurrency point of view, a 1-cell corresponds to the occurrence of an event (an action) and an n-cell corresponds to a commutation or an independence between the 1-cells occurring in its faces. The cubical set above representing the cylinder thus corresponds intuitively to a program constituted of two processes in parallel: a (while) loop (the actions f and g) and a single instruction (h). See also Example 9.

In previous example, the two transitions f and g are instances of a same event because they are parallel faces of the square α. This suggests that the notion of event should be reconstructed in a precubical set as an equivalence class of transitions as follows. Suppose given a precubical set C. We define a relation ≈ as the smallest equivalence relation on 1-cells of C, such that for every f, g ∈ C(1), f ≈ g when there exists y ∈ C(2) such that f = ∂ - i (y) and g = ∂ + i (y), for i = 0 or i = 1. An event is the equivalence class of a 1-cell under the relation ≈. Given a morphism κ : C → D between precubical sets, two 1-cells of D in a same event are sent to two 1-cells of D in a same event; any such morphism thus induces a function κ 1 / ≈ from the events of C to the events of D.

A monoidal definition of the cubical category

A shorter description of the cubical category can be given if we take its monoidal structure in account: the cubical category is the free monoidal category (that is, a category equipped with a coherent tensor product and unit [START_REF] Maclane | Categories for the Working Mathematician[END_REF]) containing a co-cubical object [START_REF] Grandis | Cubical sets and their site[END_REF]. This will help in defining very concisely the adjunctions we have in mind in Section 3. Definition 2. A cubical object (C, ε -, ε + , η) in a monoidal category (C, ⊗, I) consists of an object C together with three morphisms

η : I → C ε -: C → I ε + : C → I such that ε -• η = id I = ε + • η A morphism f between two cubical objects (C 1 , ε - 1 , ε + 1 , η 1 ) and (C 2 , ε - 2 , ε + 2 , η 2 ) is a morphism f : C 1 → C 2 such that f • η 1 = η 2 ε - 2 • f = ε - 1 ε + 2 • f = ε + 1 Dually, a co-cubical object (C, ε -, ε + , η) in C is a cubical object in C op .
In the cubical category , (1, ε -, ε + , η) is a co-cubical object. The fact that is the free monoidal category containing a co-cubical object means that all the arrows of can be recovered from those by tensoring with identities

ε α i,n = id i ⊗ ε α ⊗ id n-i and η i,n = id i ⊗ η ⊗ id n-i
and that the axioms satisfied by the morphisms -the axioms dual of (1) and (2) -are precisely those imposed by the axioms of monoidal categories and those of co-cubical objects. This can be equivalently reformulated as follows:

Proposition 3. Given a monoidal category C, the category of monoidal functors → C and monoidal natural transformations is equivalent to the category of co-cubical objects in C.

In other words, given a monoidal category C, a cubical object in C is "the same" as a monoidal functor op → C. This definition of cubical sets has been known for quite some time, but no concrete application of it has been done up to now. Interestingly, we show here that it can be used to concisely define some cubical sets (see in particular Section 1.5). It is also sometimes useful to define morphisms; for instance, given integers n and i such that 0 i n, and α ∈ {-, +}, we write ∂ α ¬i :

C(n + 1) → C(1) for the morphism ∂ α ¬i = C((ε α ) ⊗i ⊗ id 1 ⊗ (ε α ) ⊗(n-i) )
where (ε α ) ⊗i denotes the tensor product of i copies of ε α .

Similarly, monoidal functors ⊡ → C correspond to co-precubical objects in C, where a precubical object (C, ε -, ε + ) is an object C of C together with two arrows ε -, ε + : C → I (and no axiom to be satisfied), and a co-precubical object is defined dually.

From precubical sets to cubical sets

In this section, we formalize the intuition that morphisms between precubical sets are to morphisms between cubical sets what partial functions are to total functions. Recall that a pointed set (A, a) consists of a set together with a distinguished element a ∈ A, and a morphism f : (A, a) → (B, b) between two pointed sets consists of a function f : A → B such that f (a) = b. If we write Set * for the category of pointed sets, there is a forgetful functor U : Set * → Set which to every pointed set (A, a) associates the underlying set A. This functor admits a left adjoint F : Set → Set * which to every set A associates the free pointed set it generates, that is the pointed set (A ⊎ { * }, * ) where ⊎ denotes the disjoint union (we often use the notation * for the newly added element). We write ? = G • F for the monad on Set induced by this adjunction. It is well-known [START_REF] Maclane | Categories for the Working Mathematician[END_REF] that Proposition 4. The category of sets and partial functions is isomorphic to the Kleisli category Set ? associated to the monad ? on Set. Moreover, this Kleisli category is equivalent to the category Set * .

Proof. A partial function f : A → B induces a morphism g : A → B in Set ? (i.e. a morphism g : A → ? B in Set) defined on every x ∈ A by g(x) = f (x) if f (x) is defined and g(x) = * otherwise, where ? B = B ⊎ { * }. Conversely, any morphism g : A → B in Set ? (i.e. morphism g : A → ? B in Set, with ? B = B ⊎ { * }) induces a partial function f : A → B defined on every x ∈ A such that g(x) = * by f (x) = g(x). These two operations can easily be shown to be inverse of each other, thus exhibiting an isomorphism between the category of sets and partial functions and the Kleisli category Set ? .

By general properties of monads (see [START_REF] Maclane | Categories for the Working Mathematician[END_REF], exercises p. 144), the category Set ? is equivalent to the full subcategory of Set * whose objects are of the form F A for some set A ∈ Set. Moreover, every object (A, a) of Set * is isomorphic to the pointed set F (A \ {a}). The categories Set ? and Set * are thus equivalent.

The proposition above formalizes the fact that a partial function f : A → B can be seen as a total function f : A → B ⊎ { * } where f is "undefined" on an element a ∈ A whenever f (a) = * . The second part of the proposition states that this partial function can also be seen as a pointed function

f : (A ⊎ { * }, * ) → (B ⊎ { * }, * ).
The situation between precubical sets and cubical sets is very similar. There is an obvious inclusion functor ⊡ → , which by precomposition, induces a forgetful functor U : CSet → PCSet on the corresponding presheaf categories. By general theorems (see Section 1.7), this functor admits a left adjoint F : PCSet → CSet. As previously, we write ? = G • F for the induced monad on PCSet and PCSet ? for the Kleisli category associated to the monad. The morphisms in PCSet ? should be thought as "partial morphisms of precubical sets". And actually, this category can be shown to be isomorphic to a category whose objects are precubical sets and morphisms κ : C → D are families (k n : C(n) → D(n)) n∈N of partial functions satisfying suitable properties, which we do not need to detail here.

One of the main interests of expressing the "partial" variants of models as Kleisli constructions is that this enables us to easily lift the adjunctions between models into adjunctions between their partial variants. Namely, This property, which is proved in a more general version in [START_REF] Mulry | Lifting theorems for Kleisli categories[END_REF], thus enables us to lift an adjunction between the categories C and D into an adjunction between the corresponding Kleisli categories C S and D T . In the following, it will be particularly useful to lift adjunction between models into adjunctions between corresponding models with partial morphisms.

Symmetric cubical sets

One sometimes needs more structure on cubical sets in order to formally express the fact that the cells of dimension n 2 in cubical sets arising as models for concurrent processes are essentially not directed. This can be formalized by adjoining a notion of symmetry in cubical sets. The idea here is that given a 2-cell z in a cubical set as shown on the left of

x 3 x 1 y3 a a ③ ③ ③ ③ ③ z x 2 y4 ❉ ❉ ❉ ❉ ❉ x 0 y1 ❉ ❉ ❉ ❉ ❉ y2 a a ③ ③ ③ ③ ③ x 3 x 2 y4 a a ⑤ ⑤ ⑤ ⑤ ⑤ z ′ x 1 y3 ❇ ❇ ❇ ❇ ❇ x 0 y2 ❇ ❇ ❇ ❇ ❇ y1 a a ⑤ ⑤ ⑤ ⑤ ⑤
there should also be a "mirror" cell z ′ as shown on the right, expressing the fact that z is not really directed from y 1 y 3 to y 2 y 4 . The symmetry of the cubical category will associate to each two cell a "mirror" 2-cell in this way (it actually also generalizes this principle to higher dimensions). The need for symmetry is also explained in the case of labeled cubical sets in Example 9.

The symmetric cubical category S is the free symmetric monoidal category containing a co-cubical object. The presheaves on this category are called symmetric cubical sets and they form a category SCSet. The category S can also be described as the free monoidal category containing a symmetric co-cubical object

(C, ε -, ε + , η, γ), which is a co-cubical object (C, ε -, ε + , η) together with a morphism γ : C ⊗ C → C ⊗ C satisfying usual axioms for symmetry (γ ⊗ C) • (C ⊗ γ) • (γ ⊗ C) = (C ⊗ γ) • (γ ⊗ C) • (C ⊗ γ) γ • γ = γ (5)
and

γ • (ε -⊗ C) = C ⊗ ε - γ • (ε + ⊗ C) = C ⊗ ε + (η ⊗ C) • γ = C ⊗ η γ • (C ⊗ ε -) = ε -⊗ C γ • (C ⊗ ε + ) = ε -⊗ C (C ⊗ η) • γ = η ⊗ C
see [START_REF] Grandis | Cubical sets and their site[END_REF] for the details. Alternatively, the notion of symmetric cubical set can be equivalently reformulated as a cubical set C together with, for every integer n, an action of the symmetric group Σ n on C(n) -the action of the transposition being given by C(γ) : C(2) → C(2) -which satisfies the following coherence axioms: for every integers n and i such that 0 i n and every α ∈ {-, +}, -for every (n + 1)-cell x and permutation

σ ∈ Σ n+1 , ∂ α i (σx) = ∂ α σ(i) (x)
-for every n-cell x and permutation

σ ∈ Σ n , ι i (σx) = ι σ(i) (x)
Namely, any symmetry σ : n → n (i.e. a bijection on a set with n elements) can be decomposed as a product of transpositions and can therefore be seen as a morphism in S by sending the transposition σ i : n → n, which exchanges the ith and (i + 1)-th element, to the morphism i ⊗ γ ⊗ (ni -2). The axioms (5) imposed on γ, as well as the axioms of monoidal categories, ensure that this operation is well defined. In the following, we will thus sometimes implicitly consider a bijection as a morphism in the category S . Given a symmetric monoidal category C (such as Set with cartesian product), any cubical object of the underlying monoidal category of C can be canonically equipped with a structure of symmetric cubical set, the morphism γ being given by the symmetry of the category. Given an integer n, we write ( S ) n for the full subcategory of S whose objects are integers k n and SCSet n for the category of presheaves on ( S ) n , whose objects are called n-dimensional symmetric cubical sets. The symmetric precubical category ⊡ S is defined similarly as the free symmetric monoidal category containing a co-precubical object and we write SPCSet for the category of presheaves on ⊡ S , whose objects are called symmetric precubical sets. Notice that many of the usual models for concurrency can be equipped with a similar, and often related, notion of symmetry: for instance event structures [START_REF] Winskel | Event structures with symmetry[END_REF][START_REF] Staton | On the expressivity of symmetry in event structures[END_REF], or Petri nets [START_REF] Hayman | Symmetry in petri nets[END_REF].

Labeled cubical sets

We have explained that the 1-cells of a cubical set can be seen as occurrences of events in the semantics of a concurrent computational process. One sometimes needs to remember to which instruction of the process it corresponds. Labeled (pre)cubical sets formally allows this. The presentation given here is adapted from [START_REF] Goubault | Labelled cubical sets and asynchronous transistion systems: an adjunction[END_REF], see also [START_REF] Gaucher | Combinatorics of labelling in higher-dimensional automata[END_REF].

Suppose that we are given a set L of labels. The category (Set, ×, 1) has finite products and is thus monoidal with the cartesian product as tensor and the terminal set 1 = { * } as unit (for simplicity, we consider that the monoidal structure is strict). The set L can be canonically equipped with a structure of symmetric precubical object (L, ε -, ε + , γ) where ε -, ε + : L → 1 are both the terminal arrow and γ : L × L → L × L is the canonical transposition. According to the preceding remarks, it thus induces a symmetric precubical set noted ! L and called the labeling precubical set on L. Moreover, if L ′ is another set of labels, any function f : L → L ′ induces a morphism between the corresponding co-precubical objects, and therefore induces a morphism ! f : ! L → ! L ′ , extending this operation into a functor. An explicit description of the precubical set ! L can be given as follows: its n-cells l ∈ ! L(n) are lists l = (e i ) 0 i<n , of length n, of labels e i ∈ L. The face maps ∂ - n , ∂ + n : ! L(n + 1) → ! L(n) both send an (n + 1)-cell (e i ) 0 i<n+1 to the list obtained by removing the element at the k-th position and the action of a symmetry σ : n → n on ! L(n) sends a cell (e i ) 0 i<n to (e σ(i) ) 0 i<n .

It can be shown that ! L is the cofree precubical set generated by L in the following sense: Proposition 6. The functor E : SPCSet → Set, which to every precubical set C associates its set C(1)/ ≈ of events (see Section 1.1) and to every morphism κ : C → D associates the function (κ 1 / ≈) : (C(1)/ ≈) → (D(1)/ ≈), admits ! as right adjoint.

Proof. Suppose given a precubical set C and a set L. To every given function f : (C(1)/ ≈) → L, we associate the morphism ψ(f

) : C → ! L defined on an n-cell x as the n-cell (f (∂ - ¬0 (x)), . . . , f (∂ - ¬(n-1) (x))) of ! L, where the function ∂ α ¬i is defined in Section 1.2.
Conversely, to every morphism κ : C → ! L of cubical sets, we associate the function ψ(κ) : (C(1)/ ≈) → L defined as κ 1 / ≈: this is well defined since the events of ! L are (in bijection with) the elements of L.

Finally, is it straightforward to check that the functions ϕ and ψ are natural in C and L, and inverse of each other.

Remark 7. The cofree non-symmetric labeling precubical set on a set L could be defined in the same way, but a direct description is more difficult. It can for example be obtained from the symmetric labeling precubical set ! L on L by quotienting by the action of symmetries.

Recall that given categories C, D and E and functors F : C → E and G : D → E, the slice category F ↓ G (sometimes also called comma category) is the category whose objects are triples (A, f, A ′ ) where A is an object of C, A ′ is an object of D and f : F A → GA ′ is a morphism of E, and whose morphisms

(h, h ′ ) : (A, f, A ′ ) → (B, g, B ′ ) are the pairs of morphisms h : A → B of C and h ′ : A ′ → B ′ of D making the diagram F A f F h G G F B g GA ′ Gh ′ G G GB ′
⑤ ⑤ ⑤ ⑤ ⑤ y 2 a ❇ ❇ ❇ ❇ ❇ x a ❇ ❇ ❇ ❇ b b b ⑤ ⑤ ⑤ ⑤ and z y 1 b b b ⑤ ⑤ ⑤ ⑤ ⑤ α β y 2 a ❇ ❇ ❇ ❇ ❇ x a ❇ ❇ ❇ ❇ b b b ⑤ ⑤ ⑤ ⑤
with in the second case two squares α and β attached in the middle, respectively labeled by (a, b) and (b, a) (and none in the first case): the presence of a square indicates that the two actions a and b commute and more generally n-cubes indicate the commutation of n actions [START_REF] Goubault | The Geometry of Concurrency[END_REF]. Notice that the symmetry intuitively enables us to say that the cell labeled by ab is "the same as" the cell labeled by ba.

In a non-symmetric case, there would be only one cell and there is no canonical choice of naming for this cell (this is however sometimes overcome by supposing that letters are totally ordered, but supposing this is not very natural).

Notice that events provides a canonical labeling of symmetric precubical sets:

Proposition 10. The forgetful functor U : LSPCSet → SPCSet which to every labeled symmetric precubical set associates the underlying symmetric precubical set (forgetting the labels) admits the functor E : SPCSet → LSPCSet as left adjoint, which to every symmetric precubical set C associates the labeled symmetric precubical set (C, ℓ, ! L) where L = C(1)/ ≈ is the set of events of C and ℓ is the morphism induced by the function ℓ : C(1) → L which to every 1-cell associates its equivalence class under ≈.

This means in particular that all following results about labeled symmetric precubical sets simply extend to the unlabeled case by considering precubical sets labeled by their events. We thus only handle labeled cases in the following, since unlabeled structures are a particular instance. The category of labeled symmetric cubical sets is defined in a similar way. A given pointed set (L, * ) induces a symmetric cubical object (L, ε -, ε + , η, γ) where ε -, ε + : L → 1 are both the terminal arrow, η : 1 → L associates * to the unique element of 1 and γ : L × L → L × L is the canonical transposition function. As previously, this induces a symmetric cubical set, that we still write !(L, * ), and can be shown to be cofree in the sense that Proposition 11. The functor E : SCSet → Set * , which to every cubical set C associates the pointed set obtained from C(1)/ ≈ by identifying all equivalence classes containing an element of the image of ι 0 to a single element * chosen as distinguished element and to every morphism κ : C → D associates the morphism induced by κ 1 : C(1) → D(1), admits ! as right adjoint.

Definition 12. The category of symmetric labeled cubical sets, denoted by LSCSet, is the slice category SCSet ↓ !, which is isomorphic to E ↓ !.

An explicit description of !(L, * ) is similar to the one of the labeling symmetric precubical set: its n-cells are lists l = (e i ) 0 i<n , with the same face and symmetry maps as previously. The degeneracy maps ι i : !(L, * )(n) → !(L, * )(n + 1) associate to every list l of length n the list of length n + 1 obtained from l by inserting * at the i-th position.

We have defined labellings in the most natural way. There is however a slight mismatch between labeled precubical and cubical sets: in the first case functions between labels are total whereas they are partial in the second case. This mismatch actually turns out to bring annoying details, as explained in Section 1.7 (see also [START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF]). The opposite choices can be made in both cases as follows. A slightly more general notion of labeled precubical set can be defined, by allowing partial functions between morphisms. If we write U : Set * → Set for the canonical forgetful functor, the category of weakly labeled symmetric precubical sets wLSPCSet is defined as wLSPCSet = SPCSet ↓ ! U . Conversely, one can restrict labeled cubical sets by only allowing total functions between labels and imposing that only degenerate events are labeled by the distinguished element of the labeling pointed set thus defining a category of totally labeled symmetric cubical sets (we do not detail this construction here).

Finally, we introduce the notion of strongly labeled cubical set, which will turn out in Section 3 to be the "right" notion of labeled cubical set in order to relate them with most of the usual models of concurrency. Definition 13. A labeled cubical set (C, ℓ) is strongly labeled when there exists no pair of distinct k-cells, for some dimension k, whose sources and targets are equal, which have the same label: for every index k > 0, and every elements x, y ∈ C(k) such that for every index 0

i < k ∂ i (x) = ∂ i (y), if ℓ(x) = ℓ(y) then x = y.
This condition can be seen as a labeled and higher dimensional analogue of Winskel's "no ravioli" condition for HDA [START_REF] Winskel | Event structures with symmetry[END_REF], which imposes that two parallel 1-cells should be equal, and corresponds to being separated wrt a Grothendieck topology.

Higher dimensional automata

A pointed cubical set (C, i) is a cubical set together with a distinguished 0-cell i ∈ C(0). The notion of higher dimensional automaton can be seen as a generalization of the classical notion of automaton to higher dimensional transition systems: Definition 14. A higher dimensional automaton (or HDA) is a pointed labeled symmetric cubical set C, the distinguished element i being called the initial state. A morphism of HDA is a morphism between the underlying labeled symmetric cubical sets which preserves the initial state.

Given a category C of cubical sets, we often write C * for the corresponding category of pointed cubical sets. We write HDA = LSCSet * for the category of HDA and sHDA = LSPCSet * for the category of strict HDA. We also write HDA n = LSCSet * n for the subcategories for truncated HDA.

A path p : x -→ → x ′ in an HDA C is a finite sequence (y i ) 0 i<n of 1-cells of C such that ∂ + 0 (y i ) = ∂ - 0 (y i+1 ), ∂ - 0 (y 0 ) = x and ∂ + 0 (y n ) = x ′ .
We write s•t for the concatenation of two paths s and t. A 0-cell x of an HDA is reachable when there exists a path s : i -→ → x, where i is the initial state of the HDA. Since higher dimensional cells express the fact that transitions are independent, two paths differing only by a reordering of independent transitions should be considered as equivalent from the concurrency point of view. This is formally expressed by the homotopy relation between paths [START_REF] Fajstrup | Dipaths and dihomotopies in a cubical complex[END_REF][START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF], which is defined as the smallest equivalence relation relating two paths s • m • n • t and s • p • q • t where m, n, p and q are 1-cells such that there exists a 2-cell z for which

m = ∂ - 0 (z), q = ∂ + 0 (z), p = ∂ - 1 (z) and n = ∂ + 1 (z) ; graphically, t y y y y n c c ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ z q ❄ ❄ ❄ ❄ ❄ ❄ ❄ ❄ m ❄ ❄ ❄ ❄ ❄ ❄ ❄ ❄ p c c ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ s y y y y
In particular, in the situation above, m and q (resp. p and n) are part of the same event. Given two paths s and t, we write s ∼ t when they are homotopic. Two homotopic paths are necessarily parallel (they have the same source and target). 1. The functor Î : D → Ĉ admits both a left and a right adjoint and we write T for the monad induced on Ĉ.

2. The Kleisli category D T associated to the monad T embeds fully and faithfully into D.

3. When I is bijective on objects, the adjunction is monadic which means that the category D is equivalent to the category C T of algebras for the monad T on Ĉ.

Proof. (i) and (ii) are standards properties [START_REF] Lane | Sheaves in geometry and logic: A first introduction to topos theory[END_REF]. In particular, the free presheaf in D on a presheaf C ∈ Ĉ can be computed as the left Kan extension of C along I (and similarly for the right adjoint).

(iii) This fact does not seem to be very well-known and can be found for example p. 105 of [START_REF] Borceux | Galois theories[END_REF]. We have seen that the functor Î admits a left adjoint. Since it is the bijective on objects it is conservative (it reflects isomorphisms): an isomorphism between presheaves is simply a natural transformation between them whose components are all invertible. Moreover, presheaf categories are cocomplete; in particular, they have all equalizers, these are computed pointwise and they are thus preserved by precomposition with U . We can conclude by using Beck's monadicity theorem [START_REF] Maclane | Categories for the Working Mathematician[END_REF].

Notice that this generalizes in particular the situation described in Section 1.3.

This property is very interesting because, it means that all the forgetful functors between variants of categories of cubical sets admit both left and right adjoint:

-functors forgetting structure:

SCSet → CSet, CSet → PCSet, PCSet → Set, etc. SCSet n → CSet n , CSet n → PCSet n , PCSet n → Set, etc.
-truncation functors:

SCSet → SCSet n , CSet → CSet n , etc.
These adjoints will allow us to compute for example the free cubical set on a precubical set and so on, and will be used in the following. As an illustration, consider the functor PCSet → PCSet n . Given an n-dimensional precubical set C, the left adjoint sends C to the precubical set D whose k-cells are D(k) = C(k) for k n and D(k) = ∅ otherwise. The action of the right adjoint is more subtle: it sends C to the precubical set obtained from C by "filling in" all the k-dimensional cubes, with k > n, by a k-cell.

The analogy between the adjunction between sets and pointed sets and the adjunction between precubical sets and sets, can be related with the construction of labeling cubical sets as follows.

Lemma 16. The diagram

Set F E E I ⊤ SPCSet E k k J Set * H E E ⊥ SCSet G k k commutes, in the sense that J • F = H • I and G • J = I • E
, where E (resp. H) is the functor which to every symmetric precubical (resp. cubical set) associates its set (resp. pointed set) of events described along with their right adjoints in Section 1.5, and I (resp. J) is the left adjoint to the forgetful functor Set * → Set (resp. SCSet → PCSet).

It could be hoped that previous Lemma would provide the starting point of a lifting of the adjunctions between SPCSet and SCSet to adjunctions between LSPCSet and LSCSet. However this is not the case: morphisms between labels have to be total or partial in both the categories. It is however easy to show that Proposition 17. The forgetful functor LSCSet → wLSPCSet admits both a left and a right adjoint (and other adjunctions mentioned above can be lifted to the labeled case in a similar way). Similar adjunctions also exist between the variants where functions between labels are total.

The choice of partial or total functions between labels in the category of labeled symmetric (pre)cubical sets is thus difficult to handle in a modular way. The choice has to be made once for all and in the following, we deliberately do not explicit which one is made since all the constructions given here work in both cases.

2 Traditional models for concurrency

Transition systems

Transition systems are one of the oldest semantic models, both for sequential and concurrent systems, in which computations are modeled as the sequence of interactions that they can have with their environment. There is a convenient categorical treatment of this model, that we use in the sequel, taken from [START_REF] Winskel | Models for concurrency[END_REF].

Definition 18. A transition system is a quadruple (S, i, E, T ran) where -S is a set of states with initial state i, -E is a set of events, -T ran ⊆ S × E × S is the transition relation.

In other words, a transition system is a graph together with a distinguished vertex. Transition systems are made into a category by defining morphisms to be some kind of simulation (for then being able to discuss about properties modulo weak or strong bisimulation, see [START_REF] Joyal | Bisimulation and open maps[END_REF]). The idea is that a transition system T 1 simulates a transition system T 0 if as soon as T 0 can fire some action a in some context, T 1 can fire a as well in some related context. A morphism f : T 0 → T 1 defines the way states and transitions of T 0 are related to states and transitions of T 1 making transition systems into a category TS.

Definition 19. Let T 0 = (S 0 , i 0 , E 0 , T ran 0 ) and T 1 = (S 1 , i 1 , E 1 , T ran 1 ) be two transition systems. A partial morphism f :

T 0 → T 1 is a pair f = (σ, τ )
where σ : S 0 → S 1 is a function and τ :

E 0 → E 1 is a partial function such that -σ(i 0 ) = i 1 , - (s
, e, s ′ ) ∈ T ran 0 and τ (e) is defined implies (σ(s), τ (e), σ(s ′ )) ∈ T ran 1 .

Otherwise, if τ (e) is undefined then σ(s) = σ(s ′ ).

As in [START_REF] Winskel | Models for concurrency[END_REF], we can restrict to strict morphisms, i.e. the ones for which τ is a total function, by suitably completing transition systems. Partial morphisms can then be recovered by adding "idle" transitions to the systems, similarly to the construction of the category of sets and partial functions as the Kleisli category associated to the free pointed set monad ? on Set given in Section 1.3.

An idle transition is a transition * which goes from a state s to the same state s. Consider the following completion T * = (S * , i * , E * , T ran * ) of a transition system T = (S, i, E, T ran), by setting S * = S, i * = i, E * = E ⊎ { * } and T ran * = T ran ⊎ {(s, * , s) | s ∈ S}. Now, by the preceding remarks a total morphism (σ, τ ) from (T 0 ) * to (T 1 ) * such that τ ( * ) = * is the same as a partial morphism from T 0 to T 1 . Again, the operation (-) * induces a monad on the category sTS of transition systems and strict morphisms, and the category TS can be recovered as the Kleisli category associated to this monad. Likewise, all the models for concurrency considered in this article admit a "strict" variant, from which the "non-strict" model can be reconstructed by a Kleisli construction. For lack of space we will not detail all the variants here.

⑤ ⑤ ⑤ ⑤ ⑤ y 2 b ❇ ❇ ❇ ❇ ❇ y b ❆ ❆ ❆ ❆ c b b ⑥ ⑥ ⑥ ⑥ x a y y z y 1 c b b ⑤ ⑤ ⑤ ⑤ ⑤ y 2 b ❇ ❇ ❇ ❇ ❇ y b ❆ ❆ ❆ ❆ c b b ⑥ ⑥ ⑥ ⑥ x a y y

Asynchronous automata

Asynchronous automata are a nice generalization of both transition systems and Mazurkiewicz traces, and have influenced a lot of other models for concurrency, such as transition systems with independence (or asynchronous transition systems). They have been independently introduced in [START_REF] Shields | Concurrent machines[END_REF] and [START_REF] Bednarczyk | Categories of asynchronous systems[END_REF]. The idea is to decorate transition systems with an independence relation between actions that will allow us to distinguish between true-concurrency and mutual exclusion (or non-determinism) of two actions. For example, the two last transition systems of Example 20 do not allow us to distinguish between processes which are arguably different from the concurrency point of view. We actually use a slight modification for our purposes, due to [START_REF] Droste | Petri nets and automata with concurrency relations-an adjunction[END_REF], called automaton with concurrency relations:

Definition 21. An automaton with concurrency relations (S, i, E, T ran, I) is a quintuple where -(S, i, E, T ran) is a transition system, -T ran is such that whenever (s, a, s ′ ), (s, a, s ′′ ) ∈ T ran, then s = s ′′ , -I = (I s ) s∈S is a family of irreflexive, symmetric binary relations I s on E such that whenever we have a 1 I s a 2 (with a 1 , a 2 ∈ E), there exist transitions (s, a 1 , s 1 ), (s, a 2 , s 2 ), (s 1 , a 2 , r) and (s 2 , a 1 , r) in T ran.

A morphism of automata with concurrency relations consists of a morphism (σ, τ ) between the underlying transition systems such that a I s b implies that τ (a) I ′ σ(s) τ (b) whenever τ (a) and τ (b) are both defined. This makes automata with concurrency relations into a category, written ACR. We also write sACR for the variant of this category where morphisms are strict morphisms. Again, the category sACR can be constructed from ACR by a Kleisli construction, using * -transitions and total morphisms (the condition on the independence relation is then that a I c) and is empty for the second process.

Event structures

Event structures were introduced in [START_REF] Nielsen | Petri nets, event structures and domains[END_REF][START_REF] Winskel | Event structures[END_REF] in order to abstract away from the precise places and times at which events occur in distributed systems. The idea is to focus on the notion of event and the causal ordering between them. We recall below the definition of (unlabeled prime) event structures.

Definition 23. An event structure (E, , #) consists of a poset (E, ) of events, the partial order relation expressing causal dependency, together with a symmetric irreflexive relation # called incompatibility satisfying -finite causes: for every event e, the set { e ′ | e ′ e } is finite, -hereditary incompatibility: for every events e, e ′ and e ′′ , e # e ′ and e ′ e ′′ implies e # e ′′ .

We write ES for the category of event structures, a morphism between two event structures (E, , #) and (E ′ , ′ , # ′ ) consisting of a partial function f :

E → E ′ which is such that -if f (e) is defined then { e ′ | e ′ f (e) } ⊆ f ({ e ′′ | e ′′ e }),
-and if f (e 0 ) and f (e 1 ) are both defined and we have either f (e 0 ) # ′ f (e 1 ) or f (e 0 ) = f (e 1 ) then either e 0 # e 1 or e 0 = e 1 .

A labeled event structure consists of an event structure (E, , #) together with a set L of labels and a labeling function ℓ : E → L which to every event associates a label. A morphism (f, λ) : (E, , #, ℓ, L) → (E ′ , ′ , # ′ , ℓ ′ , L ′ ) of labeled event structure consists of a morphism f : (E, , #) → (E ′ , ′ , # ′ ) between the underlying event structures and a partial function λ : L → L ′ between the sets of labels such that ℓ ′ • f = λ • ℓ. We write LES for the category of labeled event structures. We also write sES (resp. sLES) for the category of strict (labeled) event structures, defined as the subcategory of ES (resp. LES) whose morphisms are total functions -these categories can also be obtained by suitable Kleisli constructions.

Example 24. The CCS processes a•(b+c), a•(b|c) and a•(b•c+c•b) respectively induce the following labeled event structures (to be read from bottom up, the continuous lines representing the partial order and the dotted ones expressing incompatibilities):

b c a ❃ ❃ ❃ ❃ ❃ b c a ❃ ❃ ❃ ❃ ❃ c b b c a ❃ ❃ ❃ ❃ ❃
Notice that in the last one, b and c appear twice: this is because we have figured the labels and not the events (and two distinct events can of course have the same label).

Petri nets

Petri nets are a well-known model of parallel computation, generalizing transition systems by using a built-in notion of resource. This allows for deriving a notion of independence of events, which is much more general than the independence relation of asynchronous transition systems. They are numerous variants of Petri nets since they were introduced in [START_REF] Petri | Communication with automata[END_REF], and we choose the definition used by Winskel and Nielsen in [START_REF] Winskel | Models for concurrency[END_REF], since this is well-suited for formal comparisons with other models for concurrency: Definition 25. A Petri net N is a tuple (P, M 0 , E, pre, post) where -P is a set of places, -M 0 ∈ N P is the initial marking, -E is a set of events, -pre : E → N P and post : E → N P are the precondition and postcondition functions.

When there is no ambiguity, given an event e of a Petri net N , we often write • e for pre(e) and e • for post(e). A marking M is a function in N P , which associates to every place the number of resources (or tokens) that it contains. The sum M 1 +M 2 of two markings M 1 and M 2 is their pointwise sum. An event e induces a transition between two markings M 1 and M 2 , that we write M 1 e -→ M 2 , whenever there exists a marking M such that

M 1 = M + • e and M 2 = M + e • .
A morphism of Petri nets (ϕ, ψ) : N → N ′ , between the two Petri nets N = (P, M 0 , E, pre, post) and N ′ = (P ′ , M ′ 0 , E ′ , pre ′ , post ′ ), consists of a function ϕ : P ′ → P and a partial function ψ : E → E ′ such that for every place p ∈ P ′ and event e ∈ E, M ′ 0 = M 0 • ϕ, • ψ(e) = • e • ϕ and ψ(e) • = e • • ϕ. We write PNet for the category of Petri nets and sPNet for the subcategory whose morphisms have total functions on events. Notice that the partial function ϕ : P ′ → P on places goes "backwards". This might seem a bit awkward at first sight and we explain why this is the "right" notion of morphism in Remark 37.

A labeled Petri net is a Petri net together with a set L of labels and a function ℓ : E → L labeling events. The notion of morphism of Petri nets can be extended in a straightforward way to labeled ones and we write LPNet for the category of labeled Petri nets and sLPNet for the subcategory whose morphisms are total functions. Now, recall that the category TS can be defined as the Kleisli category associated to the monad (-) * on sTS. Similarly, the adjunction between sHDA 1 and HDA 1 given in Proposition 15 induces a monad ? on sHDA 1 which "replaces" the underlying precubical set of an HDA by the cubical set it generates.

Theorem 28. The adjunction of Theorem [START_REF] Mulry | Lifting theorems for Kleisli categories[END_REF] lifts to an adjunction between TS and HDA 1 , which induces an equivalence if we restrict HDA 1 to strongly labeled cubical sets.

Proof. Consider a strict 1-dimensional HDA consisting of a precubical set C labeled by ℓ into L. Its image under the left adjoint F : sHDA 1 → HDA 1 to the forgetful functor HDA 1 → sHDA 1 is the 1-dimensional HDA whose underlying cubical set is D defined by

D(0) = C(0), D(1) = C(1) ⊎ C(0) with face maps being ∂ α i ⊎ id C(0) : D(1) → D(0)
as face maps and the canonical injection ι 0 : D(0) → D(1) as degeneracy maps, whose labeling is obtained by extending

ℓ 1 : C(1) → (! L) 1 to D(1) by ℓ 1 (x) = ( * ) for x ∈ C(0) ⊆ C(1).
From this concrete description, it can easily be checked that ? •G = G • (-) * and that the unit and the multiplication of (-) * are sent by G to the unit and multiplication of T . Finally, we deduce that the adjunction of Theorem 27 lifts to an adjunction between the Kleisli categories TS and HDA 1 respectively associated to the monads (-) * and ? using Proposition 5.

Remark 29. The fact that we have to restrict to a subcategory of sHDA 1 in Theorem 27 in order to obtain an equivalence of categories can be explained intuitively by remarking that in transition systems there is no distinction between events and labels: in particular, a transition system cannot contain two distinct transitions with the same event between the same source and the same target. For example, the following labeled (pre)cubical set cannot be represented in transition systems: y x a a s s More generally, in higher dimensions most models do not have the possibility to "count" the number of commutations between events: usually, two transitions either commute or not. This contrasts with cubical sets where a tile

x 3 x 1 y3 a a ③ ③ ③ ③ ③ x 2 y4 ❉ ❉ ❉ ❉ ❉ x 0 y1 ❉ ❉ ❉ ❉ ❉ y2 a a ③ ③ ③ ③ ③
can be filled with many 2-cells. This explains why in the following most of the nice adjunctions will be obtained by restricting cubical sets to strongly labeled ones.

By Proposition 15, the truncation functor HDA → HDA 1 admits a right adjoint. By composing this adjunction with the one of previous theorem, we obtain an adjunction between TS and HDA.

Remark 30. The HDA associated by the right adjoint to a transition system T = (S, i, E, T ran) can be described in a more direct way using Proposition 35 as generated by the cubical transition system (S, i, E, ℓ, E ⊎ { * }, t) where ℓ : E → E ⊎ { * } is the canonical injection and t(x, l) = y if l is reduced to an event e and (x, e, y) ∈ T ran, see Section 3.4 for details.

Asynchronous automata and HDA

The adjunction given in previous section, can be extended to an adjunction between the category of strict asynchronous automata sACR and the category of strict 2-dimensional HDA sHDA 2 .

To any strict 2-dimensional HDA C, the left adjoint F : sHDA 2 → sACR associates the asynchronous automaton whose underlying transition system is induced by the underlying 1-dimensional HDA of C and such that a 1 I s a 2 when there exists transitions (s, a 1 , s 1 ), (s, a 2 , s 2 ), (s 1 , a 2 , r) and (s 2 , a 1 , r) and a 2cell y such that

∂ - 0 (y) = (s, a 1 , s 1 ), ∂ + 0 (y) = (s 2 , a 1 , r), ∂ - 1 (y) = (s, a 2 , s 2 ) and ∂ + 1 (y) = (s 1 , a 2 , r): r s 1 a2 b b ⑥ ⑥ ⑥ ⑥ ⑥ y s 2 a1 ❆ ❆ ❆ ❆ ❆ s a1 ❆ ❆ ❆ ❆ a2 b b ⑥ ⑥ ⑥ ⑥ (6)
The functor is defined in the obvious way on morphisms.

Conversely, an asynchronous automaton A = (S, i, E, T ran, I) is sent by the right adjoint G : sACR → sHDA 2 to a strict 2-dimensional HDA C, whose underlying 1-dimensional HDA is induced by the underlying transition system of A. The 2-cells are C(2) = I, where I is seen as a subset of E × S × E. Given a pair of events a 1 and a 2 related by I s for some state s, there exist transitions (s, a 1 , s 1 ), (s, a 2 , s 2 ), (s 1 , a 2 , r) and (s 2 , a 1 , r) and these are uniquely defined by the second property of Definition 21 as in [START_REF] Droste | Petri nets and automata with concurrency relations-an adjunction[END_REF], face maps are defined on elements y = a 1 , s, a 2 of I by

∂ - 0 (y) = (s, a 1 , s 1 ) ∂ + 0 (y) = (s 2 , a 1 , r) ∂ - 1 (y) = (s, a 2 , s 2 ) ∂ + 1 (y) = (s 1 , a 2 , r)
and the labeling function is defined by ℓ(a 1 , s, a 2 ) = (a 1 , a 2 ). The requirement that I is symmetric induces the symmetry of the HDA. The functor is defined in the obvious way on morphisms.

Theorem 31. These functors form an adjunction between sACR and sHDA 2 .

The induced comonad on sACR is the identity and the adjunction induces an equivalence of categories if we restrict sHDA 2 to the full subcategory of strongly labeled HDA. Moreover, this adjunction lifts to an adjunction between ACR and HDA 2 with similar properties.

By composing with an adjunction given by Proposition 15, this induces an adjunction between ACR and HDA.

Event structures and HDA

We construct here an adjunction between sLES and sHDA. This adjunction reformulates in the framework of HDA some well-known relations between event structures and transition systems with independence [START_REF] Sassone | Relationships between models of concurrency[END_REF]. The study of relations between the two models was initiated in [START_REF] Cattani | Higher dimensional transition systems[END_REF] and a similar connection is described in [START_REF] Staton | On the expressivity of symmetry in event structures[END_REF].

A configuration of an event structure (E, , #) is a finite downward closed subset of compatible events in E. An event e is enabled at a configuration x if e ∈ x and x ⊎ {e} is a configuration. A functor F : sLES → sHDA 2 can be defined as follows. To any labeled event structure (E, , #, ℓ, L), it associates the 2-dimensional HDA C labeled by L whose 0-cells are the configurations of the event structure with the empty configuration as initial state, 1-cells are the pairs (x, e) where x is a configuration and e is an event enabled at x, and 2-cells are the pairs (x, e 1 , e 2 ) where x is a configuration and e 1 , e 2 are both enabled at x and such that e 2 is enabled at x ⊎ {e 1 } and e 1 is enabled at x ⊎ {e 2 }, graphically:

x ⊎ {e 1 , e 2 }

x ⊎ {e 1 } (x⊎{e1},e2)

V V q q q q q q q q q q q (x, e 1 , e 2 )

x ⊎ {e 2 } (x⊎{e2},e1)

f f ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ ▼ x (x,e1) g g ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ ❖ (x,e2) U U ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦ ♦
Notice for every 2-cell (x, e 1 , e 2 ), (x, e 2 , e 1 ) is also a 2-cell thus inducing a symmetry on the precubical set. The functor is defined in the obvious way on morphisms. Conversely, we define a functor G : sHDA 2 → sLES. The intuition is that given an HDA C, the elements of G(C) should be the events of C in the sense of Section 1.1. However, event structures cannot express loops, which should therefore be unfolded [START_REF] Winskel | Models for concurrency[END_REF][START_REF] Van Glabbeek | On the expressiveness of higher dimensional automata[END_REF][START_REF] Fahrenberg | Higher-Dimensional Automata from a Topological Viewpoint[END_REF]. For example, an HDA of the form

x a Ô Ô (7)
with only one 0-cell and one looping 1-cell should have as image an event structure with a countable totally ordered set of events. A 2-dimensional HDA is unfolded when it is -reachable: every 0-cell x is reachable, -acyclic: any path s : x -→ → x with the same source and target is empty, -unshared : any two parallel paths s, t : x -→ → x ′ are homotopic.

This reformulates the notion of occurrence transition system with independence.

To

∂ + i (s, z) = (s • ∂ - 1-i (z), ∂ + i (z)
), -the labeling function labels a 1-cell (s, m) by ℓ(m) and a 2-cell (s, z) by ℓ(z).

This operation can easily be extended into a comonad on the category sHDA 2 . For example, the image of the HDA ( 7) is

x 0 a G G x 1 a G G x 2 a G G . . .
Now, to every unfolded 2-dimensional HDA C, one can associate a labeled event structure V (C) = (E, , #, ℓ, L) such that E is the set of events of C in the sense of Section 1.1. We say that an event e occurs in a path s when s contains a 1-cell m such that m ∈ e. Two events e and e ′ are such that e e ′ when for every path s • n : i -→ → x with n ∈ e ′ the event e occurs in s. Two events e and e ′ are such that e#e ′ when there is no path s : i -→ → x such that both e and e ′ occur in s. The labeling function is the labeling function of C (recall that we have shown in Section 1.5 that every labeled cubical set induces a labeling function on its events). The operation V is easily extended as a functor V from the category of unfolded 2-dimensional HDA to the category of labeled event structures. Finally, we define the functor G : sHDA 2 → sLES as the composite G = V • U .

Theorem 33. The composite functor G•F is isomorphic to the identity functor on sLES. Thus sLES embeds fully and faithfully into sHDA 2 .

Proof. The adjunction between labeled event structure and transition systems with independence described [START_REF] Sassone | Relationships between models of concurrency[END_REF][START_REF] Mimram | Sémantique des jeux asynchrones et réécriture 2-dimensionnelle[END_REF] can be straightforwardly adapted to asynchronous transition systems and one obtains the result by composing with the adjunction described in previous section.

Notice that we did not claim that F and G are part of an adjunction, because it is not the case. Namely, consider the effect of the endofunctor F • G : sHDA 2 → sHDA 2 : we have pictured some HDA (on the left) together with their image under F • G (on the right):

x 2 x 1 c y y x 0 a r r b x 3 x 4 x 1 c y y x 2 c y y x 0 a ❉ ❉ ❉ ❉ ❉ b a a ③ ③ ③ ③ ③ x a Ô Ô x 0 a G G x 1 a G G x 2 a G G . . . y x a y y x ′ b ❄ ❄ ❄ ❄ ❄ ❄ ❄ y x a y y y 1 b G G y x 3 a ❈ ❈ ❈ ❈ ❈ b G G y 2 a ❆ ❆ ❆ ❆ ❆ x 1 c y y x a ❉ ❉ ❉ ❉ ❉ c y y b G G x 2 c y y y 1 b G G y x 3 a ❈ ❈ ❈ ❈ ❈ G G y 2 a ❈ ❈ ❈ ❈ ❈ x 1 c y y G G y 3 y y x a ❉ ❉ ❉ ❉ ❉ y y b G G x 2 ❈ ❈ ❈ ❈ ❈ c y y x 3 x 1 b T T b p p x 2 a ❈ ❈ ❈ ❈ ❈ ❈ ❈ ❈ x 0 a ❈ ❈ ❈ ❈ ❈ ❈ ❈ ❈ b a a ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ x 3 x 1 b a a ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ x 2 a ❈ ❈ ❈ ❈ ❈ ❈ ❈ ❈ x 0 a ❈ ❈ ❈ ❈ ❈ ❈ ❈ ❈ b a a ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤
In the third example, x is the initial position and in the last two examples all the squares for which it makes sense are filled with 2-cells. These examples are representative of various kinds of behaviors that can happen:

-the first two examples show that "shared transitions" are "unshared", and in particular loops are unrolled;

-the third example shows that the unreachable 0-cells of the HDA are removed,

-the fourth example shows that if the HDA contains half of a cube then the other half of the cube is created, completing the cube -this is related to the cube axiom which is often used to characterize asynchronous transition systems generated by an event structure [START_REF] Sassone | Relationships between models of concurrency[END_REF];

-the last example shows that HDA are made strongly labeled.

Notice, if we write C for the HDA in the left of examples, in the first three examples there is a natural arrow T C → C (but not in the other direction), whereas in the last two examples there is a natural arrow C → T C (but not in the other direction). So there is no hope that T would be either a monad or a comonad, and thus that F and G either form an adjunction in either direction. It can however be shown that G is right adjoint to F if we restrict sHDA 2 to the full subcategory whose objects are strongly labeled and satisfy the cube axioms (which state that if an asynchronous transition system contains half of a cube as in fourth example then it also contains the other half of the cube, as well as two other variants of this property). As previously, this adjunction can be extended to the non-strict variants of the models, as well as the whole category HDA. This adjunction can also be extended to an adjunction between general event structures (in which conflict is not necessarily a binary relation) and HDA.

Petri nets and HDA

This section constitutes perhaps the most novel part of the paper. We extend here previously constructed adjunctions between 1-bounded Petri Nets and asynchronous transition systems [START_REF] Winskel | Models for concurrency[END_REF][START_REF] Droste | Petri nets and automata with concurrency relations-an adjunction[END_REF][START_REF] Mukund | Petri nets and step transition systems[END_REF][START_REF] Van Glabbeek | Petri nets, configuration structures and higher dimensional automata[END_REF] to an adjunction between general Petri Nets and HDA. For similar reasons as previously, one needs to restrict to strongly labeled HDA in order to obtain a well-defined adjunction. We thus implicitly only consider strongly labeled HDA in the following.

Cubical transition systems. We introduce here a general methodology for associating a symmetric precubical set to a model for concurrent processes, that we will use in order to associate a strict HDA to a Petri net. Since monoidal functors preserve the unit of monoidal categories, all cubical sets generated by cubical objects in Set (i.e. by the functor ! introduced in Section 1.5) contain only one 0-cell. Cubical sets with multiple 0-cells can be generated by actions of the labeling cubical set on the 0-cells, formalized as follows, in the same way that a transition system can be seen as an action of the free monoid on labels over the states. The resulting notion of cubical transition system (or CTS ) generalizes to the setting of cubical set the notion of step transition system [START_REF] Mukund | Petri nets and step transition systems[END_REF] which is a variant of transition systems in which multiple events can occur simultaneously. Definition 34. A cubical transition system (S, i, E, t, ℓ, L) consists of -a set S of states, -a state i ∈ S called the initial state, -a set E of events, -a transition function which is a partial function t : S × ! E → S, -a set L of labels, -a labeling function ℓ : E → L, such that for every state x and every n-cell l of ! E for which t(x, l) is defined, 1. if l = l 1 • l 2 for some cells l 1 and l 2 then t(x, l 1 ) and t(t(x, l 1 ), l 2 ) are both defined and we have t(x, l) = t(t(x, l 1 ), l 2 ), 2. t(x, ()) is defined and equal to x (where () denotes the 0-cell of ! E),

3. for every symmetry σ : n → n, t(x, ! E(σ)(l)) is defined and equal to t(x, l).

Cubical transition systems are thus generalized transition systems, which modify state upon incoming events. These differ from traditional transition systems in that they may accept a transition under n events e 1 , . . . , e n , specified by a transition under the word e 1 • • • e n ∈ ! E. With this understanding in mind, the axioms have simple interpretations: for example the first one states that the state reached under two simultaneous events e 1 and e 2 is the same as the state reached under e 1 followed by e 2 .

An n-cell l of ! E is enabled at a position x if t(x, l) is defined. Every such CTS defines a strict HDA C labeled by L whose n-cells are pairs (x, l) where x is a state and l is an n-cell of ! E which is enabled at x. Source and target functions are defined by ∂

- i (x, l) = (x, ∂ - i (l)) and ∂ + i (x, l) = t(t(x, e i ), ∂ + i (l)
) where e i is the i-th element of l and symmetries by σ(x, l) = (x, ! E(σ)(l)). The labeling function is ! ℓ and the initial state is i.

A morphism (σ, τ, λ) : (S 1 , i 1 , E 1 , ℓ 1 , L 1 , t 1 ) → (S 2 , i 2 , E 2 , ℓ 2 , L 2 , t 2 ) between two CTS consists of -a function σ : S 1 → S 2 , -a function τ : E 1 → E 2 , -a function λ : L 1 → L 2 , such that i 2 = σ(i 1 ), ℓ 2 • τ = λ • ℓ 1 ,
and for every state x ∈ S 1 and cell l of ! E 1 , t 2 (σ(x), ! τ (l)) = σ • t 1 (x, l). Every such morphism induces a morphism (κ, λ) : C 1 → C 2 between the corresponding HDA C 1 and C 2 defined on n-cells (x, l) of C 1 by κ n (x, l) = (σ(x), ! τ (l)). We write CTS for the category thus defined.

Proposition 35. The functor CTS → sHDA defined above is well-defined. Remark 36. A variant of the notion of cubical transition system can easily be defined in order to generate symmetric cubical sets.

From Petri nets to HDA. Suppose that we are given a labeled Petri net N = (P, M 0 , E, pre, post, ℓ, L). The pre and post operations can be extended to the cells of ! E by

• () = • ( * ) = 0, • (l 1 • l 2 ) = • l 1 + • l 2 , () • = ( * ) • = 0 and (l 1 •l 2 ) • = l • 1 +l • 2 .
This enables us to see elements of ! E as generalized events. We also generalize the notion of transition and given two markings M 1 and M 2 and an event l ∈ ! E, we say that there is a transition M 1 l -→ M 2 whenever there exists a marking M such that M 1 = M + • l and M 2 = M + l • . In this case, the event l is said to be enabled at the marking M 1 . The marking M 2 is sometimes denoted M 1 /l. A marking M is reachable if there exists a transition l such that M = M 0 /l where M 0 is the initial marking of N .

Remark 37. As in [START_REF] Winskel | Models for concurrency[END_REF], we have chosen to define morphisms in the opposite direction on places. With the adjunction with HDA in mind, this can be explained as follows. Morphisms of Petri nets should, just as morphisms of HDA, preserve independence of events: if two events e and e ′ of a net N are independent and (ϕ, ψ) : N → N ′ is a morphism of nets, then their images ψ(e) and ψ(e ′ ) should also be independent. By contraposition, this means that if both events ψ(e) and ψ(e ′ ) depend on a common place p, then the events e and e ′ should depend on a corresponding common place ψ -1 (p).

Every labeled Petri net N induces a CTS (S, i, E, t, ℓ, L) whose states S are the reachable markings of the net, with the initial marking M 0 as initial state, events E are the events of the net, transition function t(M, l) is defined if and only if l is enabled at M and in this case t(M, l) = M/l, with the set L as set of labels and ℓ : E → L as labeling function.

It is routine to verify that this actually defines a CTS and thus a strict HDA. The n-cells of hda(N ) consisting of a marking M of the net and a list l of events which is enabled at M . Moreover, any morphism (ϕ, ψ) : N → N ′ between labeled Petri nets induces a morphism (σ, τ, λ) between the corresponding CTS defined by σ(M ) = M • ϕ for any reachable marking M of N , τ = ψ, and λ = ψ. We denote by hda : sLPNet → sHDA the functor thus defined.

From HDA to Petri nets. We first introduce the notion of region of an HDA, which should be thought as a way of associating a number of tokens to each 0-cell of the HDA and a pre-and postcondition to every transition of the HDA, in a coherent way. A pre-region R of a precubical set C is a sequence (R i ) i∈N of functions R i : C(i) → N × N such that -for every x ∈ C(0), R 0 (x) = (0, 0) -for every x ∈ C(i + 1) and α k ∈ {-, +},

R i+1 (x) = i k=0 R 1 (∂ α k ¬k (x))
where the sum is computed coordinate by coordinate on pairs of integers.

Notice that, by the second property, a region is uniquely determined by the image of 1-dimensional cells in x ∈ C(1). We sometimes omit the index i since it is determined by the dimension of the cell in argument and respectively write R ′ (x) and R ′′ (x) for the first and second components of R(x), where x is a cell of C. It can be remarked that two 1-cells which are part of the same event necessarily have the same image under a pre-region; a pre-region R thus induces a function from the events of C to N × N, that we still write R. A region of a precubical set consists of a pre-region R together with a function S : C(0) → N such that for every i-cell y ∈ C(i) whose 0-source is x and 0-target is x ′ , there exists an integer n such that (S(x), S(x ′ )) = (n + R ′ (y), n + R ′′ (y)).

Example 38. Consider the following precubical set

x 3 x 1 y1 a a ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ z x 2 y3 ❈ ❈ ❈ ❈ ❈ ❈ ❈ ❈ x 0 y0 ❈ ❈ ❈ ❈ ❈ ❈ ❈ ❈ y2 a a ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ ⑤ y4 G G x 4
A region (R, S) for this cubical set is for example an adjunction between asynchronous transition systems and nets. Since the net associated to an HDA by the functor hda is generally infinite, we will give an example in the case of 1-bounded nets. Consider the asynchronous automaton, depicted on the left of (8), with an empty independence relation. (1,0)

❂ ❂ ❂ ❂ 1 (1,0) ❂ ❂ ❂ ❂ (0,0) d d ✁ ✁ ✁ ✁
Now, if we consider the same automaton with e 1 I x e 2 , we obtain the same Petri net with the place h removed. The general (i.e. non-bounded) net associated to an HDA is generally infinite (even for very simple examples) and thus difficult to describe, which is why we did not provide an example in the general case.

This adjunction can easily be lifted into an adjunction between LPNet and HDA.

Conclusion and future work

In this paper, we have made completely formal the relation between HDA and various classical models of concurrent computations: transition systems, asynchronous automata, event structures and Petri nets. This is not only interesting for comparison purposes, between different semantics of parallel languages, but also, for practical reasons, which will be detailed in a subsequent article.

Stubborn sets [START_REF] Valmari | A stubborn attack on state explosion[END_REF], sleep sets and persistent sets [START_REF] Godefroid | Using partial orders for the efficient verification of deadlock freedom and safety properties[END_REF] are methods used for diminishing the complexity of model-checking using transition systems. They are based on semantic observations using Petri nets in the first case and Mazurkiewicz trace theory in the other one. We believe that these are special forms of "homotopy retracts" when cast (using the adjunctions we have hinted) in the category of higher-dimensional transition systems. We shall make this statement more formal through these adjunctions, which will allow for new state-space reduction methods.

Last but not least, in [START_REF] Joyal | Bisimulation and open maps[END_REF] is defined an abstract notion of bisimulation. Given a model for concurrency, i.e. a category of models M and a "path category" (a subcategory of M which somehow represents what should be thought of as being paths in the models), then we can define two elements of M to be bisimilar if there exists a span of special morphisms linking them. These special morphisms have a path-lifting property that, we believe, would be in higher-dimensional transition systems a (geometric) fibration property. We thus hope that homotopy invariants could be useful for the study of a variety of bisimulation equivalences (some work has been done in that direction in [START_REF] Cattani | Higher dimensional transition systems[END_REF][START_REF] Fahrenberg | A category of higher-dimensional automata[END_REF]).

Proposition 5 .

 5 Suppose that C and D are categories and with S and T monads on respectively C and D. Suppose moreover that U : D → C is a functor such that U • T = S • U and F sends the unit and the multiplication of T to the unit and the multiplication of U . Then U has a left adjoint if and only if the functor U • I D : D T → C S has a left adjoint, where I D : D T → D is the canonical comparison functor between the Kleisli category D T associated to T and D.

  commute. By abuse of notation, we often write D ↓ G for the category Id D ↓ G. A labeled variant of cubical sets is defined as follows. Definition 8. The category of labeled symmetric precubical sets, denoted by LSPCSet, is the slice category SPCSet ↓ !. By Proposition 6, a given labeled symmetric precubical set (C, ℓ, L) (defined by C ∈ SPCSet, L ∈ Set and ℓ : C → ! L) can also be seen as a triple (C, ℓ, L) with the function ℓ : E(C) → L associating a label to each event of C. In other words, the category LSPCSet is isomorphic to E ↓ !, where E is the event functor introduced in Proposition 6. Example 9. The CCS processes ab + ba and (a|b) respectively induce labeled symmetric cubical sets of the form z y 1 b b b

1. 7 Proposition 15 .

 715 Relating variants of cubical sets. Suppose given two categories C and D and a functor I : C → D. Every presheaf C : D op → Set on C induces a presheaf C • I op : C op → Set by precomposition with I, and this operation extends into a functor Î : D → Ĉ from the presheafs on D to those on C, defined on morphisms α : C → D by ( Î(α)) A = α I(A) . These functors have many nice properties, some of which useful here are detailed below: Suppose given two categories C and D, where C is small, and a functor I : C → D between them.

Example 20 .

 20 The CCS processes a•(b+c), a•(b|c) and a•(b•c+c•b) respectively induce the following transition systems:

  s b implies τ (a) I ′ σ(s) τ (b) whenever τ (a) = * and τ (b) = * ). Example 22. The CCS processes a • (b|c) and a • (b • c + c • b) induces the labeled asynchronous transition systems whose underlying transition system are isomorphic and shown in Example 20. The independence relation contains e b I y e c for the first process (where e b and e c are the events with source y, labeled respectively by b and

Example 26 .

 26 The CCS processes a•(b+c), a•(b|c) and a•(b•c+c•b) respectively induce the following labeled Petri nets:In the diagrams above, we have used the usual notation for Petri nets: square nodes represent transitions, circled ones represent places (with dots indicating tokens) and arrows represent pre-and postconditions.

Example 32 .

 32 Consider the event structure (E, , #, ℓ, L), with E = {e 1 , e 2 , e 3 }, with e 1 e 2 and e 1 e 3 , labeled in L = {a, b, c} by ℓ(e 1 ) = a, ℓ(e 2 ) = b and ℓ(e 3 ) = c. This event structure is represented on the left and induces the two HDA on the right when b is respectively incompatible and compatible with c we simply write e for a 1-cell (x, e) since x can be determined as the source of the cell). The square on the right diagram is filled with two 2-cells: ({a}, b, c) and ({a}, c, b).

  any 2-dimensional HDA C with i as initial state and ℓ : C → ! L as labeling function, one can associate an unfolded 2-dimensional HDA U (C) whose -0-cells are the paths s : i -→ → x of C modulo homotopy, -1-cells are the pairs (s, m) where s : i -→ → x is a path and m is a 1-cell such that ∂ - 0 (m) = x, with ∂ - 0 (s, m) = s and ∂ + 0 (s, m) = s • m as source and target, -2-cells are pairs (s, z) where s : i -→ → x is a path and z is a 2-cell such that ∂ - 0 ∂ - 0 (z) = x, with its faces defined by ∂ - i (s, z) = (s, ∂ - i (z)) and

R(y 0

 0 ) = (2, 1) R(y 1 ) = (3, 1) R(y 2 ) = (3, 1) R(y 3 ) = (2, 1) R(y 4 ) = (0, 2)and R(z) = (5, 2) S(x 0 ) = 6 S(x 1 ) = 5 S(x 2 ) = 4 S(x 3 ) = 3 S(x 4 ) = 8

2 ( 8 )

 28 The associated 1-bounded Petri net is shown on the right. In this automaton the place d corresponds to the region (R, S) such that R(e 1 ) = (1, 0), R(e 2 ) = (0, 0), S(x) = S(y 2 ) = 1 and S(y 1 ) = S(z) = 0. Graphically,

This work has been supported by the PANDA ("Parallel and ANR project.

Relating models for concurrency

The purpose of this section is to relate traditional models introduced in Section 2 with the geometric models of Section 1 (mainly HDA).

Transition systems and HDA

In this section, we relate labeled transition systems and HDA. We begin by relating transition systems to the category of 1-dimensional HDA by defining two adjoint functors

We define the functor F as follows. To a 1-dimensional HDA C labeled by L, we associate the transition system (S, i, E, T ran) defined by S = C(0), i being the distinguished element of C, E = L and the transitions being defined by T ran = { (∂ - 0 (e), ℓ(e), ∂ + 0 (e)) | e ∈ E }. And to any morphism (ϕ, λ) : C → D between labeled precubical sets, we associate the morphism (σ, τ ) which is defined by σ = ϕ 0 : C(0) → D(0) and τ = λ. The functor is defined in the obvious way on morphisms.

Conversely, the functor G is defined as follows. To any transition system T = (S, i, E, T ran), we associate the strict 1-dimensional HDA C labeled by E whose underlying precubical set C is such that C(0) = S, C(1) = T ran, the face morphisms ∂ - 0 : C 1 → C 0 and ∂ + 0 : C 1 → C 0 are respectively defined by ∂ - 0 (s, e, s ′ ) = s and ∂ + 0 (s, e, s ′ ) = s ′ , the labeling function is defined by ℓ(s, e, s ′ ) = e and the distinguished element is the distinguished element i ∈ C(0). To any morphism (σ, τ ) : (S 1 , i 1 , E 1 , T ran 1 ) → (S 2 , i 2 , E 2 , T ran 2 ) we associate the morphism (κ, λ) of HDA, where κ is the morphism of pointed 1-dimensional precubical set whose components are κ 0 = σ and κ 1 = τ , the morphism λ between labels being τ . The functor is defined in the obvious way on morphisms.

The functors defined above enable us to relate both models:

Theorem 27. The functor F : sHDA 1 → sTS defined above is left adjoint to the functor G : sTS → sHDA 1 . The comonad F • G on sTS is the identity and the adjunction restricts to an equivalence of categories between the full subcategory of sHDA 1 whose objects are strongly labeled.

Proof. Suppose given a transition system T = (S, i, E, T ran) and a 1-dimensional HDA C = (C, i). We construct a natural bijection between morphisms F C → T in sTS and morphisms C → GT in sHDA 1 . To every morphism (σ, τ ) : F C → T of transition systems we associate the morphism of HDA ϕ C,T (σ, τ ) : C → GT defined as (κ, λ) where κ 0 = σ and κ 1 = λ = τ . Conversely, to every morphism (κ, λ) : C → GT of HDA we associate the morphism ψ C,T (κ, λ) : F C → T of transition systems defined as (κ 0 , λ). These operations are mutually inverse and can easily be shown to be natural. The second part of the proposition can be checked directly.

Graphically,

To This thus defines a functor pn : sHDA → sLPNet.

The adjunction.

Suppose that we are given an HDA C labeled by ℓ into L, and a labeled net N = (P, M 0 , E, pre , post , m, M ). We want to exhibit a bijection between morphisms pn(C) → N in sLPNet and morphisms C → hda(N ) in sHDA.

To any morphism (ϕ, ψ, λ) : pn(C) → N of labeled Petri nets, we associate a morphism (κ, λ) : C → hda(N ) of HDA defined as follows. Given an n-cell x of C, κ n (x) should be an n-cell of hda(N ), that is a pair (M κn(x) , l κn(x) ) where M κn(x) is a marking of N and l κn(x) is a list of events of N which is enabled at M κn(x) . These are defined for every place p of N by M κn(x) (p) = S ϕ(p) (y), where y is the 0-source of x, and

where y denotes the event associated to a 1-cell x.

Conversely, to any morphism (κ, λ) : C → hda(N ) of HDA, we associate a morphism of labeled Petri nets (ϕ, ψ, λ) : pn(C) → N defined as follows. Given an n-cell x, κ n (x) is an n-cell of hda(N ), that is a pair (M κn(x) , l κn(x) ) as above. For every place p, ϕ(p) is the region (R ϕ(p) , S ϕ(p) ) of C which is defined on 0-cells x by S ϕ(p) (x) = M κn(x) (p) and on n-cells x by R ϕ(p) = ( • l κn(x) , l • κn(x) ). Given a 1-cell x, its image under κ 1 (x) is a pair (M κ1(x) , l κ1(x) ) where l κ1(x) is reduced to one 1-cell y. It is immediate to check that for any other 1-cell x ′ such that x ≈ x ′ , we have that l κ1(x) ≈ l κ1(x ′ ) : it thus makes sense to extend x → l κ1(x) into a function which to an event e of C associates an event l κ1(e) . Given an event e of C, we define ψ(e) = l κ1(e) .

It can be shown that these transformations are well defined, are natural in C and N , and are mutually inverse. Therefore, Theorem 39. The functor hda : sLPNet → sHDA is right adjoint to the functor pn : sHDA → sLPNet.

Proof. It is routine to check that the transformations given above are welldefined and natural in C and N . We now show that they are mutually inverse.

Suppose that (ϕ, ψ, λ) : pn(C) → N is a morphism of Petri nets and consider the associated morphisms By definition of the transformations, we have that for every 0-cell

and similarly l

. Moreover, for every event e of C, ψ ′ (e) = ψ(e).

Conversely, suppose that (κ, λ) : C → hda(N ) is a morphism of cubical sets and consider the associated morphisms

which concludes the construction of the adjunction.

Example 40. If we restrict to 1-bounded nets, which are nets a place can contain either 0 or 1 token, we can recover the constructions of [START_REF] Winskel | Models for concurrency[END_REF] for constructing