N Kacem

S Hentz

S Baguet

R Dufour

High Order Nonlinearities and Mixed Behavior in Micromechanical Resonators

Keywords: Nonlinear dynamics, mixed behavior, strange attraction

This paper investigates the sensitivity of the third order nonlinearity cancellation to the mixed (hardening and softening) behavior in electrostatically actuated micromechanical resonators under primary resonance at large amplitudes compared to the gap. We demonstrate the dominance of the mixed behavior due to the quintic nonlinearities, beyond the critical amplitude when the third order mechanical and electrostatic nonlinearities are balanced. We also report the experimental observation of a strange attraction which can lead to a chaotic resonator.

Introduction

The large potential of microelectromechanical systems (MEMS) and nanoelectromechanical systems (NEMS) has been widely demonstrated for ultrasensitive force and mass sensing applications [START_REF] Rugar | Single spin detection by magnetic resonance force microscopy[END_REF][START_REF] Jensen | An atomic-resolution nanomechanical mass sensor[END_REF]. However, it is a challenge to enhance their dynamic range (DR) by achieving large amplitudes comparable to the gap in the case of electrostatically driven resonators without altering their frequency stability. Combined with the noise mixing issue [START_REF] Kaajakari | Phase noise in capacitively coupled micromechanical oscillators[END_REF] when the resonator is driven in the nonlinear regime, this leads to a drastic limitation on the sensor resolution.

An alternative to overcome this physical limitation is the hysteresis suppression by nonlinearity cancellation which has been the aim of extensive research work lately and requests the study of nonlinear dynamics of MEMS and NEMS. Most nonlinear models dealing with the nonlinearity cancellation in capacitive micro and nanoresonators includes nonlinear terms up to the third order [START_REF] Kozinsky | Tuning nonlinearity, dynamic range, and frequency of nanomechanical resonators[END_REF][START_REF] Shao | The nonlinearity cancellation phenomenon in micromechanical resonators[END_REF]. So even experimentally observed [START_REF] Shao | The nonlinearity cancellation phenomenon in micromechanical resonators[END_REF], the nonlinearity cancellation is limited by the high order nonlinearities which occur proportionally sooner with respect to the resonator size. Precisely, the onset of the mixed behavior is close to the critical amplitude for resonant NEMS sensors.

Indeed, accurate nonlinear models [START_REF] Kacem | Nonlinear dynamics of nanomechanical beam resonators: improving the performance of NEMS-based sensors[END_REF][START_REF] Kacem | Computational and quasi-analytical models for non-linear vibrations of resonant MEMS and NEMS sensors[END_REF] for large amplitudes includes all main sources of nonlinearities without Taylor series expansion of the nonlinear electrostatic forces. Kacem et al. developed complete multiphysics models including high order nonlinear terms and demonstrated analytically the ability to cancel out the nonlinearities in MEMS and NEMS capacitive clamped-clamped beam resonators [START_REF] Kacem | Nonlinear dynamics of nanomechanical beam resonators: improving the performance of NEMS-based sensors[END_REF] as well as cantilevers [START_REF] Kacem | Dynamic range enhancement of nonlinear nanomechanical resonant cantilevers for highly sensitive NEMS gas/mass sensor applications[END_REF]. Moreover, Kacem and Hentz [START_REF] Kacem | Bifurcation topology tuning of a mixed behavior in nonlinear micromechanical resonators[END_REF] identified experimentally the mixed behavior predicted in [START_REF] Kacem | Nonlinear dynamics of nanomechanical beam resonators: improving the performance of NEMS-based sensors[END_REF] i.e. they demonstrated the physical significance of the quintic nonlinear terms.

In this paper, we report experimentally the high sensitivity of the third order nonlinearity cancellation to the mixed behavior on a MEMS resonator under primary resonance at large amplitudes with respect to the gap. Based on a high order nonlinear model, the fabricated resonator was designed with a large ratio between its width and the sensing gap in order to maximize its global critical amplitude. We demonstrate the ability to reach very large amplitudes of order 90% of the sensing gap without pull-in occurrence. Moreover, strange attraction on a mixed behavior is experimentally identified which can lead in some configurations to chaos.

Experimental investigations

The fabricated resonator shown in Figure 1 consists in a silicon doubly clamped beam electrostatically in plane actuated and detected using two electrodes (electrode 1 for actuation and 2 for sensing) which allows for 2 port electric measurements.

It has been fabricated on 200 mm SOI (Silicon on insulator) wafers and microelectronic silicon processes. It is 200 µm long, 2 µm thick, 5 µm wide, the actuation gap is 1 µm, and the detection gap 300 nm. It has been designed to enable the compensation of the nonlinearities thanks to a compact analytical model [START_REF] Kacem | Nonlinear dynamics of nanomechanical beam resonators: improving the performance of NEMS-based sensors[END_REF] including all main sources of nonlinearities (electrostatic and mechanical) presenting non linear terms up to the seventh order as shown in Equation [START_REF] Rugar | Single spin detection by magnetic resonance force microscopy[END_REF].

(

1 + 4 ∑ i=1 µ i a i 1 ) ( ä1 + c ȧ1 ) + 2 ∑ i=0 ζ i a i 1 cos(Ωt) + 7 ∑ i=0 χ i a 1 i + 5 ∑ i=3 ζ i a i-3 1 cos(2Ωt) = 0 (1)
Fig. 1 SEM images of the fabricated resonator designed using a complete nonlinear model [START_REF] Kacem | Computational and quasi-analytical models for non-linear vibrations of resonant MEMS and NEMS sensors[END_REF].

The device was placed in a vacuum chamber (down to 1 mTorr), and the 2-port electrical measurements were performed at room temperature using a low noise lock-in amplifier (Signal Recovery 7280). As a first step, the critical behavior is approached in order to slowly access the nonlinear regime. Figure 2 displays a hardening behavior for which the mechanical nonlinearities are much higher than the electrostatic nonlinearities. Indeed, for a DC voltage of 1V , the nonlinear negative Duffing nonlinearity is very low which implies a high quality factor (Q ≈ 10 4 ). Hence, in this configuration, the mechanical critical amplitude is smaller than the electrostatic one (A c ≈ 80nm). The hardening resonance peak of Figure 2 has been obtained in sweep up and down frequency which displays a critical behavior at an output voltage of 7µV . The fabricated device has the characteristic of large width to gap ratio and consequently can potentially display a linear compensated behavior when both electrostatic and mechanical nonlinearities are balanced by increasing the nonlinear spring softening effect.

In order to approach this operating point (hysteresis suppression), the DC voltage has been increased to 3V and 5V as shown in Figure 3 where the resonance curves have been electrically characterized in sweep up and down frequency.

Since the negative nonlinear stiffness is proportional to the square of V dc (for V dc >> V ac ), unlike the first peak obtained at a DC voltage of 3V , the second one (left curve) measured for V dc = 5V displays nonlinear branches in the softening domain characterized by a complete modification of the dynamic bifurcation topology. The frequency shift between both curves due to the negative stiffness is about 2 KHz.

Moreover, the first peak measured at V dc = 3V displays a quality factor Q = 6000 which has been measured on a linear curve at a low AC voltage and the same DC voltage. The resonance curve, in this case, is strangely nonlinear (hardening behavior). The third bifurcation is the highest one in the hardening domain obtained in sweep up frequency where the corresponding curve displays two regimes: a first fast in amplitude variation and a second slow with a slope approaching zero. The first bifurcation is obtained in sweep down frequency and intercepts the sweep up frequency curve in a small part of the slow regime and the entire fast regime of amplitude variation. The strange nonlinear hardening behavior obtained experimentally can be explained by a strong dynamic perturbation due to the increase of the softening nonlinearitie. In Figure 3, the left resonance curve measured at V dc = 5V displays a quality factor Q = 4000. Using the analytical model of a 2 ports nonlinear resonator developped in [START_REF] Kacem | Nonlinear dynamics of nanomechanical beam resonators: improving the performance of NEMS-based sensors[END_REF], for these parameters, the resonator should display a linear resonance peak obtained by the compensation of the mechanical and the electrostatic nonlinearities. Unlike the mixed behavior (hardening-softening) demonstrated in [START_REF] Kacem | Bifurcation topology tuning of a mixed behavior in nonlinear micromechanical resonators[END_REF], the experimental peak measured at V dc = 5V displays clearly a mixed behavior starting by a softening branch and ending by a hardening one where the peak amplitude is around three times the critical amplitude displayed in Figure 2.

Particularly, in this mixed behavior, the P point and the first bifurcation have the same frequency and the hardening domain is reduced in comparison with the first resonance curve of Figure 3. Actually, for the fabricated resonator, the fifth order nonlinear terms are no more negligible when it is used to operate close to the hysteresis suppression point. Indeed, the compensation of the nonlinearities is sensitive to the highly unstable mixed behavior.

Once the mixed behavior was reached, we continue the increase of the DC voltage in order to track the transition from a mixed to a softening behavior as shown in Figure 4. The first peak has been measured at a DC voltage of 7.5V where the branches obtained in sweep down frequency enable the capture of two bifurcation points: the first one is the P point which corresponds to the initiation of the mixed behavior domain and the second one is the highest bifurcation point in the hardening domain. Then, in sweep up frequency, the output voltage V out follows the curve characterized by the bifurcation points 1 and 3. When the frequency of the first bifurcation point is reached, a strange attractor brings the resonator oscillation to the upper branch in the hardening domain instead of following the sweep down frequency curve (jump to the downer branch) which should be physically easier where the basins of attraction are quite larger. This is another illustration of the physical importance of the quintic nonlinearities. Hence, it is difficult to achieve large amplitudes for MEMS and NEMS capacitive resonators without altering their frequency stability.

In order to suppress the mixed behavior, the effect of the hardening nonlinearities is reduced in the second peak of Figure 4 for V dc = 10V and an estimated quality factor Q = 2000. The electrostatic nonlinearities are amplified with respect to the mechanical nonlinearities which brings the third bifurcation point at the same frequency as the first one. Remarkably, the resonator has reached very large oscillations up to 90% of the sensing gap without pull-in occurence. Nevertheless, the highest branch in the softening domain displays an inflection point (potentially due to the high order hardening nonlinearities) followed by a dynamic relaxation at the jump down bifurcation point.

