=Paper=
{{Paper
|id=Vol-1698/CS&P2016_08_Barylska&Mikulski&Piatkowski&Koutny&Erofeev_Reversing-Transitions-in-Bounded-Petri-Nets
|storemode=property
|title=Reversing Transitions in Bounded Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-1698/CS&P2016_08_Barylska&Mikulski&Piatkowski&Koutny&Erofeev_Reversing-Transitions-in-Bounded-Petri-Nets.pdf
|volume=Vol-1698
|authors=Kamila Barylska,Lukasz Mikulski,Marcin Piatkowski,Maciej Koutny,Evgeny Erofeev
|dblpUrl=https://dblp.org/rec/conf/csp/BarylskaMPKE16
}}
==Reversing Transitions in Bounded Petri Nets==
https://ceur-ws.org/Vol-1698/CS&P2016_08_Barylska&Mikulski&Piatkowski&Koutny&Erofeev_Reversing-Transitions-in-Bounded-Petri-Nets.pdf
Reversing Transitions in Bounded Petri Nets?
Kamila Barylska1 , Evgeny Erofeev2 , Maciej Koutny3 ,
Łukasz Mikulski1 , and Marcin Piątkowski1
1
Faculty of Mathematics and Computer Science,
Nicolaus Copernicus University
Toruń, Chopina 12/18, Poland
{kamila.barylska,lukasz.mikulski,marcin.piatkowski}@mat.umk.pl
2
Parallel Systems, Department of Computing Science
Carl von Ossietzky Universität
D-26111 Oldenburg, Germany
evgeny.erofeev@informatik.uni-oldenburg.de
3
School of Computing Science
Newcastle University
Newcastle upon Tyne, NE1 7RU, United Kingdom
maciej.koutny@newcastle.ac.uk
Abstract. Reversible computation deals with mechanisms for undoing
the effects of actions executed by a dynamic system. This paper is con-
cerned with reversibility in the context of Petri nets which are a general
formal model of concurrent systems. A key construction we investigate
amounts to adding ‘reverse’ versions of selected net transitions. Such
a static modification can severely impact on the behaviour of the sys-
tem, e.g., the problem of establishing whether the modified net has the
same states as the original one is undecidable. We therefore concentrate
on nets with finite state spaces and show, in particular, that every tran-
sition in such nets can be reversed using a suitable set of new transitions.
Keywords: Petri net, reversibility, reversible computation
1 Introduction
Reversible computation deals with (typically local) mechanisms for undoing the
effects of actions executed by a dynamic system. Such an approach has been
applied, in particular, to various kinds of process calculi and event structures
(see, e.g., [3–6, 8, 11, 12, 10]), and to a category theory based setting [7].
?
This research has been partially supported by the Polish
grant No.2013/09/D/ST6/03928, and by the EU COST Action IC1405, and
by DFG (German Research Foundation) through grant Be 1267/14-1 CAVER (Design
and Analysis Methods for Real-Time Systems) and Graduiertenkolleg GRK-1765
SCARE (System Correctness under Adverse Conditions).
This paper is concerned with reversibility in the context of Petri nets which are
a general formal model of concurrent systems. A key construction we investigate
amounts to adding ‘reverse’ versions of selected net transitions, e.g., a ‘straight-
forward’ reverse simply changes the directions of arcs adjacent to a transition
being reversed. As shown in [2], such a static modification can severely impact
on the behaviour of the system, e.g., the problem of establishing whether the
modified net has the same states as the original one is undecidable.
We therefore concentrate in this paper on Petri nets with finite state spaces,
more precisely bounded Place/Transition-nets (PT-nets). The state spaces of
such nets can be represented by finite labelled transition systems (flts’s) which
are a convenient tool for specifying different variants of reversibility. One can
therefore aim at synthesising a PT-net with ‘reversed’ behaviour given by an
flts.
In this paper we show that it is, in general, impossible to reverse a transition
using its straightforward reverse. What is more, the situation does not change if
we relax the notion of a reverse by only requiring that the effect of its execution
is opposite to that of the original transition. We therefore relax the requirement
further, by allowing several reverses for a single transition. This leads to our
main result that every transition in a bounded PT-net can be reversed using
a suitable set of new transitions.
2 Preliminaries
Transition systems
A finite labelled transition system (or, simply, flts) is a tuple T S = (S, T, →, s0 )
with a finite set of states S, a finite set of labels T , a finite set of arcs → ⊆
(S × T × S), and an initial state s0 ∈ S.4 A label t is fireable at s ∈ S, denoted
by s[ti, if (s, t, s0 ) ∈ →, for some s0 ∈ S. A state s0 is reachable from s through
the execution of σ ∈ T ∗ , denoted by s[σis0 , if there is a directed path from s to
s0 whose arcs are labelled consecutively by σ. The set of states reachable from s
is denoted by [si. A sequence σ ∈ T ∗ is fireable, from a state s, denoted by s[σi,
if there is some state s0 such that s[σis0 .
Let t•T S = {s ∈ S | (s0 , t, s) ∈→, for some s0 ∈ S} and • tT S = {s ∈ S |
(s, t, s0 ) ∈→, for some s0 ∈ S} be respectively the sets of all states having an
incoming arc labeled with t, and an outgoing arc labeled with t. The set of all
→
− →
−
arcs labelled by t is denoted by t . We assume that each t is nonempty.
Two flts’s, T S1 = (S1 , T, →1 , s01 ) and T S2 = (S2 , T, →2 , s02 ), are isomorphic
if there is a bijection ζ : S1 → S2 with ζ(s01 ) = s02 and (s, t, s0 ) ∈ →1 ⇔
(ζ(s), t, ζ(s0 )) ∈ →2 , for all s, s0 ∈ S1 .
Petri nets
A Place/Transition Petri net (or, simply, net) is a tuple N = (P, T, F, M0 ),
4
An flts may be considered as a finite automaton with no accepting states.
where P is a finite set of places, T is a finite set of transitions (or actions), F is
the flow function F : ((P × T ) ∪ (T × P )) → N specifying the arc weights, and
M0 is the initial marking (where a marking is a mapping M : P → N, indicating
the number of tokens in each place). A transition t ∈ T is enabled at a marking
M , denoted by M [ti, if M (p) ≥ F (p, t), for all p ∈ P . The effect of a transition t
on a place p is eff p (t) = F (t, p) − F (p, t). The firing of t at marking M leads
to M 0 , denoted by M [tiM 0 , if M [ti and M 0 (p) = M (p) + eff p (t) for every p ∈ P .
The notions of enabledness and firing, M [σi and M [σiM 0 , are extended in the
usual way to sequences σ ∈ T ∗ , and [M i denotes the set of all markings reachable
from M . We assume that each transition is enabled in at least one reachable
marking. There is a partial order relation < on the markings of a Petri net defined
so that M ≤ M 0 if M (p) ≤ M 0 (p), for every place p ∈ P . It is easy to observe
that transition enabledness is monotonic, which means that if a transition t is
enabled at a marking M and M ≤ M 0 , then t is also enabled at M 0 .
A Petri net N = (P, T, F, M0 ) net is bounded if [M0 i is finite, and its reachability
graph is then defined as an flts
RG(N ) = ([M0 i, T, {(M, t, M 0 ) | M, M 0 ∈ [M0 i ∧ M [tiM 0 }, M0 ).
If a labelled transition system T S is isomorphic to the reachability graph of
a Petri net N , then we say that N solves T S, and T S is synthesisable to N .
Definition 1 (transition reverse). A (strict) reverse of a transition t ∈ T in
a net N = (P, T, F, M0 ) is a new transition t such that F (p, t) = F (t, p) and
F (t, p) = F (p, t). An effect-reverse of a transition t ∈ T is a new transition t
such that eff p (t) = −eff p (t), for all places p ∈ P .
To improve readability, we depict newly created reverses and adjacent arcs by
dashed (or dotted) lines. Clearly, for a given transition t, its strict reverse t is
unique and, at the same time, it is an effect-reverse of t. However, an effect-
reverse t is not necessarily a strict reverse (see Figure 1).
• •
a • a a • a
2 2 2 2
Fig. 1. A transition a and its (strict) reverse a (lhs), and an effect-reverse a, which is
not a strict reverse (rhs).
(Un)solvable words
A word w = t1 t2 . . . tn of length n ∈ N uniquely corresponds to a labelled
transition system T S(w) = ({0, . . . , n}, T, {(i − 1, ti , i) | 0 < i ≤ n ∧ ti ∈ T }, 0).
We say that a net N solves a word w if it solves T S(w). A word w is then called
solvable, and otherwise unsolvable.
If a word w is solvable, then so are all its factors (where a factor w0 satisfies
w = vw0 u, for some v and u). Thus, the unsolvability of any proper factor of w
entails the unsolvability of w. For this reason, the notion of a minimal unsolvable
word, defined as an unsolvable word with all proper factors being solvable, is
well-defined (see [1] for details).
The mirror image wR of a word w is w written from right to left.
3 Solvability of flts’s with reverses
We now define reverses for labelled transition systems, and investigate how they
affect the solvability of the resulting flts’s. We first introduce the notions of
reduction and extension of an flts.
Definition 2 (flts reduction and extension). Let T S = (S, T, →, s0 ) be
a solvable flts.
– The reduction of T S by deleting t ∈ T is an flts T S [−t] = (S 0 , T \ {t}, →0 , s0 )
such that:
→
−
• S 0 ⊆ S are all the states reachable in T S without using t ;
• (s1 , a, s2 ) ∈→0 if (s1 , a, s2 ) ∈→, for all a 6= t and s1 , s2 ∈ S 0 .
– The extension of T S by reversing t ∈ T is an flts T S [+t] = (S, T ∪{t}, →0 , s0 )
such that, for all s1 , s2 ∈ S:
• (s1 , a, s2 ) ∈→0 if (s1 , a, s2 ) ∈→, for all a ∈ T ;
• (s1 , t, s2 ) ∈→0 if (s2 , t, s1 ) ∈→.
These above notions can be extended to finite sets of transitions, by setting
T S [−t1 ,t2 ...tn ] = T S [−t1 ][−t2 ]...[−tn ] and T S [+t1 ,t2 ...tn ] = T S [+t1 ][+t2 ]...[+tn ] .
N1 : p4
• T S0 : T S1 : T S2 :
••
b
•• b b
p2 b
b b b b b b b b
a a b
p1 2 b a b b a b a a a
b
3 a b a b a b
p3
[+a]
Fig. 2. T S0 and T S2 = T S0 are solvable by net N1 (respectively without and with
[+b]
the dashed part), while T S1 = T S0 is unsolvable.
Consider a word w = bbbabab which, in Figure 2, corresponds to a solvable flts
T S0 . If we add a reverse of transition a, we obtain T S2 which is solvable by N1 .
We will later show that reversing transition b leads to an unsolvable flts T S1 .
The a in Figure 2 is an effect-reverse but not a strict reverse of a. We will now
show that if a label a can be effect-reversed, i.e., T S [+a] is solvable, then there
exists a solution in which transition a is a strict reverse of a.
Proposition 1. Let T S = (S, T, →, s0 ) be a solvable flts and a ∈ T . If T S [+a]
is solvable then there exists its solution such that a is a strict reverse of a.
N2 : T S3 : T S4 :
3
2 p1 2 b b
b b b b
a b b
p2 b a b b b a
•• a b a b
[+b]
Fig. 3. Adding a reverse b in T S4 = T S3 does not violate solvability.
Consider N2 of Figure 3 without the dashed part. It solves the word bbabab, and
so its reachability graph is isomorphic to T S3 . Unlike the case with the reverse of
b in T S1 , T S4 obtained from T S3 by adding a reverse for transition b is solvable
by N2 with dashed part. Note that, in N2 , b is a strict reverse of b.
Similarly, we may reverse a in T S3 , obtaining T S5 of Figure 4. This flts is solvable
by the net N3 with the dashed part.
p1
N3 : •• T S5 :
p2
b b
a p3 a b
•• b a a a
2 a b
2
p4
[+a]
Fig. 4. T S5 = T S3 is solvable (e.g. by N3 ).
The next result states that for a given flts and two of its transitions, if adding
a reverse for each of them separately yields solvable flts’s, then the flts with both
reverses is also solvable.
Proposition 2. Let T S = (S, T, →, s0 ) be a solvable flts and a 6= b ∈ T . If both
T S [+a] and T S [+b] are solvable, then so is T S [+a,b] .
For T S = T S3 of Figure 3, by Proposition 2, starting from the solutions for
T S4 = T S [+a] and T S5 = T S [+b] , we can construct a solution N4 for T S6 =
T S [+a,b] depicted in Figure 5.
3
p1
•• T S6 :
p2 3
2 p5 2 b b b b
a p3 a b b
•• p6 b b b a a
a
2 ••
b
2 a
p4
N4 :
3
[+a,b]
Fig. 5. N4 solving T S6 = T S3 derived by synchronising the transitions
of N2 and N3 .
We end this section looking at the solvability of words over a two-letter alphabet.
Proposition 3. Let w ∈ {a, b}∗ be a minimal unsolvable word. Then T S(wR )
is solvable.
Due to Propositions 2 and 3, reversing of both transitions in the mirror image
wR of some minimal unsolvable word w over {a, b} yields solvability of w, which
is a contradiction. Hence, the following corollary holds
Corollary 1. Let w ∈ {a, b}∗ be a minimal unsolvable word and T S = T S(wR ).
Then T S [+a] or T S [+b] is unsolvable.
The above result explains why b in T S1 of Figure 2 cannot be reversed. All we
need to observe is that w = bbbabab is the mirror image of a minimal unsolvable
word bababbb, and then recall that a can be reversed in T S1 .
4 Splitting reverses
In this section we discuss the possibility of "splitting" reverses. More specifically,
we investigate flts’s in which more than one reverse to a given transition can exist.
Consider N5 of Figure 6, together with its reachability graph T S7 . First, we
observe that eff b1 (p) = eff b2 (p) = −eff b (p), for every place p. Hence, transitions
b1 and b2 are both effect-reverses for b. We have already seen that it is impossible
to synthesise an flts with just one reverse of b (i.e., T S1 of Figure 2), but the
behaviour of N5 is exactly what one might indeed want to obtain. The only
difference is that N5 has more than one reverse for b. In what follows, we show
that every action of a bounded net can be reversed using finitely many effect-
reverses.
p3
•
N5 : ••
2 T S7 : [2, 0, 3] [0, 3, 0]
b1 b2 b
2 b
2 b1
[2.1.2] [0, 2, 1]
a 3 b b2 b a
3 p2
[2, 2, 1] [1, 3, 0]
p1 b2 b2
2 b b
•• b1
2 [2, 3, 0]
a
[1, 2, 1]
Fig. 6. Splitting reverses in T S7 results in solvability.
Definition 3 (splitting reverse). Let T S = (S, T, →, s0 ) be a solvable flts.
The extension of T S by a set T of reverses of t ∈ T is an flts T S [+tφ] =
(S, T 0 , →0 , s0 ) such that:
→
−
– φ : t → 2T \ {∅} is a mapping specifying all possible ways in which each of
t-labelled arcs can be reversed;
– T0 = T ∪ T;
– (s1 , a, s2 ) ∈→0 if (s1 , a, s2 ) ∈→, for any a ∈ T ;
– (s1 , t0 , s2 ) ∈→0 if (s2 , t, s1 ) ∈→ and t0 ∈ φ((s1 , t, s2 )).
We also extend the above notion in the usual way to T S [+t1 φ1 ,t2 φ2 ,...,tn φn ] .
Lemma 1. Let N = (P, T, F, M0 ) be a bounded net, T S = ([M0 i, T, →, M0 )
be its reachability graph, and t ∈
/ T be a new transition symbol. If a reachable
marking M is ≤-maximal in [M0 i and M 0 ∈ [M0 i, then
T S 0 = ([M0 i, T ∪ {t}, → ∪{(M, t, M 0 )}, M0 )
is a solvable flts.
Proof. Let N 0 = (P, T ∪ {t}, F 0 , M0 ), where:
F 0 (p, a) = F (p, a) for all p ∈ P and a ∈ T
F 0 (a, p) = F (a, p) for all p ∈ P and a ∈ T
F 0 (p, t) = M (p) for every p ∈ P
F 0 (t, p) = M 0 (p) for every p ∈ P .
We then obtain that:
(1) t is not enabled at any marking M 00 6= M reachable in N . Indeed, suppose
that there exists such a marking M 00 . Then, by the definition of enabled-
ness, M 00 (p) ≥ F 0 (p, t) = M (p), for every p ∈ P . Hence M 00 ≥ M , which
contradicts the ≤-maximality of M .
(2) M [tiM 0 . This follows directly from the definition of F 0 .
We then observe that, by (1) and (2), the sets of reachable markings of the nets
N and N 0 are equal, and RG(N 0 ) = T S 0 . t
u
Lemma 1 states that to a given solvable flts (with a solution N = (P, T, F, M0 ))
one can always add a new edge (s, t(s,s0 ) , s0 ), obtaining another solvable flts,
provided that s is a state corresponding to some marking M , which is ≤-maximal
in [M0 i, and t(s,s0 ) denotes the label of the edge from s to s0 , such that t(s,s0 ) ∈
/ T.
We will use this fact to prove the following theorem
Theorem 1. Let T S = (S, T, →, s0 ) be a solvable flts. Then, for every t ∈ T ,
→
−
there exists a finite set T and a function φ : t → 2T \ {∅} such that T S [+tφ] is
solvable.
Proof. Let N = (P, T, F, M0 ) be a net solving T S. As T S is finite, N is bounded,
and so we can calculate a common bound n on the tokens in the reachable
markings for all the places, n = max(M (p) | M ∈ [M0 i, p ∈ P ).
We extend N to N 0 = (P ∪ P 0 , T, F 0 , M00 ) by adding complement places [9]
P 0 = {p0 | p ∈ P } in such a way that, for all M ∈ [M0 i and p ∈ P , we define
M 0 , such that M 0 (p) = M (p) and M 0 (p0 ) = n − M (p). This can be done by
inserting in the initial marking n − M0 (p) tokens into each p0 ∈ P 0 , and setting
F 0 (p0 , a) = F (a, p) as well as F 0 (a, p0 ) = F (p, a), for all p0 ∈ P 0 and a ∈ T .
Since, for distict markings M1 , M2 ∈ [M00 i, there exists a place p ∈ P (in which
they differ) such that M1 (p) > M2 (p) and M1 (p0 ) < M2 (p0 ), or M2 (p) > M1 (p)
and M2 (p0 ) < M1 (p0 ), all distinct markings reachable in N 0 are ≤-incomparable.
Hence all markings reachable in N 0 are ≤-maximal in [M00 i. By the construction,
the reachability graph of N 0 is isomorphic to T S.
→
−
We then construct T S 0 by adding to T S a set T of | t | new transitions in such
a way that, for every (p, t, q) ∈→, we also add (q, t(q,p) , p) ∈→. We then define
→
−
a function φ : t → 2T \ {∅} in such a way that φ((p, t, q)) = {t(q,p) }.
Finally, by repeatedly using Lemma 1 for the net N 0 , we obtain that T S 0 =
T S [+tφ] is solvable. t
u
The construction described in the proof of Theorem 1 will in most cases lead to
a substantial enlargement of the net, as the size of places is doubled, and the
number of newly created transitions is bounded by the size of the reachability
graph of the initial net. However, as illustrated by the example depicted in
Figure 6, there may also exist solutions that are much smaller. Hence, there is a
room for improvement of the suggested constructive technique.
5 Infeasibility for reversing
To draw attention to another important issue, which becomes relevant during the
analysis of flts’s from the viewpoint of reversibility of transitions, let us consider
the following example.
Suppose that one attempted to introduce a reverse for a in T S8 of Figure 7,
which can be solved by N6 . Although there exists a (strict) reverse a in N6 ,
depicted in Figure 7, the meaning of a may be confusing. We cannot regard it as
an undoing of the executing of action a, since N6 can fire bca where a does not
occur at all. What is more, we can keep repeating the firing of bca indefinitely,
without executing a even once. To address this situation, we introduce the notion
of infeasibility for reversing.
T S8 :
N6 : a
• a •
a
a
b c
b c
Fig. 7. T S [+a] allows execution of a without executing of a.
Definition 4. Let T S = (S, T, →, s0 ) be an flts. Then a ∈ T is infeasible (for
reversing), if T S [+a] has a path starting from s0 with more occurrences of a
than a. Otherwise, a is feasible (for reversing).
There is a straightforward necessary condition for being feasible for reversing.
Proposition 4. Let T S = (S, T, →, s0 ) be an flts and t ∈ T . If T S [−t] has
a path from • tT S ∪ {s0 } to t•T S then t is infeasible for reversing.
In general, the reversed implication does not hold. Take, for example, T S10 =
[+a]
T S9 of Figure 8. It has a path labelled acdaa, with more a’s than a’s, implying
the infeasibility for reversing of transition a in T S9 . However, the reduction
[−a]
of T S9 by deleting a, namely T S9 has no path starting from • aT S9 ∪ {s0 }
•
to aT S . Note that T S10 and T S9 are both solvable (see N7 of Figure 8 with
or without dashed arcs, respectively). We will now show that one can always
2 T S9 : a
a • b • b a
2 a
• s0 c
N7 : d
2
• d a
2 T S10 :
a a
a b
a
a c •
s0 a c d
[−a]
Fig. 8. a is infeasible for reversing in T S9 , even though T S9 has no path from
•
aT S9 ∪ {s0 } to a•T S9 .
establish whether a label of an flts is (in)feasible for reversing. To this end,
formulate the following decision problem:
Feasibility for Reversing Problem
Instance: An flts T S = (S, T, →, s0 ) and t ∈ T .
Question: Is t feasible for reversing in T S?
Proposition 5. The Feasibility for Reversing Problem is decidable.
Proof (Sketch of the algorithm.).
The following algorithm reduces the problem of checking the feasibility of a
transition for reversing to the problem of finding shortest paths in a weighted
digraph.
Input: An flts T S = (S, T, →, s0 ) and t ∈ T .
Output: YES if t is feasible for reversing in T S; otherwise NO.
Procedure:
1. Compute a weighted graph G = (V, E, w) on the basis of the extension
T S [+t] = (S, T ∪ {t}, →0 , s0 ) of T S, in the following way (for all s, s0 ∈ S,
a ∈ T ∪ {t}):
– V = S;
– (s, s0 ) ∈ E if(s, a, s0 ) ∈→0 ;
1 if (s, t, s0 ) ∈→0
– w((s, s )) = −1 if (s, t, s0 ) ∈→0
0
0 otherwise.
2. Use, e.g., Bellman-Ford algorithm, to search for a state swit , such that
the distance between s0 and swit is negative.
3. If swit exists, return NO and otherwise YES. t
u
For a transition system consisting of n states the preprocessing phase (step 1)
can be done in time O(n2 ). The computation of step 2 can be performed in time
O(n3 ) (basing on Bellman-Ford algorithm). Therefore the overall complexity of
the algorithm is O(n3 ).
6 Concluding remarks
In this paper, we have investigated reversibility of transitions in bounded nets. In
particular, we have shown that each transition in such nets can be reversed using
a suitable set of new transitions, but not necessarily a single reverse transition.
In future, we plan to investigate ways in which the generation of sets of reverses
could be optimised.
Acknowledgements
We thank Uli Schlachter for assistance with preliminary tests and for adding
new modules to APT. We are also grateful to all anonymous reviewers for their
constructive comments.
References
1. Kamila Barylska, Eike Best, Evgeny Erofeev, Łukasz Mikulski, and Marcin
Piątkowski. On binary words being Petri net solvable. Proceedings of the In-
ternational Workshop on Algorithms & Theories for the Analysis of Event Data,
ATAED 2015, 1371:1–15, 2015.
2. Kamila Barylska, Maciej Koutny, Łukasz Mikulski, and Marcin Piątkowski. Re-
versible computation vs. reversibility in Petri nets. Reversible Computation - 8th
International Conference, RC 2016, Proceedings, 9720:105–118, 2016.
3. Gérard Berry and Gérard Boudol. The chemical abstract machine. Theoretical
Computer Science, 96(1):217–248, 1992.
4. Luca Cardelli and Cosimo Laneve. Reversible structures. In François Fages, ed-
itor, Proceedings of 9th International Computational Methods in Systems Biology
(CMSB’11), pages 131–140. ACM, 2011.
5. Vincent Danos and Jean Krivine. Reversible communicating systems. In Proceed-
ings of 15th International Conference on Concurrency Theory (CONCUR’04), vol-
ume 3170 of Lecture Notes in Computer Science (LNCS), pages 292–307. Springer-
Verlag (New York), 2004.
6. Vincent Danos and Jean Krivine. Transactions in RCCS. In Proceedings of 16th
International Conference on Concurrency Theory (CONCUR’05), volume 3653 of
Lecture Notes in Computer Science (LNCS), pages 398–412. Springer-Verlag (New
York), 2005.
7. Vincent Danos, Jean Krivine, and Pawel Sobocinski. General reversibility. Elec-
tronic Notes Theoretical Computer Science, 175(3):75–86, 2007.
8. Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Reversing
higher-order Pi. In Proceedings of 21th International Conference on Concurrency
Theory (CONCUR’10), volume 6269 of Lecture Notes in Computer Science, pages
478–493. Springer, 2010.
9. Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of
the IEEE, 77:541 – 580, 1989.
10. Iain Phillips and Irek Ulidowski. Reversing algebraic process calculi. Journal of
Logic and Algebraic Programming, 73(1-2):70–96, 2007.
11. Iain Phillips and Irek Ulidowski. Reversibility and asymmetric conflict in event
structures. Journal of Logic and Algebraic Methods in Programming, 84(6):781–
805, 2015.
12. Iain Phillips, Irek Ulidowski, and Shoji Yuen. A reversible process calculus and
the modelling of the ERK signalling pathway. In Proceedings of 4th Workshop
on Reversible Computation (RC’12), volume 7581 of Lecture Notes in Computer
Science, pages 218–232. Springer, 2012.