Reversible computation deals with mechanisms for undoing the effects of actions executed by a dynamic system. 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. 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 on nets with finite state spaces and show, in particular, that every transition in such nets can be reversed using a suitable set of new transitions.
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 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 ‘straightforward’ 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
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 2 S.4 A label t is fireable at s 2 S, denoted by s[ti, if (s; t; s0) 2 !, for some s0 2 S. A state s0 is reachable from s through the execution of 2 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 2 T is fireable, from a state s, denoted by s[ i, if there is some state s0 such that s[ is0.
Let tT S = fs 2 S j (s0; t; s) 2!; for some s0 2 Sg and tT S = fs 2 S j (s; t; s0) 2!; for some s0 2 Sg 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) 2 !1 , ( (s); t; (s0)) 2 !2, for all s; s0 2 S1.
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 2 T is enabled at a marking M , denoted by M [ti, if M (p) F (p; t), for all p 2 P . The effect of a transition t on a place p is e 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) + e p(t) for every p 2 P . The notions of enabledness and firing, M [ i and M [ iM 0, are extended in the usual way to sequences 2 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 2 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 [M0i is finite, and its reachability graph is then defined as an flts
RG(N ) = ([M0i; T; f(M; t; M 0) j M; M 0 2 [M0i ^ M [tiM 0g; 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 2 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 2 T is a new transition t such that e p(t) = e p(t), for all places p 2 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 effectreverse t is not necessarily a strict reverse (see Figure 1).
a 2 2 a a 2 2 a (Un)solvable words A word w = t1t2 : : : tn of length n 2 N uniquely corresponds to a labelled transition system T S(w) = (f0; : : : ; ng; T; f(i 1; ti; i) j 0 < i n ^ ti 2 T g; 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 = vw0u, 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
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 2 T is an flts T S[ t] = (S0; T n ftg; !0; s0) such that:
S0 S are all the states reachable in T S without using !t ; (s1; a; s2) 2!0 if (s1; a; s2) 2!, for all a 6= t and s1; s2 2 S0. – The extension of T S by reversing t 2 T is an flts T S[+t] = (S; T [ftg; !0; s0) such that, for all s1; s2 2 S: (s1; a; s2) 2!0 if (s1; a; s2) 2!, for all a 2 T ; (s1; t; s2) 2!0 if (s2; t; s1) 2!.
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 : a p2 p1 a 3 p4 2 p3 b b b
T S0 : b a b
T S1 : b b a b b b b b a b b
a b b
T S2 : b b a b a
b a a b the dashed part), while T S1 = T S0[+b] 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 2 T . If T S[+a] is solvable then there exists its solution such that a is a strict reverse of a.
N2 : a 3 b 2
2 p1 p2 b b b
T S3 : a b b a b b
T S4 : b b a b b
a b b 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.
N3 : a 2 p2 p3 p1 p4 a 2 b
T S5 : b b a a a b b a
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 2 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.
a
2 N4 : p2 p3 3 p1 p4 3 a 2 3 b 2 p5 p6 2 b b b
T S6 : b b a a b b b a b a Fig. 5. N4 solving T S6 of N2 and N3.
=
T S3[+a;b] derived by synchronising the transitions We end this section looking at the solvability of words over a two-letter alphabet. Proposition 3. Let w 2 fa; bg 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 fa; bg yields solvability of w, which is a contradiction. Hence, the following corollary holds Corollary 1. Let w 2 fa; bg 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.
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 e b1 (p) = e b2 (p) = e 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 effectreverses.
N5 : a p3 2 p1 2 3 p2 3 b1 2
T S7 : 2 2 b b2 b2 b2 b2
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 2 T is an flts T S[+t ] = (S; T 0; !0; s0) such that: – : !t ! 2T n f;g is a mapping specifying all possible ways in which each of t-labelled arcs can be reversed; – T 0 = T [ T ; – (s1; a; s2) 2!0 if (s1; a; s2) 2!, for any a 2 T ; – (s1; t0; s2) 2!0 if (s2; t; s1) 2! and t0 2 ((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 = ([M0i; T; !; M0) be its reachability graph, and t 2= T be a new transition symbol. If a reachable marking M is -maximal in [M0i and M 0 2 [M0i, then
T S0 = ([M0i; T [ ftg; ! [f(M; t; M 0)g; M0) is a solvable flts.
Proof. Let N 0 = (P; T [ ftg; F 0; M0), where:
F 0(p; a) = F (p; a) for all p 2 P and a 2 T F 0(a; p) = F (a; p) for all p 2 P and a 2 T F 0(p; t) = M (p) for every p 2 P
F 0(t; p) = M 0(p) for every p 2 P .
We then obtain that:
(
We then observe that, by (
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) j M 2 [M0i; p 2 P ).
We extend N to N 0 = (P [ P 0; T; F 0; M00 ) by adding complement places [9] P 0 = fp0 j p 2 P g in such a way that, for all M 2 [M0i and p 2 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 2 P 0, and setting F 0(p0; a) = F (a; p) as well as F 0(a; p0) = F (p; a), for all p0 2 P 0 and a 2 T . Since, for distict markings M1; M2 2 [M00 i, there exists a place p 2 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 S0 by adding to T S a set T of j!t j new transitions in such a way that, for every (p; t; q) 2!, we also add (q; t(q;p); p) 2!. We then define a function : !t ! 2T n f;g in such a way that ((p; t; q)) = ft(q;p)g. Finally, by repeatedly using Lemma 1 for the net N 0, we obtain that T S0 = T S[+t ] is solvable. 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
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.
N6:
a b a c
T S8: a a b c
Definition 4. Let T S = (S; T; !; s0) be an flts. Then a 2 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 2 T . If T S[ t] has a path from tT S [ fs0g to tT S then t is infeasible for reversing. In general, the reversed implication does not hold. Take, for example, T S10 = T S9[+a] 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 of T S9 by deleting a, namely T S9[ a] has no path starting from aT S9 [ fs0g 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 N7: a a 2 2 2 2 b c d
T S9:
s0 T S10: a a s0 a b b c c a a a d a d a a Fig. 8. a is infeasible for reversing in T S9, even though T S9[ a] has no path from aT S9 [ fs0g to aT S9 . establish whether a label of an flts is (in)feasible for reversing. To this end, formulate the following decision problem:
Instance: An flts T S = (S; T; !; s0) and t 2 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 2 T .
Output: YES if t is feasible for reversing in T S; otherwise NO.
1. Compute a weighted graph G = (V; E; w) on the basis of the extension T S[+t] = (S; T [ ftg; !0; s0) of T S, in the following way (for all s; s0 2 S, a 2 T [ ftg): – V = S; – (s; s0) 2 E if (s; a; s0) 2!0; – w((s; s0)) = <8 11 iiff ((ss;; tt;; ss00)) 22!!00
: 0 otherwise. tu 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
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.
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.
7. Vincent Danos, Jean Krivine, and Pawel Sobocinski. General reversibility.
Electronic Notes Theoretical Computer Science, 175(
Logic and Algebraic Programming, 73(