Conclusions

In summary, we have demonstrated the high sensitivity of the third order nonlinearity cancellation to the mixed behavior in nonlinear capacitive clamped-clamped MEMS resonators under primary resonance at large oscillations. The experimental investigations were performed on a fabricated resonator designed using a complete analytical nonlinear model in order to balance the third order nonlinearities and drive the resonator linearly at high amplitudes. Beyond the critical amplitude, the quintic nonlinearities drastically limit the operating domain of the nonlinearity cancellation. Moreover, strange attractions become possible which can lead to undesirable chaotic sensors. Consequently, for nonlinear optimized resonant MEMS designs, the onset of the mixed behavior must be considered.

Fig. 2

 2 Fig. 2 Measured critical hardening resonance peak for V ac = 0.2V . W Max is the displacement of the beam at its middle point normalized by the gap g d .

Fig. 3

 3 Fig.3Measured strange hardening and mixed resonance peaks for V ac = 0.2V showing the changes on the bifurcation topologies. P is the mixed behavior initiation point and the third bifurcation is the highest point in the hardening domain.

Fig. 4

 4 Fig. 4 Measured mixed and softening resonance peaks for V ac = 0.2V .

Acknowledgements The authors gratefully acknowledge financial support from the CEA LETI and I@L Carnot institutes (NEMS Project) and from the MNTEurop Project.


N Kacem

S Hentz

S Baguet

R Dufour

Mixed behavior identification in nonlinear nanomechanical resonators

The small size of NEMS resonators combined with their physical attributes make NEMS quite attractive and suitable for a wide range of technological applications such as ultrasensitive force and mass sensing, narrow band filtering, and time keeping. However, at this size regime, nonlinearities occur sooner which reduce the NEMS dynamic range [1]. Consequently, a nonlinear multiphysics model is needed as a tool of performances optimization in resonant sensors for MEMS and NEMS designers.

To this end, the nonlinear behavior of resonators remains yet to be explored, and numerous models have been presented. Some models are purely analytical [2,3] but they include coarse assumptions concerning nonlinearities. Other models [4,5] are more complicated and use numerical simulations which make them less interesting for MEMS designers. In the present paper, a compact and analytical model including the main sources of nonlinearities (mechanical and electrostatic) is presented and validated thanks to the fabrication of a resonant accelerometer and the characterization of its sensing element, an electrostatically doubly clamped beam. A perturbation technique, the averaging method [START_REF] Nayfeh | Introduction to Perturbation Techniques[END_REF], has been used to obtain two first-order-nonlinear-ordinary-differential equations which describe the amplitude and phase modulation of the response and allows the computation of its stability. This analytical approach proves to be a powerful and quick tool for the sensor design, enabling the description of the competition between the hardening and the softening behavior (Figure 1), and thus the capture of all possible dynamic behaviors, particularly, the mixed behavior characterized by four bifurcation points. Furthermore, the model may be used as a tool to enhance the dynamic range of the resonator, i.e. its detectability.

On the way from MEMS to NEMS, a "small" MEMS resonant accelerometer [1] shown in Figure 2a has been fabricated. The sensor structure has not been designed to display high inertial performances, but rather is a way to validate process [START_REF] Kacem | [END_REF], characterization and model choices. In order to electrically characterize its sensitive part (the resonator described in Figure 2b), the device was placed in a vacuum chamber (down to 1 mTorr), and the 2-port electrical measurements were performed at room temperature using a low noise lock-in amplifier (Signal Recovery 7280). The drive voltage is V ac = 0.5V and the beam is polarized with V dc = 10V . This ensures a mixed behavior as shown in Figure 3. The quality factor obtained with this polarization voltage and in a linear regime is 4000. The critical amplitude [START_REF] Kacem | [END_REF] is then A c = 53nm, i.e. V c = 25µV . The peak obtained is then far beyond A c , up to 75% of the gap. The mixed behavior is fully identified with its four bifurcation points using a sweep up frequency to capture the points P and 2 as well as a sweep down frequency for points 1 and 3. Moreover, we experimentally track the point P (mixed behavior initiation point) while varying the drive and the bias voltage and we show that this bifurcation point is fixed by the design parameters. Then, the mixed behavior can be retarded and avoided by designing resonators for which the P point amplitude is close to the gap.

Further

  measurements are under work to validate the dynamic range enhancement based on the compensation of the nonlinearities shown by the model.

Figure 1 :

 1 Figure 1: Predicted forced frequency responses for several set of parameters. W max is the displacement of the beam normalized by the gap g d at its middle point l 2 .

Figure 2 :

 2 Figure 2: (a): SEM image of the resonant accelerometer. (b): Schema of an electrostatically clampedclamped resonator.

Figure 3 :

 3 Figure 3: Analytical and experimental forced frequency responses showing a mixed behavior.


Roberto Guanciale
email: robertog@kth.se

DiRPOMS: automatic checker of Distributed Realizability of POMSets

Keywords: Pomsets, choreography, realisability, CFSMs

DiRPOMS permits to verify if the specification of a distributed system can be faithfully realised via distributed agents that communicate using asynchronous message passing. A distinguishing feature of DiRPOMS is the usage of set of pomsets to specify the distributed system. This provides two benefits: syntax obliviousness and efficiency. By defining the semantics of a coordination language in term of pomsets, it is possible to use DiRPOMS for several coordination models. Also, DiRPOMS can analyze pomsets extracted by system logs, when the coordination model is unknown, and therefore can support coordination mining activities. Finally, by using sets of pomsets in place of flat languages, DiRPOMS can reduce exponential blows of analysis that is typical in case of multiple threads due to interleaving. 1

Introduction

Choreographic approaches advocate two views of the same distributed system: a global view that describes ordering conditions and constraints under which messages are exchanged, and local views that are used by each party to build their components. Here, the global view is a specification that is realised by combination of the local systems. As observed in [START_REF] Alur | Inference of Message Sequence Charts[END_REF], a source of problems is that there are some global specifications that are impossible to implement using distributed agents in a given communication model.

DiRPOMS is a tool designed to analyze realisability of choreographies. A choreography is formalized as a set of pomsets, were each pomset represents the causalities of events in one single branch of execution. Local views are modeled via finite state machines that communicate via asynchronous message passing. DiRPOMS checks realizability by verifying two closure conditions of the input pomsets and outputs the corresponding counterexamples:

WS-CDL

DiRPOMS

The first use case of our tool is design time analysis, where an architect checks if a choreography is realizable. In this case, violations of the closure conditions (i.e. the counterexamples) enable to identify behaviors that are not included in the choreography but are necessary in any distributed system that implements it (using finite state machines and asynchronous message passing). The usage of set of pomsets allows this analysis to be syntax oblivious, since the semantics of several existing choreographic models (i.e.

[11], [START_REF] Gunter | Compositional Message Sequence Charts[END_REF], [START_REF] Lange | From Communicating Machines to Graphical Choreographies[END_REF]) can be expressed using set of pomsets.

The second use case is choreography mining. In this case an analyst extracts a hypotheses choreography from (partial) execution logs of a distributed system. Here, violations of the closure conditions enable to identify behaviors of the distributed system that are not included in the logs, so supplementing partial information regarding the system under test and reducing the number of executions needed to extract a model of the system.

The paper is organized as follows. In Section 2 we present the models for local and global views and in Section 3 we briefly recall the theory supporting our tool. Section 4 presents some examples of faulty choreographies, which cannot be implemented using communicating finite state machines. Section 5 shows an example of choreography mining, where the tool is used to identify missing traces from a partial execution log. Usage, implementation, and evaluation of the tool are presented in Sections 6, 7, and 8.

Local and global views of choreographies

We assume a set P of distributed participants (ranged over by A, B, etc.) and a set M of messages (ranged over by m, x, etc.). Participants communicate by exchanging messages over channels, that are elements of the set C = (P × P ). The set of (communication) labels L, ranged over by l and l , is defined by

L = L ! ∪L ?
where (outputs) L ! = C ×{!}×M and (inputs) L ? = C ×{?}×M we shorten (A, B, !, m) as A B!m and (A, B, ?, m) as A B?m. The subject of output and input are the sender (sbj A B!m = A) and receiver (sbj A B?m = B) respectively.

Local systems are modeled in terms of communicating fine state machines [START_REF] Alur | Inference of Message Sequence Charts[END_REF].

Definition 1. An A-communicating finite state machine (A-CFSM) M = (Q, q 0 , F, →)
is a finite-state automaton on the alphabet {l ∈ L | sbj l = A} such that, q 0 ∈ Q is the initial state, and F ⊆ Q are the accepting states. A (communicating) system is a map S assigning an A-CFSM to each participant A ∈ P . A configuration of a communicating system consists of a state-map q, which maps each participant to its local state, and buffer-map b, which maps each channel and message to the number of outputs that have been consumed. A configuration is accepting if all buffers are empty and the local state of each participant is accepting while it is a deadlock if no accepting configuration is reachable from it. The initial configuration is the one where, for all A ∈ P , q(A) is the initial state of the corresponding CFSM and all buffers are empty. The semantics of communicating systems is defined in terms of a labeled transition relation between configurations. Each transition models one action performed by one machine: an output, which adds a message to a channel, or an input, which consumed a pending message from a channel. Formally q ; b l = ⇒ q ; b if there is a message m ∈ M such that either (1) or (2) below holds:

A0 A1 A2 A3 A B!x A B!y A B!z A B!z B0 B1 B2 B3 B4 B5 B6 A B?x A B?y C B?x C B?x A B?x A B?z C B?x A B?y A B?z C0 C1 C B!x M A M B M C
1. l = A B!m, q(A) l - → q (A), q (C) = q(C) for all C = A ∈ P , and b (A B) = b(A B)[m → b(A B)(m) + 1] 2. l = A B?m, q(B) l - → q (B), q (C) = q(C) for all C = B ∈ P , b(A B)(m) > 0 and b (A B) = b(A B)[m → b(A B)(m) -1]
where, f [x → y] represents updating of a function f in x with a value y. Definition 2. The language of a communicating system S is the set L(S) ∈ L of sequences l 0 . . . l n-1 such that exist a trace labeled with l 0 . . . l n-1 that start in the initial configuration and ends in an accepting configuration.

