Resource Allocation Systems (RAS) have been intensively studied in the last years in the domain of Flexible Manufacturing Systems (FMS). The success of this research line has been based on the identi cation of particular subclasses of Petri Nets that correspond to a RAS abstraction of this kind of systems. In this paper we take a parallel road to that travelled through for FMS, but for the case of software applications. The considered applications present concurrency and deadlocks can happen due to the allocation of shared resources. We will evince that the existing subclasses of Petri Nets used to study this kind of deadlock problems are insu cient, even for very simple software systems. From this starting point we propose a new subclass of Petri Nets that generalizes the previously known RAS subclasses and we present a taxonomy of anomalies that can be found in the context of software systems.
Among the most recurrent patterns in a wide disparity of engineering disciplines,
the competition for shared resources between concurrent processes takes a
prominent position. The reader might think of examples in the context of distributed
systems, operations research, manufacturing plants, etc. The perspective of
discrete event systems theory proves appropriate and powerful as a framework in
which provide solutions to the so-called resource allocation problem [
RAS are usually conceptualized around two distinct entities, processes and
resources, thanks to a prior abstraction process which is inherent in the discipline.
The resource allocation problem refers to satisfying successfully the requests for
resources made by the processes, ensuring that no process ever falls in a
deadlock. A set of processes is deadlocked when they inde nitely wait for resources
that are already held by other processes of the same set [
RAS can be categorized both on the type of processes (sequential,
nonsequential) and resources (serially reusable, consumable) [
Although other models of concurrency have also been considered [
This fact is well notorious in the domain of Flexible Manufacturing Systems
(FMS), where Petri net models for RAS have widely succeeded since the
seminal work of Ezpeleta et al. was introduced [
Nowadays, there exists a plethora of Petri net models for modelling RAS in
the context of FMS, which often overcome some of the syntactical limitations of
the S3PR class [
Most analysis and control techniques in the literature are based on the
computation of a structural element which univocally characterizes deadlocks in
many RAS models: the so-called bad siphon. A bad siphon is a siphon which is
not the support of a p-semi ow. If bad siphons become (su ciently) emptied,
their output transitions die since the resource places of the siphon cannot regain
tokens anymore, thus revealing the deadly embrace. Control techniques thus rely
on the insertion of monitor places [
Although there exist obvious resemblances between the resource allocation
problem in FMS and that of parallel or concurrent software, previous attempts
to bring these well-known RAS techniques into the eld of software engineering
have been, to the best of our knowledge, either too limiting or unsuccessful.
Gadara nets [
Section 2 presents a motivating example and discusses the elements that a RAS net model should desirably feature in order to successfully explore the resource allocation problem within the software enginering discipline. Taking into account those considerations, section 3 introduces a new Petri net class, called PC2R. Section 4 relates the new class to those de ned in previous works and establishes useful net transformations which forewarn us about new behavioural phenomena. Section 5 introduces some of these anomalies which highlight the fact that previous theoretical results in the context of FMS are insu cient in the new framework. Finally, section 6 summarizes the results of the paper. 2
The RAS view of a software application
Example 1 presents a humorous variation of Dijkstra’s classic problem of the
dining philosophers. We will adopt and adapt the beautiful writing by Hoare at
[
Example 1. The pragmatic dining philosophers. Five philosophers spend their lives thinking and eating. The philosophers share a common dining room where there is a circular table surrounded by ve chairs, each belonging to one philosopher. A microwave oven is also available. In the center of the table there is a large bowl of spaghetti which is frequently re lled (so it cannot be emptied), and the table is laid with ve forks. On feeling hungry, a philosopher enters the dining room, sits in his own chair, and picks up the fork on the left of his place. Then he touches the bowl to feel its temperature. If he feels the spaghetti got too cold, he will leave his fork and take the bowl to the microwave. Once it is warm enough, he will come back to the table, sit on his chair and leave the bowl on the table after recovering his left fork (please bear in mind that the philosopher is really hungry by now). Unfortunately, the spaghetti is so tangled that he needs to pick up and use the fork on his right as well. If he can do it before the bowl gets cold again, he will serve himself and start eating. When he has nished, he puts down both forks and leaves the room.
According to the classic RAS nomenclature, each philosopher is a sequential process, and the ve forks plus the bowl are serially reusable resources which are shared among the ve processes. From a software perspective, each philosopher can be a process or a thread which will be executed concurrently.
Algorithm 1 introduces the code for each philosopher. Notationally, we modelled the acquisition / release of resources by way of the wait() / signal() operations, respectively. Both of them have been generalized for the acquisition of multiple resources (separated by commas when invoking the function). Finally, the trywait() operation is a non-blocking wait operation. If every resource is available at the time trywait() is invoked, then it will acquire them and return TRUE. Otherwise, trywait() will return FALSE without acquiring any resource. For the sake of simplicity, it is assumed that the conditions with two or more literals are evaluated atomically.
Algorithm 1 - Code for Philosopher i (where i ∈ {1, 2, 3, 4, 5}) var fork: array [1..5] of semaphores; // shared resources bowl: semaphore; // shared resource begin do while (1)
THINK;
Enter the room; (T1) wait(fork[i]); do while (not(trywait(bowl, fork[i+1 mod 5]))
or the spaghetti is cold ) (T2) if (trywait(bowl)
and the spaghetti is cold ) then (T3) signal(fork[i]);
Go to the microwave; Heat up spaghetti;
Go back to table; (T4) wait(fork[i]); (T5) signal(bowl);
end if; (T 6) loop;
Serve spaghetti; (T7) signal(bowl);
EAT; (T8) signal(fork[i], fork[i+1 mod 5]);
Leave the room; loop; R_S
A1 A0
A5 T1 T6 T7 A6 T8
T2 T5
T4
T3
A3 A2 A4
R_F1
R_F2
Figure 1 depicts the net for algorithm 1, with i = 1, after abstracting the relevant information from a RAS perspective. Figure 2 renders the composition of the ve philosopher nets via fusion of the common shared resources. Note that if we remove the dashed arcs from gure 2, then we can see ve disjoint strongly connected state machines plus six isolated places.
The ve state machines represent the control ow for each philosopher. Every state machine is composed of seven states (each state being represented by a place). Tokens in a state machine represent concurrent processes/threads which share the same control ow. In this case, the unique token in each machine is located at the so-called idle place. This means that, at the initial state, every philosopher is thinking (outside the room). In general, the idle place can be seen as a mechanism which enforces a structural bound: the number of concurrent active threads (i.e. non-idle) is limited. Here, at most one philosopher of type i can be inside the room, for each i ∈ {1, 2, 3, 4, 5}.
The six isolated places are called resource places. A resource place represents a certain resource type, and the number of tokens in it represents the quantity of free instances of that resource type. In this case, every resource place is monomarked. Thus, at the initial state there is one fork of type i, for every i ∈ {1, 2, 3, 4, 5}, plus one bowl of spaghetti (modelled by way of the resource place at the centre of the gure).
Finally, the dashed arcs represent the acquisition or release of resources by the active threads when they change their execution state. Every time a transition is red, the total amount of resources available is altered. Please note, however, that moving one isolated token of a state machine (by ring its transitions) until the token reaches back the idle state, leaves the resource places marking unaltered. Thus, the resource usage is conservative.
Fig. 2. The dining philosophers are thinking. Arcs from/to PR are dashed for clarity.
At this point, we will discuss some capabilities that (in our humble opinion) a RAS model should have so as to support the modelling of concurrent programs.
Although acyclic sequential state machines are rather versatile as models
for sequential processes in the context of FMS (as the success of the S3PR and
S4PR classes prove), this is clearly too constraining even for very simple software
systems. Considering B hm and Jacopini’s theorem [
Another signi cant di erence between FMS and software systems from a RAS perspective is that resources in the latter are not necessarily physical (e.g., a le) but can also be logical (e.g., a semaphore). This has strong implications in the degree of freedom allowed for allocating those resources: we will return to this issue a little later.
In this domain, a resource is an object that is shared among concurrent processes/threads and must be used in mutual exclusion. Since the number of resources is limited, the processes will compete for the resource and will use it in a non-preemptive way. This particular allocation scheme can be imposed by the resources’ own access primitives, which may be blocking. Otherwise, the resource can be protected by a binary semaphore/mutex/lock (if there is only one instance of that resource type) or by a counting semaphore (multiple instances). Note that this kind of resources can be of assorted nature (e.g., shared memory locations, storage space, database table rows) but the required synchronization scheme is inherently similar.
On the other side, it is well-known that semaphores used in that aim can be also seen as non-preemptive resources which are used in a conservative way. For instance, a counting semaphore that limits the number of connections to a database can be interpreted in that way from a RAS point of view. Here processes will wait for the semaphore when attempting to establish a database connection, and will release it when they decide to close the aforementioned connection.
However, semaphores also perform a relevant role as an interprocess signaling facility, which can also be a source of deadlocks. In this work, our goal is the study of the resource allocation problem, so this functionality is out of scope. We propose xing deadlock problems due to resource allocation issues rstly, and later apply other techniques for amending those due to message passing.
Due to their versatility, semaphore primitives are interesting for studying how resources can be allocated by a process/thread. For instance, XSI semaphores (also known as System V semaphores) have a multiple wait primitive (semop with sem_op<0). An example of multiple resource allocation appears in algorithm 1. Besides, an XSI semaphore can be decremented atomically in more than one.
Both POSIX semaphores (through sem_trywait) and XSI semaphores (through semop with sem_op<0 and sem_flag=IPC_NOWAIT) have a non-blocking wait primitive. Again, algorithm 1 could serve as an example. Finally, XSI semaphores also feature inhibition mechanisms (through semop with sem_op=0), i.e. processes can wait for a zero value of the semaphore.
As we suggested earlier, the fact that resources in software engineering do not always have a physical counterpart is a very peculiar characteristic with consequences. In this context, processes do not only consume resources but also can create them. A process will destroy the newly created resources before its termination. For instance, a process can create a shared memory variable (or a service!) which can be allocated to other processes/threads. Hence the resource allocation scheme is no longer rst-acquire-later-release, but it can be the other way round too. Nevertheless, all the resources will be used in a conservative way by the processes (either by a create-destroy sequence or by a wait-release sequence). As a side e ect, and perhaps counterintuitively, there may not be free resources during the system startup (as they still must be created), yet being the system live.
Summing up, for successfully modelling RAS in the context of software engineering, a Petri net model should have at least the following abstract properties: 1. The control ow of the processes should be represented by state machines with support for decisions (if-then-else blocks) and nested internal cycles (while-do blocks). 2. There can be several resource types and multiple instances of each one. 3. State machines can have multiple tokens (representing concurrent threads). 4. Processes/threads use resources in a conservative way 5. Acquisition/release arcs can have non-ordinary weights (e.g., a semaphore value can be atomically incremented/decremented in more than one unit) 6. Atomic multiple acquisition/release operations must be allowed 7. Processes can have decisions dependent of the allocation state of resources (due to the non-blocking wait primitives, as in gure 2) 8. Processes can lend resources. As a side e ect, there could exist processes that depend on resources which must be created/lent by other processes (hence they cannot nish if executed in isolation) 3
In this section, we will present a new Petri net class, which ful lls the requirements advanced in section 2: the class of Processes Competing for Conservative Resources (PC2R). This class generalizes other subclasses of the SnPR family while respecting the design philosophy on these. Hence, previous results are still valid in the new framework. However, PC2R nets can deal with more complex scenarios which were not yet addressed from the domain of SnPR nets.
De nition 1 presents a subclass of state machines which is used for modelling the control ow of the processes in isolation. Iterations are allowed, as well as decisions within internal cycles, in such a way that the control ow of structured programs can be fully supported. Non-structured processes can still be refactored into them as discussed in Section 2.
De nition 1. An iterative state machine N = h{p0} ∪ P, T, Ci is a strongly connected state machine such that either every cycle contains p0 or P can be partitioned into two subsets P1, P2, with a place p ∈ P2 such that: 1. The subnet generated by h{p} ∪ P1, •P1 ∪ P1•i is a strongly connected state machine in which every cycle contains p, and 2. The subnet generated by h{p0} ∪ P2, •P2 ∪ P2•i is an iterative state machine.
In gure 1, if we remove the resource places R_F 1, R_F 2 and R_S then we obtain an iterative state machine, with P1 = {A2, A3, A4}, P2 = {A1, A5, A6}, p0 = A0 and p = A1. The de nition of iterative state machines is instrumental for introducing the class of P C2R nets.
P C2R nets are modular models. Two P C2R nets can be composed into a new P C2R model via fusion of the common shared resources. Please note that a P C2R net can simply be one process modelled by an iterative state machine along with the set of resources it uses. Hence the whole net model can be seen as a composition of the modules for each process. We will formally de ne the class in the following: De nition 2. Let IN be a nite set of indices. A P C2R is a connected generalized pure P/T net N = hP, T, Ci where: 1. P = P0 ∪ PS ∪ PR is a partition such that: (a) [idle places] P0 = {p01 , ..., p0|IN | }; (b) [process places] PS = P1 ∪ ... ∪ P|IN |, where ∀i ∈ IN : Pi 6= ∅ and ∀i, j ∈ IN : i 6= j, Pi ∩ Pj = ∅; (c) [resource places] PR = {r1, ..., rn}, n > 0. 2. T = T1 ∪ ... ∪ T|IN |, where ∀i ∈ IN , Ti 6= ∅, and ∀i, j ∈ IN , i 6= j, Ti ∩ Tj = ∅. 3. For all i ∈ IN the subnet generated by restricting N to h{p0i } ∪ Pi, Tii is an iterative state machine. 4. For each r ∈ PR, there exists a unique minimal p-semi ow associated to r,
Yr ∈ IN|P |, ful lling: {r} = kYrk ∩ PR, (P0 ∪ PS ) ∩ kYrk 6= ∅, and Yr[r] = 1. 5. PS = Sr∈PR (kYrk \ {r}).
Please note that the support of the Yr p-semi ows (point 4 of de nition 2) may include P0: this is new with respect to S4P R nets. Such a resource place r is called a lender resource place. If r is a lender, then there exists a process which creates (lends) instances of r. In our model, processes can start their execution creating resource instances, but before acquiring any other resource. Otherwise, it could happen that the support of a minimal p-semi ow would contain more than one resource place (thus infriging condition 4 of de nition 2).
The class supports iterative processes, multiple resource acquisitions, nonblocking wait operations and resource lending. Inhibition mechanisms are not natively supported (although some cases can still be modelled with PC2R nets).
The next de nition generalizes the notion of acceptable initial marking
introduced for the S4PR class. In software systems all processes/threads are initially
inactive and start from the same point (the begin operation). Hence, all of the
corresponding tokens are in the idle place in the initial marking (the process
places being therefore empty). Note that lender resource places may be empty
for an acceptable initial marking. Figure 2 shows a P2CR net with an acceptable
initial marking which does not belong to the S4PR class.
In [
The transformation rule is based on the idea of converting every while-do block in an acyclic process which is activated by a lender resource place. This lender place gets marked once the thread reaches the while-do block. The token is removed at the exit of the iteration. This transformation must be applied starting by the most intern loops, proceeding in decreasing nesting order. Figure 3 depicts the transformation rule. The rule preserves the language accepted by the net (and thus liveness) since it basically consists in the addition of a implicit place (place P 1 in the right hand net of gure 3, since R_P 1 can be seen as a renaming of P 1 in the left hand net).
Figure 4 illustrates the transformation of the net of example 1 but restricted to two philosophers into the corresponding SB SPQR.
Thanks to such transformations, the SB SPQR class can express the widest range of systems in the Sequential RAS Petri net family. Figure 5 introduces the inclusion relations between a variety of Petri net classes for Sequential RAS.
T3
P2
T4 P3 P1
P1
R_P1 T1
T2
T1
T2 T5
T6
T5
T6
P R
T3
P2 T4 P3
Fig. 3. Transforming PC2Rs into SB SPQRs: From iterative to acyclic processes
Petri Nets & Concurrency TB4
B4 B3
TB3 B2
TB5
TB2 TA2 TA5
A2 A4
TA3 TA4
A3
R_F1 R_S R_F2
R_S TA2
A2
TA3
A3
TA4
A4
TA5 R_A1
R_F1 TA1 A1
TA6 A0
A5 TA7 A6
TA8 TA1 A1 TA6 A0 TA7
A5 A6
TA8 S* PR
+ process structure − Fig. 5. Inclusion relations between Petri net classes for RAS TB8 B6 TB7 B5
B0 TB6 B1 TB1 TB8 B6 B5 TB7 B0 TB6 B1
TB1
"contains" "contains
after transformation" TB5
B4
TB4
B3
TB3
B2
TB2 5
Some bad properties through examples The bad news about the discussion in sections 2 and 3 is that siphon-based control techniques for RAS do not work in general for concurrent software, even ignoring (i.e., not using) the resource lending feature introduced by PC2R nets.
Let us have a look back at example 1 and its related algorithm 1. It is not di cult to see that, if every philosopher enters the room, sits down and picks up the fork on the left of himself, the philosophers will be trapped in a livelock. Every philosopher can eventually take the bowl of spaghetti and heat it up in the microwave. This pattern can be repeated in nitely, but it is completely useless, since no philosopher will ever be able to have dinner.
This behaviour is obviously re ected in the corresponding net representation
at gure 2. Let us construct a ring sequence σ containing only the rst transition
of each state machine (i.e., the output transition of its idle place). The ring order
of these transitions is irrelevant. Now let us re such a sequence, and the net falls
in a livelock. The internal cycles are still rable in isolation, but no idle place can
ever be marked again. Unfortunately, the net has several bad siphons, but none
of them is empty or insu ciently marked in the livelock. In other words, for every
reachable marking in the livelock, there exist output transitions of the siphons
which are rable. As a result, the siphon-based non-liveness characterization for
earlier net classes (such as S4PR [
A similar pattern can be observed in the upper net of gure 4. There exist three bad siphons, which are D1 = {A2, A3, A4, A5, A6, B2, B4, B5, B6, R_F 2, R_S}, D2 = {A2, A4, A5, A6, B2, B3, B4, B5, B6, R_F 1, R_S} and D3 = {A2, A4, A5, A6, B2, B4, B5, B6, R_F 1, R_F 2, R_S}. Besides, every transition in the set Ω = {T A2, T A3, T A4, T A5, T B2, T B3, T B4, T B5} is an output transition of D1, D2 and D3. After ring T A1 and T B1 from the initial marking, the state A1 + B1 + R_S is reached. This marking belongs to a livelock with other six markings. The reader can check that, unfortunately, there exists a rable transition in Ω for every marking in the livelock. A similar phenomenon can be observed for the SB SPQR net at the bottom of gure 4.
In general, livelocks are not a new phenomenon in the context of Petri net
models for RAS. Even for L − S3P R nets, which are the simplest models in
the family, deadlock freeness does not imply liveness [
We believe that the transformation of PC2R nets into SB SPQR can be
useful to understand the phenomena from a structural point of view. Intuitively
speaking, the concept of lender resource seems a simple yet powerful instrument
which still remains to be fully explored. Still, SB SPQRs can present very
complex behaviour. For instance, acceptably marked SB SPQR nets do not even
hold the directness property [
TA1 A1 TA2 A2 TA3
R1 R2 R3
TB3
B2 TB2
B1 TB1
A1, B1, R2 B0
A2,B1,R1,R2
A1,B2,R2,R3
A2,B2,R1,R2,R3 A2, B3, R3
A3, B2, R1
other properties are profoundly discussed (along with their implications) in a
previous work [
T1
A1
T2
A2
T3
A3
A4
T5
A5
T6
A6
T7 A0 T4 T11
B0 R1
R2
R3
R4
R5 T8
B1
T9
B2
T10
B3
B4
T12
B5
T13
B6
T14
Although there exist a variety of Petri net classes for RAS, many of these definition e orts have been directed to obtain powerful theoretical results for the analysis and synthesis of this kind of systems. Nevertheless, we believe that the process of abstraction is a central issue in order to have useful models from a real-world point of view, and therefore requires careful attention. In this work, we have followed that path and constructed a requirements list for obtaining an interesting Petri net subclass of RAS models applied to the software engineering domain. Considering that list, we de ned the class of PC2R nets, which ful lls those requirements while respecting the design philosophy on the RAS view of systems. We also introduced some useful transformation and class relations so as to locate the new class among the myriad of previous models. Finally we observed that the problem of liveness in the new context is non-trivial and presented some cases of bad behaviour which will be subject of subsequent work. A
A place/transition net (P/T net) is a 3-tuple N = hP, T, W i, where W is a total function W : (P × T ) ∪ (T × P ) → IN, being P , T non empty, nite and disjoint sets. Elements belonging to the sets P and T are called respectively places and transitions, or generally nodes. P/T nets can be represented as a directed bipartite graph, where places (transitions) are graphically denoted by circles (rectangles): let p ∈ P , t ∈ T , u = W (p, t), v = W (t, p), there is a directed arc, labelled u (v), beginning in p (t) and ending in t (p ) i u 6= 0 (v 6= 0).
The preset (poset ) or set of input (output) nodes of a node x ∈ P ∪ T is denoted by •x (x•), where •x = {y ∈ P ∪ T | W (y, x) 6= 0} (x• = {y ∈ P ∪ T | W (x, y) 6= 0}). The preset (poset) of a set of nodes X ⊆ P ∪ T is denoted by •X (X•), where •X = {y | y ∈ •x, x ∈ X} (X• = {y | y ∈ x•, x ∈ X}
An ordinary P/T net is a net with unitary arc weights (i.e., W can be de ned as a total function (P × T ) ∪ (T × P ) → {0, 1}). If the arc weights can be nonunitary, the P/T net is also called generalized. A state machine is an ordinary net such that for every transition t ∈ T , |•t| = |t•| = 1. An acyclic state machine is an ordinary net such that for every transition t ∈ T , |•t|, |t•| ≤ 1, and there is no circuit in it.
A self-loop place p ∈ P is a place such that p ∈ p••. A pure P/T net (also selfloop free P/T net) is a net with no self-loop places. In pure P/T nets, the net can be also de ned by the 3-tuple N = hP, T, Ci, where C is called the incidence matrix, C[p, t] = W (p, t) − W (t, p). Nets with self-loop places can be easily transformed into pure P/T nets without altering most signi cant behavioural properties, such as liveness, as shown in gure 8.
m
T n P m
P
n T’
T’’
Fig. 8. Removing self-loop places
A p- ow is a vector Y ∈ ZZ|P |, Y 6= 0, which is a left annuler of the incidence matrix, Y · C = 0. The support of a p- ow is denoted kY k, and its places are said to be covered by Y . A p-semi ow is a non-negative p- ow, i.e. a p- ow such that Y ∈ IN|P |. The P/T net N is conservative i every place is covered by a p-semi ow. A minimal p-semi ow is a p-semi ow such that the g.c.d of its non-null components is one and its support kY k is not an strict superset of the support of another p-semi ow.
A set of places D ⊆ P is a siphon i every place p ∈ •D holds p ∈ D•. The support of a p-semi ow is a siphon but the opposite does not hold in general.
Let N = hP, T, W i be a P/T net, and let P 0 ⊆ P and T 0 ⊆ T , where P 0, T 0 6= ∅. The P/T net N 0 = hP 0, T 0, W 0i is the subnet generated by P 0, T 0 i W 0(x, y) ⇔ W (x, y), for every pair of nodes x, y ∈ P 0 ∪ T 0.
A marking m of a P/T net N is a vector IN|P |, assigning a nite number of marks m[p] (called tokens ) to every place p ∈ P . Tokens are represented by black dots within the places. The support of a marking, kmk, is the set of places which are marked in m, i.e. kmk = {p ∈ P | m[p] 6= 0}. We de ne a marked P/T net (also P/T net system) as the pair hN , m0i, where N is a P/T net, and m0 is a marking for N , also called initial marking. N is said to be the structure of the system, while m0 represents the system state.
Let hN , m0i be a marked P/T net. A transition t ∈ T is enabled (also rable ) i ∀p ∈ •t : m0[p] ≥ W (p, t), which is denoted by m0[ti. The ring of an enabled transition t ∈ T changes the system state to hN , m1i, where ∀p ∈ P : m1[p] = m0[p] + C[p, t], and is denoted by m0[tim1. A ring sequence σ from hN , m0i is a non-empty sequence of transitions σ = t1 t2 ... tk such that m0[t1im1[t2i ... mk−1[tki. The ring of σ is denoted by m0[σitk. A marking m is reachable from hN , m0i i there exists a ring sequence σ such that m0[σim. The reachability set RS(N , m0) is the set of reachable markings, i.e. RS(N , m0) = {m | ∃ σ : m0[σim}.
A transition t ∈ T is live i for every reachable marking m ∈ RS(N , m0), ∃m0 ∈ RS(N , m) such that m0[ti. The system hN , m0i is live i every transition is live. Otherwise, hN , m0i is non-live. A transition t ∈ T is dead i there is no reachable marking m ∈ RS(N , m0) such that m[ti. The system hN , m0i is a total deadlock i every transition is dead, i.e. no transition is rable. A home state mk is a marking such that it is reachable from every reachable marking, i.e. ∀m ∈ RS(N , m0) : mk ∈ RS(N , m). The net system hN , m0i is reversible i m0 is a home state.