The notion of realisability is given in terms of the relation between the language of the global view and the one of a system of local views "implementing" it [START_REF] Alur | Inference of Message Sequence Charts[END_REF].

Definition 3 (Realisability). A language L ⊆ L is weakly realisable if there is a communicating system S such that L = L(S); when S is deadlock-free we say that L is safely realisable.

We model the global views in terms of sets of pomsets, where each pomset models one branch of execution. Definition 4 (Pomsets [START_REF] Gaifman | Partial order models of concurrency and the computation of functions[END_REF]). A labelled partially-ordered set (lposet) is a triple (E, ≤, λ), with E a set of events, ≤⊆ E × E a reflexive, anti-symmetric, and transitive relation on E, and λ : E → L a labelling function mapping events in E to labels in L.

A partially-ordered multi-set (of actions), pomset for short, is an isomorphism class of lposets, where (E, ≤, λ) and (E , ≤ , λ ) are isomorphic if there is a bijection φ : E → E such that e ≤ e ⇐⇒ φ(e) ≤ φ(e ) and λ = λ • φ.

     A B!x A B!z A B?x A B?z C B?x C B!x   ,   A B!y A B!z A B?y A B?z C B?x C B!x     
Fig. 2: A set of two pomsets that represents the global view of the system of Figure 1 Pomsets allow to represent scenarios where the same communication occurs multiple times. Intuitively, ≤ represents causality; if e < e then e is caused by e. Note that λ is not required to be injective: λ(e) = λ(e ) means that e and e model different occurrences of the same action. In the following, [E, ≤, λ] denotes the isomorphism class of (E, ≤, λ), symbols r, r , . . . (resp. R, R , . . . ) range over (resp. sets of) pomsets, and we assume that pomsets r contain at least one lposet which will possibly be referred to as (E r , ≤ r , λ r ).

The projection r A of a pomset r on a participant A ∈ P is obtained by restricting r to the events having subject A. We will represent pomsets as (a variant of) Hasse diagrams of the immediate predecessor relation.

A pomset is well-formed if (1) for every output A B!m there is at most one immediate successor input A B?m, (2) for every input A B?m there exists exactly one immediate predecessor output A B!m, (3) if an event immediately precedes an event having different subjects then these events are matching output and input respectively, (4) ordered output events with the same label cannot be matched by inputs that have opposite order. A pomset is complete if there is no output event in without a matching input event.

Definition 5. Given a pomset r = [E, ≤, λ], a linearization of r is a string in L obtained by considering a total ordering of the events E that is consistent with the partial order ≤ , and then replacing each event by its label. The language of a pomset (L(r)) the set of all linearizations of r. The language of a set of pomsets R is simply defined as

L(R) = r∈R L(r).
The set of pomsets of Figure 2 represents the global view of the system of Figure 1, i.e. the two views have the same language. The two pomsets represents two different scenarios (i.e. branches): in the left scenario A sends x, in the right scenario A sends y.

Realisability conditions

Our tool uses the verification conditions for realisability identified in [START_REF] Guanciale | Realisability of pomsets via communicating automata[END_REF]. These conditions requires to introduce the following definitions.

Definition 6 (Inter-Participant Closure). Let (r A ) A∈P be the tuple where r A = r A A for all A ∈ P . The inter-participant closure ((r A ) A∈P ) is the set of all well-formed pomsets

[ A∈P E r A , ≤ I ∪ A∈P ≤ r A , A∈P λ r A ] where ≤ I ⊆ {(e A , e B ) ∈ E r A × E r B , A, B ∈ P λ r A (e A ) = A B!m, λ r B (e B ) = A B?m}.
The inter-participant closure takes one pomset for every participant and generates all "acceptable" matches between output and input events. We use the following tuple of pomsets (r A , r B ) to illustrate the inter-participant closure.

r A =          A B!x e1 e2 A B!x A B!x e3 e4          r B =          A B?x e5 e6 A B?x A B?x e7         
Pomset r A represents a fork while pomset r B represents a join. The inter-participant closure of (r A , r B ) consists of four well-formed pomsets:

         A B!x e1 e2 A B!x A B!x e3 e4 A B?x e5 e6 A B?x A B?x e7                   A B!x e1 e2 A B!x A B!x e3 e4 A B?x e5 e6 A B?x A B?x e7                    A B!x e1 e2 A B!x A B!x e3 e4 A B?x e5 e6 A B?x A B?x e7                     A B!x e1 e2 A B!x A B!x e3 e4 A B?x e5 e6 A B?x A B?x e7          
Definition 7 (More permissive relation). A pomset r is more permissive than pomset r, written r r , when E r = E r , λ r = λ r , and ≤ r ⊇≤ r .

The more permissive relation guarantees language inclusion, i.e. if r r then L(r) ⊆ L(r ).

Definition 8 (Prefix pomsets).

A pomset r = [E , ≤ , λ ] is a prefix of pomset r = [E, ≤, λ] if there exists a label preserving injection φ : E → E such that φ(≤ ) =≤ ∩(E × φ(E )).
A prefix of a pomset r is a pomset on a subset of the events of r that preserves the order and labelling of r.

The realisability conditions presented in [START_REF] Guanciale | Realisability of pomsets via communicating automata[END_REF] are two closure conditions, which are formalized by the following theorem Theorem 1. If R satisfies CC2-POM then L(R) is weak realisable, if R also satisfies CC3-POM then its language is safe realisable, where -CC2-POM(R) for all tuples (r A ) A∈P of pomsets of R, for every pomset r ∈ ((r A A ) A∈P ), there exists r ∈ R such that r r .

-CC3-POM(R) for all tuples of pomsets (r A ) A∈P such that rA is a prefix of a pomset r A ∈ R for every A, and for every pomset r ∈ ((r A A ) A∈P ) there is a pomset r ∈ R and a prefix r of r such that r r .

Intuitively CC2-POM requires that if all the possible executions of a pomset cannot be distinguished by any of the participants of R, then those executions must be part of the language of R. Similarly, CC3-POM requires that if all partial executions cannot be distinguished by any of the participants of R, then those executions must be a prefix of the language of R.

Realisability by examples

In this section we give some examples of the problems related to implementing pomsetbased choreographers using CFSMs. Distributed choices can prevent faithful implementations in case of lack of coordination. For example, the set R 1 models two branches. Participants A and C should both send the message x or both send the message y. However, A and C do not coordinate to achieve this behaviour; this makes it impossible for them to distributively commit to a common choice. R 1 satisfies CC2-POM. However, pomset r 1 , which represents the case A and C do not agree on the message to deliver, is in the inter-participant closure of prefixes and violates CC3-POM.

             A B!x A B!z A B?x A B?z C B?x C B!x   ,       A B!y A B!z A B?y C B?y A B!z C B!y                    A B!y A B!z A B?y C B!x   R 1 r 1 A different problem affects R 2 .
Here the two branches describe different orders of the same set of events. The behaviour of A (and D) is the same in both branches: A (resp. D) concurrently sends message x (resp. y) to B and C. The behaviours of B and C differ: in the left branch they first receive the message from A then the one from D, in the right branch, they have the same interactions but in opposite order. This choreography cannot be realised since, intuitively, it requires B and C to commit on the same order of reception without communicating with each other. Pomset r 2 , which captures the case when B and C do not agree on the order of message reception, is in the inter-participant closure and violates CC2-POM.

                          A B!x A B?x D B?y D B!y A C?x A C!x D C?y D C!y          ,        D B?y D B!y A B?x A B!x D C!y D C?y A C?x A C!x                                 D B?y D B!y A B?x A B!x A C?x A C?x D C!y D C?y         R 2 r 2
The last example demonstrates problems led by the usage of the same message in the concurrent threads. The set R 3 : consists of a single pomset, which represents two concurrent sub-choreographies. The usage of message x in both threads can cause the following problem: (1) the left thread of A executes A C!l 1 and A B!x; (2) after the output B C!r 2 , the right thread of B executes the input A B?x, so "stealing" the message x generated by the left thread of A and meant for the left thread of B; (3) the right thread of B executes B C!r 3 . Pomset r 3 , which represents this case, is in the inter-participant closure and violates CC2-POM.

                             A C!l1 B C!l2 A B?x A B!x B C!l3 A C?l1 B C?l2 A C?l3 A C!r1 A C?r1 B C!r2 A B?x A B!x B C!r3 B C?r2 A C?r3                                        A C!l1 B C!l2 A B?x A B!x B C!l3 A C?l1 B C?l2 A C?l3 A C!r1 A C?r1 B C!r2 A B?x A B!x B C!r3 B C?r2 A C?r3           R 3 r 3

Identifying missing execution logs for choreography mining

Choreography (and process) mining [START_REF] Van Der Aalst | Process mining: discovery, conformance and enhancement of business processes[END_REF] consists of extracting a hypothesis choreography from a partial execution log of a distributed system. In this section we show that violations of the closure conditions can be used to identify behaviors of the distributed system that are not included in the log. Therefore the closure conditions can support the mining and testing activities.

Let the partial execution log of the system of Figure 1 contains the following traces ----------+----------------+-------AB ! y ; AB ! z | CB?x ; . . .

A l o g | B l o g | C l o g -----------+----------------+------- AB ! x ;

| CB! x

This information can be used to fix the hypothesis choreography, by enabling the traces that are necessarily part of the behaviors of the distributed system. The set of pomsets of Figure 2 satisfies both closure conditions and its language includes the initial partial execution log.

Tool usage

DiRPROM is written in Python and provides a set of API to build and manipulate pomsets and to check the closure conditions. The API can be invoked by any Python development environment (in the demo video we use org-mode [START_REF] Schulte | A multi-language computing environment for literate programming and reproducible research[END_REF] for analyzing the examples using literate programming).

A typical DiRPOM session starts by defining the set of pomsets modeling the choreography. Pomsets can be loaded using the existing formats (including GEXF, GraphML, and JSON), be generated by translating other choreography models, or be dynamically generated. For example, the following snippet creates R 1 as input choreography: # a d d p a i r ( gr1 ,A ,B ,n ,m) c r e a t e s two node " out-n " and " i n-n " # l a b e l e d w i t h AB !m and AB?m, connects t h e two events and r e t u r n s # t h e p a i r ( out-n , i n-n ) abx = a d d p a i r ( gr1 , " a " , " b " , 1 , " x " ) cby = a d d p a i r ( gr1 , " c " , " b " , 2 , " x " ) abz = a d d p a i r ( gr1 , " a " , " b " , 3 , " z " ) # I n p u t pomsets do n o t need t o be t r a n s i t i v e ( t r a n s i t i v e c l o s u r e # i s done i n t e r n a l l y ) gr1 . add edge ( abx [START_REF] Alur | Inference of Message Sequence Charts[END_REF] , abz [START_REF] Alur | Inference of Message Sequence Charts[END_REF] ) gr1 . add edge ( cby [START_REF] Alur | Inference of Message Sequence Charts[END_REF] , abz [START_REF] Alur | Inference of Message Sequence Charts[END_REF] ) gr1 . add edge ( abx [ 0 ] , abz [ 0 ] ) g l o b a l v i e w . append ( gr1 ) # r i g h t pomset o f R2 gr2 = nx . DiGraph ( ) abx = a d d p a i r ( gr2 , " a " , " b " , 1 , " y " ) cby = a d d p a i r ( gr2 , " c " , " b " , 2 , " y " ) abz = a d d p a i r ( gr2 , " a " , " b " , 3 , " z " ) gr2 . add edge ( abx [START_REF] Alur | Inference of Message Sequence Charts[END_REF] , cby [START_REF] Alur | Inference of Message Sequence Charts[END_REF] ) gr2 . add edge ( cby [START_REF] Alur | Inference of Message Sequence Charts[END_REF] , abz [START_REF] Alur | Inference of Message Sequence Charts[END_REF] ) gr2 . add edge ( abx [ 0 ] , abz [ 0 ] ) g l o b a l v i e w . append ( gr2 )

The closure condition CC2-POM can be checked using The result cc2res is a map that yields for each index i of cc2c the index of global_view matching it or None if cc2c[i] is a counterexample. Similarly closure condition CC3-POM can be checked using ( cc3c , p r e f ) = c c 3 c l o s u r e ( g l o b a l v i e w ) # cc3c and p r e f i x are l i s t s cc3res = cc3pom ( cc3c , p r e f )

The list pref contains the list of prefixes of the input choreography, and the result cc3res maps each index of cc3c to an index of pref or None. The counter examples can be rendered using: e r r o r s = counterexamples ( cc3c , cc3res ) debug graphs ( e r r o r s , " o u t p u t-f o l d e r " ) # generates p i c t u r e s o f e r r o r s DiRPOM also provides a command line utility, which uses GraphML format for input and output of pomsets. The left pomset of R 1 can be defined by the following GraphML file:

<?xml v e r s i o n = ' 1 . 0 ' encoding= ' u t f -8 ' ?> <graphml >
<key a t t r . name= " l a b e l " a t t r . t y p e = " s t r i n g " f o r = " node " i d = " d0 " /> <graph e d g e d e f a u l t = " d i r e c t e d "> <node i d = " b-2"><data key= " d0 ">CB?x</ data></ node> <node i d = " b-3"><data key= " d0 ">AB?z</ data></ node> <node i d = " b-1"><data key= " d0 ">AB?x</ data></ node> <node i d = " a-1"><data key= " d0 ">AB ! x</ data></ node> <node i d = " a-3"><data key= " d0 ">AB ! z</ data></ node> <node i d = " c-2"><data key= " d0 ">CB! x</ data></ node> <edge source= " b-2" t a r g e t = " b-3" /> <edge source= " b-1" t a r g e t = " b-3" /> <edge source= " a-1" t a r g e t = " a-3" /> <edge source= " a-1" t a r g e t = " b-1" /> <edge source= " a-3" t a r g e t = " b-3" /> <edge source= " c-2" t a r g e t = " b-2" /> </ graph> </ graphml> Each GraphML must contain a key element, specifying the existence of the node attribute label of type string. Each node has a unique identifier and a data sub-element, which defines the node label. The following command executes the analysis of a choreography:

dirpom [ i n p u t ] [ o u t p u t 1 ] [ o u t p u t 2 ] --draw --graphml

Tool implementation

DiRPROM relies on the NetworkX package for graph operations. In fact, pomsets are represented as direct labelled acyclic graphs. The tool consists of five modules:

utils: provides export of pomsets to png and utilities to build pomsets pomset: provides functions to process pomsets, e.g. query lists of participants and messages, projections per participant or message, transitive closure and reduction, enumeration of prefixes, enumeration of linearizations

Tool evaluation

The main primitive of NetworkX used by the tool is subgraph_is_ismorphic, which returns true iff r 1 is (label-preserving) isomorphic to a subgraph of r 2 . If r 1 and r 2 have the same number of nodes and the predicates holds then r 2 r 1 . The complexity of finding a label-preserving graph isomorphism is in general exponential in the number of events. However, since the graphs are acyclic, the complexity can be bound to the number of concurrently-repeated actions: i.e. events that have the same label, are unordered, and have the same number of predecessor with the same label (e.g. A B!x in R 3 ). If there are no concurrently repeated actions then isomorphism of pomsetes can be checked in polynomial time with respect to the number of events.

We report the performance of our tool for the examples. The experiments have been executed on a Intel 2.2 Ghz i7 with 16 GB of RAM. The table reports the size of the closures, the number of counterexamples, and the processing time in milliseconds. In general the evaluation of closure conditions is fast for simple examples. However, the number of prefixes to check in CC3-POM can be large when participant have several concurrent threads. One of the advantages of checking CC -POM with respect to previous work [START_REF] Alur | Inference of Message Sequence Charts[END_REF] is that the former does not require the explicit computation of the language of the family of pomsets, which can lead to combinatorial explosion due to interleavings. In fact, in case of concurrency, the number of prefixes is usually smaller than the number of possible linearizations of a pomset. For example, the following pomset consists of two independent threads, each one consisting of n sequential and distinguished events

CC2-POM

  e1 e2 . . . en e 1 e 2 . . . e n  
The closure condition in [START_REF] Alur | Inference of Message Sequence Charts[END_REF] requires to directly compute the language of the pomset, which has 2 n words. Instead, the prefix of the pomset are (n + 1) 2 . As a further example, the set of pomsets R 3 contains one pomset and has two actions that occur in both threads: A B!x and A B?x. The inter-participant closure has exactly two pomsets: the element of R 3 itself and r 3 . The left and right subpomsets of R 3 , which represent the two threads, have 32 different linearizations, each one consisting of 8 events. Therefore the language of R 3 consists of 32 * 32 * 2 8 = 2 18 words. On the other hand, analyzing CC3-POM for R 3 requires to check 668 prefixes.

Concluding remarks

Realisability of specifications is of concern for both practical and theoretical reasons. Several works (e.g., [START_REF] Bocchi | Resolving non-determinism in choreographies[END_REF]3,[START_REF] Honda | Multiparty asynchronous session types[END_REF]) defined constraints to guarantee soundness of the implementation of choreographies. These approaches address the problem for specific languages and use conditions that rely on the syntactical structure of the specification. DiRPOMS provides a language independent tool to check realisability of choreographies. Therefore, it can be used for several choreographic models, as long as their semantics can be expressed via set of partial orders.

There two main limitations of DiRPOMS that we plan to address. First, our tool cannot analyze recursive choreographies, since their pomset based semantics is infinite. Even if loops are bounded, naive loop unrolling can easily generate large sets of pomsets which are intractable. Secondly, CC -POM conditions are sufficient but not necessary conditions for realisability. In fact, the same set of traces can be expressed using different sets of pomsets by exploring different interleavings. We are currently investigating a notion of normal forms for families of pomsets that can be used to guarantee that our conditions are necessary.

We are also working on optimizing our tool. In particular we think that it is possible to demonstrate equivalence between CC3-POM and a different formulation, which requires to check only a subset of prefixes. For instance, in verifying CC3-POM for R 3 , the analysis of the prefix A C!l1 A C!r1 covers also the cases of the prefixes A C!l1 and A C!r1 .

Figure 1

 1 Figure 1 presents a system with three participants: A, B, and C. Participant C always sends message x to B. Participant A sends two messages to B: the first message is x or y; the second message is always z. Participant B receives the first message from A and C in any order, then it receives the second message of A.A configuration of a communicating system consists of a state-map q, which maps each participant to its local state, and buffer-map b, which maps each channel and message to the number of outputs that have been consumed. A configuration is accepting if all buffers are empty and the local state of each participant is accepting while it is a

Fig. 1 :

 1 Fig. 1: A system consisting of CMFSs. Initial states are A 0 , B 0 , and C 0 . Accepting states are A 3 , B 5 , and C 1 .



  AB ! z | AB?x ;CB?x ; AB?z | CB! x AB ! x ; AB ! z | CB?x ; AB?x ; AB?z | CB! x AB ! y ; AB ! z | AB?y ;CB?x ; AB?z | CB! x A choreography that precisely represents these traces is the following set of pomsets: This set of pomsets satisfies CC2-POM, but it does not satisfy CC3-POM. The following pomset is in the inter-participant closure of prefixes and violates CC3-POM:This pomset represents the fact that there must be an execution of the system where A sends y and B receives the first message from C, i.e.: A l o g | B l o g | C l o g -

#

  a choreography i s a l i s t o f pomsets g l o b a l v i e w = [ ] # a pomset i s a d e f i n e d u s i n g a d i r e c t e d graph # l e f t pomset o f R1 gr1 = nx . DiGraph ( )

cc2c = c c 2

 2 c l o s u r e ( g l o b a l v i e w ) # cc2c i s t h e l i s t o f pomsets cc2res = cc2pom ( cc2c , g l o b a l v i e w )

-

  inter_closure: implements inter-participant closure ccpom: generates the two closure sets and verifies the closure conditions dirpom: provides the command line utility In order to demonstrate the implementation of the analyses and the internal API, we report the implementation of CC3-POM: d e f c c 3 c l o s u r e ( graphs ) : # r e t r i e v e s t h e l i s t o f p r i n c i p a l s i n graphs p r i n c i p a l s = pomset . g e t a l l p r i n c i p a l s ( graphs ) # p r o j e c t s t h e i n p u t graphs on p r i n c i p a l s and y i e l d s a map mapping # p r i n c i p a l s t o l i s t o f " l o c a l " pomsets ( a v o i d s d u p l i c a t e s ) l o c a l t h r e a d s = pomset g e t p r i n c i p a l t h r e a d s ( graphs , p r i n c i p a l s ) l o c a l p r e f i x e s = {} f o r p i n p r i n c i p a l s : # computes a l l p r e f i x e s o f a l l graphs i n l o c a l t h r e a d s [ p ] # ( a v o i d s d u p l i c a t e s ) l o c a l p r e f i x e s [ p ] = pomset . g e t p r e f i x e s ( l o c a l t h r e a d s [ p ] ) # generates a l l t u p l e s i n t h e p r o d u c t o f l o c a l p r e f i x e s t u p l e s = i n t e r c l o s u r e . make tuples ( l o c a l p r e f i x e s ) # computes t h e i n t e r -p a r t i c i p a n t c l o s u r e o f a l l t h e t u p l e s # ( a v o i d s d u p l i c a t e s ) i p c = i n t e r c l o s u r e . i n t e r p r o c e s s c l o s u r e ( t u p l e s ) # computes a l l p r e f i x e s o f t h e i n p u t graphs ( a v o i d s d u p l i c a t e s ) p r e f i x e s = pomset . g e t p r e f i x e s ( graphs ) r e t u r n ( i p c , p r e f i x e s ) d e f cc3pom ( i p c , p r e f i x e s ) : matches = {} f o r i i n range ( l e n ( i p c ) ) : matches [ i ] = None f o r j i n range ( l e n ( graphs ) ) : # checks i f graph [ j ] i s more p e r m i s s i v e than i p c [ i ] i f ( pomset . i s m o r e p e r m i s s i v e ( graph [ j ] , i p c [ i ] ) ) : matches [ i ] = j break r e t u r n matches

  i m p o r t networkx . a l g o r i t h m s . isomorphism as i s o nm = i s o . c a t e g o r i c a l n o d e m a t c h ( ' l a b e l ' , ' ' ) d e f i s m o r e p e r m i s s i v e ( g1 , g2 ) : i f l e n ( g1 . nodes ( ) ) ! = l e n ( g2 . nodes ( ) ) : r e t u r n False m = i s o . GraphMatcher ( g1 , g2 , nm) r e t u r n m. s u b g r a p h i s i s o m o r p h i c ( )

Demo video available at https://youtu.be/ISYdBNMxEDY

Tool available at https://bitbucket.org/guancio/chosem-tools/


Hernán Melgratti

Claudio Antares Mezzina

Irek Ulidowski

Claudio Antares Mezzina

Reversing P/T Nets

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Reversible computing is attracting interest for its applications in many fields including hardware design and quantum computing [START_REF] Vos | Synthesis of Quantum Circuits vs. Synthesis of Classical Reversible Circuits[END_REF], the modelling of biochemical reactions [START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF][START_REF] Kuhn | A calculus for local reversibility[END_REF][START_REF] Pinna | Reversing steps in membrane systems computations[END_REF], parallel discrete event simulation [START_REF] Schordan | Generation of reversible C++ code for optimistic parallel discrete event simulation[END_REF] and program reversing for debugging [START_REF] Giachino | Causal-consistent reversible debugging[END_REF][START_REF] Lanese | Cauder: A causal-consistent reversible debugger for Erlang[END_REF][START_REF] Hoey | Reversing imperative parallel programs with blocks and procedures[END_REF].

A model for reversible computation features two computation flows: the standard forward direction and the reverse one, which allows to reach back any past state of the computation. Reversibility is well understood in a sequential setting in which executions are totally ordered sets of events (see [START_REF] Leeman | A formal approach to undo operations in programming languages[END_REF]): a sequential computation can be reversed by successively undoing the last not yet undone event. Reversibility becomes more challenging in a concurrent setting because there is no natural way for totally ordering events. Often concurrency models account for the causal dependencies among events, which are reflected as a partial order. Reversing an execution consisting of a partially ordered set of events reduces to successively undoing one of the maximal events not yet undone. This is at the basis of the causally-consistent reversibility [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Lanese | Causal-consistent reversibility[END_REF], which relates reversibility with causality. Intuitively, this notion stipulates that any event can be undone provided that all its consequences, if any, are undone beforehand. Reversibility in distributed systems such as in checkpoint/rollback protocols [START_REF] Vassor | Checkpoint/rollback vs causally-consistent reversibility[END_REF] and in transactions [START_REF] Danos | Transactions in RCCS[END_REF][START_REF] Lanese | Concurrent flexible reversibility[END_REF] can be modelled by causal-consistent reversibility. The interplay between reversibility and concurrency has been widely studied in process

• Ñ Ñ ) ) a t1 t2 b c t3
)

) t4 Ñ Ñ d (a) Initial Ñ Ñ ) ) a t1 t2 b c t3
)

) t4 Ñ Ñ • d (b) Final Ñ Ñ
) calculi [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF][START_REF] Cristescu | A compositional semantics for the reversible π-calculus[END_REF][START_REF] Medic | A parametric framework for reversible π-calculi[END_REF], event structures [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF][START_REF] Cristescu | Rigid families for CCS and the π-calculus[END_REF][START_REF] Ulidowski | Reversing event structures[END_REF][START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF] and lately Petri Nets [START_REF] Philippou | Reversible computation in Petri nets[END_REF][START_REF] Barylska | Reversing computations modelled by coloured Petri nets[END_REF]. Despite being a very basic model of concurrency, Petri nets still lack a satisfactory causally-consistent reversible semantics. For instance, no current models are able to handle cyclic nets.

) a t -1 1 P P t1 t2 t -1 2 l l b b b c t -1 3 b b t3 ) ) t4 Ñ Ñ t -1 4 • c c d (c) Naive reversing
A key point when reversing computation in Petri nets is to handle backward conflicts, i.e., the fact that a token can be generated in a place because of different causes. Consider the net in Figure 1(a) showing the initial state of a system that can either perform t 1 followed by t 3 , or t 2 followed by t 4 . The final state of a complete computation is depicted in Figure 1(b). The information in that state is not enough to deduce whether the token in d has been produced because of t 3 or t 4 . Even worse, if we "naively" reverse the net by just adding transitions in the reverse direction, as shown in Figure 1(c), the reverse transition will do more than undoing the computation. In fact, the token in d can be put back either in b or c regardless of the previous computation.

Analogous problems arise when a net is cyclic. Previous approaches [START_REF] Philippou | Reversible computation in Petri nets[END_REF][START_REF] Barylska | Reversing computations modelled by coloured Petri nets[END_REF] to reversing Petri nets tackle backward conflicts by relying on a new kind of tokens, called bonds that keep track of the execution history. Bonds are rich enough for allowing other approaches to reversibility, such as out-of-order reversibility [START_REF] Kuhn | A calculus for local reversibility[END_REF], but they cannot cope with cyclic nets. We propose here a reversible model for p/t nets that can handle cyclic nets by relying on standard notions in Petri net theory. We first observe that a Petri Net can be mapped via the standard unfolding construction to an occurrence net, i.e., an acyclic net that does not have backward conflicts and makes causal dependencies explicit. Then, an occurrence net can be "simply" reversed by reversing each of its transitions. Such construction gives a model that features causally-consistent reversibility. This is shown by proving that each reachable marking in the reversible version of the occurrence net is a marking that can be reached by just forward computational steps. We observe that the unfolding construction could produce an infinite occurrence net. However, the unfolding can be seen as the definition of a coloured net, where colours account for causal histories. Such interpretation associates a p/t net with an equivalent coloured p/t net, which can be reversed in the "simple" way. The correctness of the construction is shown by exhibiting a oneto-one correspondence of its executions with the ones of the reversible version of the unfolding. Interestingly, the colours used by the construction resemble the memories common in reversible calculi [START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF][START_REF] Danos | Reversible communicating systems[END_REF].

We remark that our proposal deals with reversing (undoing) computation in a Petri net and not with the classical problem of reversibility [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups[END_REF] which requires every computation to be able to reach back the initial state of the system (but not necessary by undoing the previous events). In this sense, the problem of making a net reversible equates to adding a minimal amount of transitions that make a net reversible [START_REF] Barylska | Reversible computation vs. reversibility in Petri nets[END_REF]. Reversibility is a global property while reversing a computation is a local one, as discussed in [START_REF] Barylska | Reversible computation vs. reversibility in Petri nets[END_REF].

Background

Petri Nets

Petri nets are built up from places (denoting, e.g., resources and message types), which are repositories for tokens (representing instances of resources), and transitions, which fetch and produce tokens. We consider the infinite sets P of places and T of transitions, and assume that they are disjoint, i.e., P ∩ T = ∅. We let a, a , . . . range over P and t, t , . . . over T . We write x, y, . . . for elements in P ∪T .

A multiset over a set S is a function m : S → N (where N denotes the natural numbers including zero). We write N S for the set of multisets over S. For m ∈ N S , supp(m) = {x ∈ S | m(x) > 0} is the support of m, and |m| = x∈S m(x) stands for its cardinality. We write ∅ for the empty multiset, i.e., supp(∅) = ∅. The union of m 1 , m 2 ∈ N S , written (m 1 ⊕ m 2 ), is defined such that (m 1 ⊕ m 2 )(x) = m 1 (x) + m 2 (x) for all x ∈ S. Note that ⊕ is associative and commutative, and has ∅ as identity. Hence, N S is the free commutative monoid S ⊕ over S. We write x for a singleton multiset, i.e., supp(x) = {x} and m(x) = 1. Moreover, we write x 1 . . . x n for x 1 ⊕ . . . ⊕ x n . Let f : S → S , we write f also for its obvious extension to multisets, i.e., f (x 0 . . . x n ) = f (x 0 ) . . . f (x n ). We avoid writing supp( ) when applying set operators to multisets, e.g., we write

x ∈ m or m 1 ∩ m 2 instead of x ∈ supp(m) or supp(m 1 ) ∩ supp(m 2 ). Definition 1 (Petri Net). A net N is a 4-tuple N = (S N , T N , • N , • N )
where S N ⊆ P is the (nonempty) set of places, T N ⊆ T is the set of transitions and the functions • N , • N : T N → 2 S N assign source and target to each transition such that • t = ∅ and t • = ∅ for all t ∈ T N . A marking of a net N is a multiset over S N , i.e., m ∈ N S . A Petri net is a pair (N, m) where N is a net and m is a marking of N .

We denote S N ∪T N by N , and omit the subscript N if no confusion arises. We abbreviate a transition t ∈ T with preset • t = s 1 and postset t • = s 2 as s 1 [ s 2 . Hereafter, we only consider nets whose transitions have non-empty presets. The pre and postset of a place a ∈ S are defined respectively as

• a = {t | a ∈ t • } and a • = {t | a ∈ • t}. We let • N = {x ∈ N | • x = ∅} and N • = {x ∈ N | x • = ∅}
denote the sets of initial and final elements of N respectively. Note that we only consider nets whose initial and final elements are places since transitions have non-empty pre and postsets, i.e., • t = ∅ and t • = ∅ holds for all t.

Definition 2 (Net morphisms). Let N, N be nets. A pair f = (f S :

S N → S N , f T : T N → T N ) is a net morphism from N to N (written f : N → N ) if f S ( • t N ) = • (f T (t)) N and f S (t • N ) = (f T (t))
• N for any t. Moreover, we say N and N are isomorphic if f is bijective.

The operational (interleaving) semantics of a Petri net is given by the least relation on Petri nets satisfying the following inference rule:

(firing) t = m [ m ∈ T N (N, m ⊕ m ) t - → (N, m ⊕ m )
which describes the evolution of the state of a net (represented by the marking m ⊕ m ) by the firing of a transition m[ m that consumes the tokens m in its preset and produces the tokens m in its postset. We sometimes omit t in t -→ when the fired transition is uninteresting.

According to Definition 1, transitions consume and produce at most one token in each place. On the other hand, p/t nets below fetch and consume multiple tokens by defining the pre-and postsets of transitions as multisets. • N : T N → N S N assign source and target to each transition. A marking of a net N is multiset over S N , i.e., m ∈ N S . A marked p/t net is a pair (N, m) where N is a p/t net and m is a marking of N .

The notions of pre-and postset, initial and final elements, morphisms and operational semantics are straightforwardly extended to p/t nets. Note that Petri nets can be regarded as a p/t net whose arcs have unary weights.

Next, we introduce some notation for sequences of transitions. Let ';' denote concatenation of such sequences. For the sequence s = t 1 ; t 2 ; . . . ; t n , we write

(N, m 0 ) s -→ (N, m n ) if (N, m 0 ) t1 -→ (N, m 1 ) t2 -→ . . . tn -→ (N, m n ); we call s a firing sequence. We write (N, m 0 ) - → * (N, m n ) if there exists s such that (N, m 0 ) s -→ (N, m n ),
| (N, m) - → * N, m )}.
We say a marked 2 shows different p/t nets, which will be used throughout the paper. As usual, places and transitions are represented by circles and boxes, respectively. The nets O 1 and N 4 are Petri nets, and N 1 , N 2 and N 3 are p/t nets which, when executing, may produce multiple tokens in some places.

p/t net (N, m) is (1-)safe if every reachable marking is a set, i.e., m ∈ reach(N, m) implies m ∈ 2 S N . • a • b t1 t2 c d (a) (O1, a ⊕ b) • a t1 • 1 1 b • | | 4 4 c • d t2 t3 e f (b) (N1, a ⊕ b ⊕ c ⊕ d) • a • b t1 1 1 t2 • 1 1 c d t3 e (c) (N2, a ⊕ b ⊕ c) • × × a t1 r r b (d) (N3, a) • a • b t1 B B • Q Q k k c t2 t t d e (e) (N4, a ⊕ b ⊕ c) Fig. 2. p/t nets Example 5. Figure

Unfolding of p/t nets

Our approach to reversing Petri nets relies on their occurrence net semantics, which explicitly exhibit the causal ordering, concurrency, and conflicts among events. We start by introducing several useful notions and notations. First, we shall describe a flow of causal dependencies in a net with the relation ≺:

Definition 6. Let ≺ be {(a, t)|a ∈ S N ∧ t ∈ a • } ∪ {(t, a)|a ∈ S N ∧ t ∈ • a}.
We write for the reflexive and transitive closure of ≺.

Consider Figure 2. We have a ≺ t 1 and t 1 ≺ c in O 1 as well as t 1 t 2 in N 1 .
Two transitions t 1 and t 2 are in an immediate conflict, written t 1 # 0 t 2 , when t 1 = t 2 and • t 1 ∩ • t 2 = ∅. For example, t 1 and t 2 in N 4 in Figure 2 are in an immediate conflict since they share a token in the place c. Correspondingly, for t 2 and t 3 in N 1 . The conflict relation # is defined by letting x#y if x = y and there are t 1 , t 2 ∈ T such that t 1 x, and t 2 y, and t 1 # 0 t 2 .

We are now ready to give the definition of an occurrence net following [START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF][START_REF] Hayman | The unfolding of general Petri nets[END_REF].

Definition 7 (Occurrence net). A net (N, m) is an occurrence net if 1. N is acyclic; 2.
N is a (1-)safe net, i.e, any reachable marking is a set; 3. m = • N , i.e., the initial marking is identified with the set of initial places; 4. there are no backward conflicts, i.e., | • a| ≤ 1 for all a in S N ; 5. there are no self-conflicts, i.e, ¬(t#t) for all t in T N .

We use O to range over occurrence nets.

Example 8. The net O 1 in Figure 2 is an occurrence net, while the remaining nets are not. N 1 is not an occurrence net since there is a token in place c and c is not an initial place of the net. N 2 has a backward conflict since two transitions produce tokens on the place d. N 3 is cyclic, and N 4 is cyclic and has a backward conflict on c.

The absence of backward conflicts in occurrence nets ensures that each place appears in the postset of at most one transition. Hence, pre-and postset relations can be interpreted as a causal dependency. So, represents causality.

We say x, y ∈ N are concurrent, written x co y, if x = y and x y, y x, and

¬x#y. A set X ⊆ N is concurrent, written CO(X), if ∀x, y ∈ X : x = y ⇒ x co y, and |{t ∈ T N | ∃x ∈ X, t x}| is finite. For example, the set {t 1 , t 2 } of firings in O 1 of Figure 2 is concurrent, so we can write CO({t 1 , t 2 }).
Two transitions are coinitial if they start with the same marking, and cofinal if they end up in the same marking. We now have a simple version of the Square Lemma [START_REF] Danos | Reversible communicating systems[END_REF] for forward concurrent transitions. It will be helpful in proving our Lemma 16 in the next section. Lemma 9. Let t and t be coinitial concurrent transitions. Then, there exist transitions t 1 and t 1 such that t; t 1 and t ; t 1 are cofinal.

The lemma says that if transitions t and t originate from one corner of a square, and if they represent independent (concurrent) events, then the square completes with two other independent transitions (t 1 and t 1 ) meeting at the opposite corner of the square. The order in which concurrent transitions are executed in a firing sequence does not matter. Indeed, the order which should be preserved among firings in a sequence is the causal order. We then consider sequences equivalent up to the swapping of concurrent transitions. This corresponds to considering the set of Mazurkiewicz traces induced by co as the independence relation.

Formally, trace equivalence ≡ is the least congruence over firing sequences s such that ∀t 1 , t 2 : t 1 co t 2 =⇒ t 1 ; t 2 ≡ t 2 ; t 1 . The equivalence classes of ≡ are the (Mazurkiewicz) traces. We use ω to range over such traces. We also will use for the empty trace, and ; for the concatenation operator.

For occurrence nets we have this standard property:

s 1 ≡ s 2 iff (O, m 0 ) s1 -→ (O, m n ) ⇐⇒ (O, m 0 ) s2 -→ (O, m n ) (1)
Two traces are coinitial if they start with the same marking, and cofinal if they end up in the same marking. Hence, equation (1) tells us that two traces that are coinitial and cofinal are then trace equivalent. The unfolding of a net N is the least occurrence net that can account for all the possible computations of N and makes explicit causal dependencies, conflicts and concurrency between firings [START_REF] Nielsen | Petri nets, event structures and domains, part I[END_REF].

(ini-mk) m(a) = n {a(∅, i) | 1 ≤ i ≤ n} ⊆ S (pre) H = {aj(hj, ij) | j ∈ J} ⊆ S Co(H) t ∈ TN • tN = ⊕j∈J aj t(H) ∈ T, • (t(H)) = H (post) x = t(H) ∈ T Q = {a({x}, i) | 1 ≤ i ≤ t • N (a)} ⊆ S, x • = Q Fig. 3. Unfolding rules. • a t1 • 5 5 b • { { 5 5 c { { 5 5 c • { { d t2 t2 t3 t3 e e f f (a) U[N1, a ⊕ b ⊕ c ⊕ d] • a • b t1 t2 d • | | 4 4 c d t3 t3 e e (b) U[N2, a ⊕ b ⊕ c] • a t1 | | b a t1 | | b a . . . (c) U[N3, a]
Definition 10 (Unfolding). Let (N, m) be a p/t net. The unfolding of N is the occurrence net U[N, m] = (S, T, δ 0 , δ 1 ) generated inductively by the inference rules in Figure 3 and the folding morphism

(f S , f T ) : U[N, m] → N defined such that f S (a, , ) = a and f T (t, ) = t.
Places are named by triples a(H, i) where: a is a place of N where tokens reside; H is the set of immediate causes (i.e., the history of tokens); and i is a positive integer used to disambiguate tokens with the same history. Transitions (or events) are encoded as t(H), where H is as above and t is the fired transition. After the transitions t 1 and t 2 have fired, there is a token in each of the places labelled d. The token in the leftmost d has the history t 1 and the token in the other d has the history t 2 . Once t 3 has fired, we can tell the copies of t 3 apart by inspecting their histories: the leftmost t 3 is caused by a token in d with the history t 1 (as well as the token in c), whereas the other t 3 is caused by d with the history t 2 and by c.

- → O = (S - → O , T - → O , • - → O , • - → O ) defined such that S - → O = S O T - → O = T O ∪ { - → t | t ∈ T O } • t - → O = • t O if t ∈ T O t • O otherwise t • - → O = t • O if t ∈ T O • t
( - → O , m) - → t ( - → O , m ) if ( - → O , m ) t ( - → O , m) ( - → O , m) - → t ( - → O , m ) if ( - → O , m ) t ( - → O , m)
Hence, we have -→ -→ t = t. We shall work with sequences of transitions and reverse transitions, ranged over by s, s 1 and s 2 . We say that a sequence is a forward (resp. backward) sequence when all its firings are forward (resp. backward).

Next, we extend the notions of causality, conflict and concurrency to transitions and reverse transitions in reverse versions of occurrence nets. We extend ≺ in Definition 6 to cover reverse transitions in an obvious way using Definition 12. As a result, we obtain t -→ t and -→ t t. As for the conflict relation, we define an immediate conflict between different

- → t 1 and - → t 2 as • - → t 1 ∩ • - → t 2 = ∅. This is t 1 • ∩ t 2 • = ∅,
t - → (O, m ) iff ( - → O , m) t ( - → O , m ).
In general, a reversible occurrence net is not an occurrence net. This is because adding reverse transitions may introduce backward conflict for these transitions. Consider N 1 in Figure 2. We notice that initially t 1 and t 2 are in conflict. Then, in -→ N 1 in Figure 5, the place c with a token has two reverse transitions in its preset, namely -→ t 2 and -→ t 3 , hence there is a backward conflict.

Properties

We now study the properties of the reversible versions of occurrence nets.

An important property of a fully reversible system is the Loop Lemma stating that any reduction can be undone. Formally:

Lemma 14 (Loop Lemma). ( - → O , m) t ( - → O , m ) iff ( - → O , m ) - → t ( - → O , m).
We can generalise the result of the Loop Lemma to sequences as follows:

Corollary 15. ( - → O , m) - → * ( - → O , m ) iff ( - → O , m ) - → * ( - → O , m).
Next, we have a lemma which is instrumental for the proof of causal-consistent reversibility in reversible calculi [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF]. Note that t and t can be either forward or reverse transitions.

Lemma 16 (Square Lemma). Let t and t be coinitial concurrent transitions. Then, there exist transitions t 1 and t 1 such that t; t 1 and t ; t 1 are cofinal.

In order to prove causal consistency we first define a notion of equivalence on sequences of transitions and reverse transitions in reversible occurrence nets. By following Lévy's approach [START_REF] Lévy | An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus[END_REF], we define the notion of reverse equivalence on such sequences as the least equivalence relation which is closed under composition with ; such that the following hold (recall that t, t are transitions or reverse transitions):

t; t t ; t if t co t t; - → t - → t ; t
Reversible equivalence allows us to swap the order of t and t in an execution sequence as long as t, t are concurrent. Moreover, it allows cancellation of a transition and its inverse. We have that ≡⊂ . The equivalence classes of are called traces; it is clear that they contain the Mazurkiewicz traces. Hence, we shall use ω, ω 1 and ω 2 to range over such traces.

The following lemma says that, up to reverse equivalence, one can always reach for the maximum freedom of choice, going backward, and only then going forwards.

Lemma 17 (Parabolic Lemma). Let ω be a trace. There exist two forward traces ω 1 and ω 2 such that ω -→ ω 1 ; ω 2 .

Proof. By lexicographic induction on length of ω and on the distance between the beginning of ω and the earliest pair of opposing firings in ω. The analysis uses both the Loop Lemma (Lemma 14) and the Square Lemma ( Lemma 16).

The following lemma says that, if two traces ω 1 and ω 2 are coinitial and cofinal (e.g. they start from the same marking and end in the same marking) and ω 2 is a forward only trace, then ω 1 has some forward firings and their reverse ones that cancel each other. And this implies that ω 1 is causally equivalent to a forward trace in which all those pairs of fairing are cancelled out.

Lemma 18 (Shortening Lemma). Let ω 1 ω 2 with ω 2 forward. Then,

|ω 2 | ≤ |ω 1 |.
Proof. The proof is by induction on length of ω 1 , using Lemma 16 and Lemma 17. In the proof, the forward trace ω 2 is the main guideline for shortening ω 1 into a forward trace. Indeed, the proof relies crucially on the fact that ω 1 and ω 2 share the same source and target and that ω 2 is a forward trace.

Theorem 19 (Causal Consistency). Two traces ω 1 and ω 2 are reversible equivalent iff they are coinitial and cofinal, namely

ω 1 ω 2 iff ( - → O , m 0 ) ω1 -→ ( - → O , m n ) ⇐⇒ ( - → O , m 0 ) ω2 -→ ( - → O , m n ).
Proof. The "if" direction follows by definition of reverse equivalence and trace composition. The "only if" direction exploits the properties the Square, Parabolic and Shortening Lemmas.

With Theorem 19 we proved that the notion of causal consistency characterises a space for admissible rollbacks which are: (1) consistent (in the sense that they do not lead to previously unreachable configurations) and ( 2) flexible enough to allow rearranging of undo actions. This implies that starting from an initial marking, all the markings reached by mixed computations are markings that could be reached by performing only forward computations. Hence, we have: Theorem 20. Let O be an occurrence net and m 0 an initial marking. Then,

( - → O , m 0 ) - → * ( - → O , m ) ⇐⇒ ( - → O , m 0 ) * ( - → O , m ). • X X a - → t2 @ @ - → t2 v v - → t1 d d t1 - → t3 v v • @ @ b • v v A A c u u @ @ c • v v d t2 t2 t3 t3 c c c c e f f - → t3 h h (a) ( - → N1, a ⊕ b ⊕ c ⊕ d) • a - → t1 X X t1 z z y y b d d a - → t1 X X t1 z z y y b d d a . . . W W . . . (b) ( - → N3, a) • a • b - → t1 X X d d t1 t2 - → t2 d d X X d • | | 4 4 c d t3 t3 e e - → t3 x x f f - → t3 (c) ( - → N2, a ⊕ b ⊕ c) • a • b t1 - → t1 k k t2 - → t2 k k h h c h h d (d) (O1, a ⊕ b)
- - - → (N, m), is - - - - - → U[N, m].
Example 22. The reversible version of the nets in Figure 2 are shown in Figure 5.

We remark that they are the reversible versions of the nets in Figure 4, which are the unfoldings of the original nets.

The following result states that a reversible net is a conservative extension of its original version, i.e., reversibility does not change the set of reachable markings. The result is a direct consequence of Lemma 13 and the fact that unfoldings preserve reductions up-to the folding morphism U.

Lemma 23. (N, m) - → * (N, m ) iff - - - - → (N, m) * ( - → O , m ) and m = f s (m )
, where (f s , f t ) : U[N, m] → N , defined such that f S (a, , ) = a and f T (t, ) = t, is the folding morphism.

We remark that the reversible version of a p/t is defined as the reversible version of an occurrence net (i.e., its unfolding). Consequently, all properties shown in the previous section apply to the reversible semantics of p/t nets. In particular, Lemma 23 combined with Theorem 20 ensures that all markings reachable by the reversible semantics are just the reachable markings of the original P/T net.

Finite Representation of Reversible p/t Nets

As shown in Figure 5(c), the reversible version of a finite net may be infinite. In this we show how to represent reversible nets in a compact, finite way by using coloured Petri nets. We assume infinite sets X of variables and C of colours, defined such that X ⊂ C. For c ∈ C, we write vars(c) for the set of variables in c. With abuse of notation we write vars(m) for the set of variables in a multiset m ∈ N P×C . Let σ : X → C be a partial function and c a colour (also, m ∈ N P×C ), we write cσ (resp., mσ) for the simultaneous substitution of each variable x in c (resp., m) by σ(x).

Definition 24 (c-p/t net). A coloured place / transition net ( c-p/t net) is a 4-tuple N = (S N , T N , • N , • N ) where S N ⊆ P is the (nonempty) set of places, T N ⊆ T is the set of transitions and the functions • N , • N : T N → N S N ×C assign source and target to each transition defined such that vars(t • ) ⊆ vars( • t). A marking of a c-p/t net N is multiset over S N × C that does not contain variables, i.e., m ∈ N S×C and vars(m) = ∅. A marked c-p/t net is a pair (N, m) where N is a p/t net and m is a marking of N . c-p/t nets generalise p/t nets by extending markings to multisets of coloured tokens, and transitions to patterns that need to be instantiated with appropriate colours for firing, as formally stated by the firing rule below.

(coloured-firing) t = m [ m ∈ T N (N, mσ ⊕ m ) t - → (N, m σ ⊕ m )
The firing of a transition t = m [ m requires to instantiate m and m by substituting variables by colours, i.e., the firing of t consumes the instance mσ of the preset m and produces the instance m σ of the postset of m .

We now introduce an encoding that associates each p/t net N with an equivalent c-p/t net N , whose tokens carry their execution history. We rely on the set of colours C defined as the least set that contains X and it is closed under the following rules.

(token) h ∈ 2 C n ∈ N (h, n) ∈ C (elem) x ∈ T ∪ P h ∈ 2 C x(h) ∈ C
Colours resemble the unfolding construction (Figure 3): the colours for tokens are (h, n), where h denotes its (possible empty) set of causes and n is a natural number used for distinguishing tokens with identical causal history. Causal histories are build from coloured versions of transitions (t(h)) and places (a(h)).

Definition 25 (P/T as C-P/T). Let N = (S N , T N , • N , • N ) be a p/t net. Then, N is the c-p/t defined such that N = (S N , T N , • N , • N ) and

-• t N = a 1 (x 1 ) ⊕ . . . ⊕ a n (x n ) where • t N = a 1 . . . a n and ∀1 ≤ i ≤ n.x i ∈ X . -t • N = {a({t(h)}, i) | a ∈ supp(t • N ) ∧ 1 ≤ i ≤ t • N (a) ∧ h = • t N }. A marked net (N, m) is encoded as (N, m) = ( N , m ) where m = {a(∅, i) | a ∈ supp(m) ∧ 1 ≤ i ≤ m(a)}.
The encoding does not alter the structure of a net; it only adds colours to its tokens. In fact, an encoded net has the same places and transitions as the original net, and pre-and postsets of each transition have the same support. Added colours do not interfere with firing because the preset of each transition uses different colour variables for different tokens. The colour {t(h)} assigned to each token produced by the firing of t describes the causal history of the token, i.e., it indicates that the token has been produced by t after consuming the tokens in the preset of t, which is denoted by h. The natural number i is used for distinguishing multiple tokens produced by the same firing. Tokens in the initial marking are coloured as (∅, i), i.e., they have empty causal history.

Example 26. The encoding of the nets in Figure 2 are shown in Figure 6. We comment on the encoding of N 1 . The transition t 1 = a[ c in N 1 is encoded as a(x)[ c(t 1 (a(x)), 1), i.e., the firing of t 1 that consumes a token with colour h from place a generates a token in c with colour (t 1 (a(h)), 1). The transition t 2 = b ⊕ c[ e has two places in the preset and uses two variables x and y in its encoded form b(x) ⊕ c(y)[ e(t 2 (b(x) ⊕ c(y)), 1). Note that the colour of the token produced in c carries the information of the tokens consumed from both places b and c. The encoding for t 3 is defined analogously.

We illustrate a sequence of firings of (N

1 , a ⊕ b ⊕ c ⊕ d) . ( N 1 , a(∅, 1) ⊕ b(∅, 1) ⊕ c(∅, 1) ⊕ d(∅, 1)) t1 -→( N 1 , b(∅, 1) ⊕ c(t 1 (a(∅, 1)), 1) ⊕ c(∅, 1) ⊕ d(∅, 1)) t2 -→( N 1 , e(t 2 (b(∅, 1) ⊕ c(t 1 (a(∅, 1)), 1)), 1) ⊕ c(∅, 1) ⊕ d(∅, 1
))

The firing of t 1 consumes the token (∅, 1) from a and produces the token (t 1 (a (∅, 1)), 1) in place c. The causal history of the token t 1 (a(∅, 1) indicates that the token has been produced by the firing of t 1 that consumed the token (∅, 1) from a. The second reduction takes place because of the firing of t 2 . By inspecting the causal history of the token produced in the place e we can conclude that t 2 has consumed the token previously generated by t 1 .

The following result shows that there is a tight correspondence between the semantics of the coloured version of a p/t net and its unfolding.

(∅,1)

x a t1 (t 1 (a(x)),1) 6, is shown in Figure 7. We now illustrate the execution of -→ N 2 . In the example above, the firing t 2 can choose to consume either the token b(∅, 1) or the token b(t 1 (a(∅, 1)), 1). Since the first one is chosen, then after t 2 it is still possible to undo t 1 . If t 2 chose the second token, then in order to undo t 1 we would first undo t 2 , since firing -→ t 1 is not enabled by the token a(∅, 1).

(∅,1) x $ $ b (∅,1) y Ó Ó x ' ' c (∅,1) y Ö Ö d t2 (t 2 (b(x)⊕c(y)),1) t3 (t 3 (c(x)⊕d(y)),1) e f (a) N1 (∅,1) x a (∅,1) x b t1 (t 1 (a(x)),1) & & t2 (t 2 (b(x)),1) Ô Ô (∅,1) x & & c y Ô Ô d t3 (te(c(x)⊕d(y)),1) e (b) N2 (∅,1) x × × a t1 (t 1 (a(x)),1) (t 1 (a(x)),1) r r b (c) N3
-→ ( N , m ) iff (O, m) s -→ (O, m ). If ) ( N , m ) t - → ( N , m ) implies m = • t N ⊕ m and m = t • N ⊕ m . Since (O, m) s -→ (O, m ), CO( • t).
( - → N2 , a(∅, 1) ⊕ b(∅, 1) ⊕ c(∅, 1) ⊕ d(∅, 1))
The following result states that the reductions of the reversible c-p/t of a net are in one-to-one correspondence with the reductions of its reversible unfolding.

Conclusions

We have presented a causally reversible semantics for Place/Transitions Petri Nets (P/T nets) based on two observations. First, occurrence net can be straightforwardly reversed by adding for each transition its reverse. Second, the standard unfolding construction associates a P/T net with an occurrence net that preserves all of its computation. Consequently, the reversible semantics of a P/T net can be obtained as the reversible semantics of its unfolding. We have showed that reversibility in reversible occurrence net is causal-consistent, that is it preserves causality. The unfolding of an occurrence net can be infinite (e.g., it the original P/T net is not acyclic). Therefore we have shown that the reversible behaviour of reversible occurrence nets can be expressed as a finite net whose tokens are coloured by causal histories. Colours in our encoding resemble the causal memories that are typical in reversible process calculi [START_REF] Lanese | Reversibility in the higher-order π-calculus[END_REF][START_REF] Danos | Reversible communicating systems[END_REF].

Occurrence nets have a direct mapping into prime event structures. We shall investigate in the future the relation between reversible event structures [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF][START_REF] Cristescu | Rigid families for CCS and the π-calculus[END_REF][START_REF] Ulidowski | Reversing event structures[END_REF][START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF] and our reversible occurrence nets. There is an alternative method for proving causally-consistent reversibility in a reversible model of computation. It is based on showing other properties than those in Section 4, mainly the well-foundedness (lack of infinite reverse sequences) and Reverse Diamond properties [START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Phillips | Reversibility and models for concurrency[END_REF]. It would be worthwhile to prove the alternative properties for our reversible nets, and compare the two approaches.

Fig. 1 .

 1 Fig. 1. Backward conflict and naive reversing.

Definition 3 (

 3 p/t net). A Place / Transition Petri net ( p/t net) is a 4-tuple N = (S N , T N , • N , • N ) where S N ⊆ P is the (nonempty) set of places, T N ⊆ T is the set of transitions and the functions • N ,

  and m for the empty sequence.

Definition 4 .

 4 Let (N, m) be a p/t net. The set of reachable markings reach(N, m) is defined as m

Fig. 4 .

 4 Fig. 4. Unfoldings of p/t nets

Example 11 .

 11 The unfoldings of the nets (N 1 , a ⊕ b ⊕ c ⊕ d), (N 2 , a ⊕ b ⊕ c) and (N 3 , a) in Figure 2 are shown in Figure 4. Note that since O 1 is an occurrence net its unfolding is isomorphic to O 1 , thus it is omitted. Consider the occurrence net U[N 1 , a ⊕ b ⊕ c ⊕ d]. The leftmost transition t 2 is different from the other transition t 2 since they have different histories: the leftmost t 2 is caused by the tokens in b and c (which are available in the initial marking), whereas the other t 2 is caused only by the token in b and the token that is produced by the firing of t 1 . Correspondingly, for the two transitions labelled t 3 . Consider U[N 2 , a ⊕ b ⊕ c].

3

  Reversing Occurrence Nets Definition 12. Let O be an occurrence net. The reversible version of O is

Fig. 5 .

 5 Fig. 5. Reversible p/t and Petri nets

Fig. 6 .

 6 Fig. 6. p/t nets as c-p/t nets

1 ) 1 ) 1 )Fig. 7 .

 1117 Fig. 7. Reversible coloured net -→ N2 .

Theorem 30 (

 30 Correctness). Let (N, m) be a marked p/t net and U[N, m] = (O, m ) its unfolding. Then,

  in Figure5reverse (or backwards) transitions (or firings), and use t, t 1 and t 2 to denote transitions or reverse transitions.

	Given a transition t we write transitions like -→ t 1 and -→ t 2 For -→ O , we write ( -→ O , m) ( -→ O , m)	t	-→ t for a transition that reverses t. We shall call ( -→ O , m ) for a forward firing when t ∈ T O , and
	firing t we indicate with	-→ t its inverse that is	-→ O , m)	t -→ (	-→ O , m ) as t. Given a

O otherwise t ( -→ O , m ) for the reverse (or backward) firing when t ∈ T O . We also let t -→ be t ∪

t . We will often refer to a firing (

  meaning t 1 and t 2 are in backward conflict, which is ruled out in occurrence nets. Hence, the immediate conflict relation is empty between reverse transitions, and so is the conflict relation. The immediate conflict relation be-

	tween t and means t	-→ t is defined as • t ∩ • -→ t = ∅. This is equivalent to • t ∩ t t. Consequently, the conflict relation on transitions in • = ∅, which -→ O is given
	by the conflict relation on the forward transitions, and can be defined using the
	causality relation for pairs of a transition and reverse transition. This allows us to define concurrent transitions in -→ O . We say t co t if (a) t co t for t, t ∈ T O , (b) t t and t t if t, t are reverse transitions, and (c) t t , t t and -→ t t
	if t is a transition and t is a reverse transition. Next, we show that -→ O is a conservative extension of O.
	Lemma 13. (O, m)

  The only if follows analogously.The reversible version of N is defined as for occurrence nets, by adding transitions that are the swapped versions of the ones in N . , the reversible version of N 2 from Figure

	Definition 28 (Reversible P/T net). Let N be a p/t net. The reversible version of N is --→ N . The reversible version of a marked p/t net (N, m) is the marked c-p/t net ( --→ N , m ).
	Example 29. The net	-→ N 2

Then, by the unfolding construction we conclude (O, m ) t -→ (O, m ).

Acknowledgment Research partly supported by the EU H2020 RISE programme under the Marie Sk lodowska Curie grant agreement No 778233. Partly supported by UBACyT projects 20020170100544BA and 20020170100086BA, and CONICET project PIP 11220130100148CO. Also, we thank COST Action IC1405 on Reversible Computation for partial support. The second author acknowledges the support of the Marie Sk lodowska Curie Action Individual Fellowship RCADE No 794405.