T he present work is devoted to the study of deadlock problem in Place/Transition (P/T) nets, particularly to the exploration of how a deadlocks' presence can be revealed solely on the basis of the P/T net N0 in question and a structure, here termed as the fsa of the type Mw, that represents the reachability set <(N0) of N0. The structure can be obtained from N0 following the original algorithm for solving the reachability problem RP for Petri Nets in general case by the author. It turns out, that the structure of Mw bears some important properties with respect to the deadlock analysis. Deadlock analysis is an important part of system veri¯cation, so the results achieved can be of some value to that. It is demonstrated that results presented are quite signi¯cant, and cover some gap in both, theory and practice of the deadlock analysis of state-based systems, particularly those whose speci¯cation can be expressed via Petri Nets.
In the development of (state-based) system, the design of a system in
question, is the core of the process. The latter is actually a realization of the what
requirement speci¯cation is about. There are two intrinsic activities of any
development:validation and veri¯cation. The validation is the process of assurance
that the design will produce the right system (according to requirements), while
the veri¯cation assures that the design is carried on properly (according to a
particular design principle)[
The approach is founded on the information that was neglected and suppressed by the RP algorithm while creating Mw, and thus hidden in it. The modi¯cation of Mw construction, that is introduced in this paper, discloses the information previously hidden to serve the purpose mentioned.
The paper consists of four parts. In the ¯rst part basic notions and results
concerned Petri Nets, reachability and deadlock analysis are given. The second part
deals with the algebraic properties of Mw. It turns out that Mw is ¯nite state
automaton, with some interpretations of its states via k -dimensional
nonegative integer ! vectors. Each such ! vector represents a state subspace of PN
in question, and can be thought of as a poset. That view on ! states allows
us to establish relation among deadlocks and minimal or least elements of such
the posets. In the third part we deal with the issue of disclosing the
information previously hidden, and de¯ne more precisely the new notion and denotation
of !coordinates. The fourth part consists of an application of the theory of
!coordinates developed. The application is made to two PNs, which was
introduced by T.Murata [
In the paper we denote by IN the set of natural numbers f0; 1; 2; : : :g, by Z the set of all integers, Zk (INk ) the set of k-dimensional (nonnegative)integer vectors. A notion of (k-dimensional) vector addition system (VAS) Wk is a couple
Wk = (q0; W ) where q0 2 INk is the initial state of Wk; W is a ¯nite set of (k- dimensional integer) vectors. We call a reachable state vector of Wk each q 2 INk such that 1. q = q0 + wi1 + : : : + win for some integer n ¸ 0; wij 2 W; j = 1; : : : ; n and 2. for 8j(1 · j < n) : qj = q0 + wi1 + : : : + wij 2 INk Here by + we mean the operation of vector addition. We call the set of all such vectors the reachability set of VAS Wk, and denote it as R(Wk). Given any VAS Wk = (q0; W ) then or any q 2 INk a problem whether q 2 R(Wk) is called the reachability problem of VAS (with respect to q). We will occasionally use the abbreviation RP (q; Wk) for it.
With any VAS Wk = (q0; W ) we can associate a tree structure, which we call the vector state tree, V STw, and we mean by that a double labelled oriented rooted tree V STw = (Tw; Lab(V ); Lab(E); q0), Tw = (V; E; r0) is an oriented rooted tree , V - a set of vertices, E µ V £ V - a set of edges, r0 2 V - the root of Tw , Lab(V ) µ INk -a set of vertex labels, Lab(E) µ W - a set of edge labels that are de¯ned as follows: there are two labelling mappings lab1 : V ! Lab(V ); lab2 : E ! Lab(E) such that lab1(r1) = q0 and any vertex of Tw v 2 V with lab1(v) = q has a son u 2 V with lab1(u) = q0 and lab(v; u) = a i® q0 = q+a.
As a very consequence of the above de¯nition we have that Lab(V ) = R(Wk) where Wk = (q0; W ) is the VAS and we can alternatively write V STw = (Tw; R(Wk); Lab(E); q0) 2.1
Place/Transition (P/T) Nets stand here for a class of Petri Nets in which
multiple arcs are allowed and places have unlimited capacities. For more
details on PN we refer the reader to the literature , e.g. [
In Fig. 2 there is a correspondence shown between the graph representation of PN N and pre and post functions. ²t = fp j pre(p; t) 6= 0g the set of preconditions of t t² = fp j post(p; t) 6= 0g the set of postconditions of t p² = ft j pre(p; t) 6= 0g ²p = ft j post(p; t) 6= 0g By the marking of PN N = (P; T; pre; post) we mean a totally de¯ned function m : P ¡! IN (1) (2)
We use m to describe the situation or con¯guration in PN N . Namely we say the condition represented by the place p in PN N holds i® m(p) 6= 0. Without loss of generality we assume that P and T have k and m elements respectively. i.e. P = fp1; p2; ; :::; pkg, T = ft1; t2; ; :::; tmg and we ¯x some ordering of both, places and transitions from now on. Using the ordering of places we can consider m to be the k-dimensional nonnegative integer vector, i.e. m! 2 INk. More formally ! m = (m(p1); m(p2); :::; m(pk)) and m(pi) is the value of m in pi , i = 1; 2; :::; k, according to (1). In our example (Fig. 1) m(pi) = 1 i® i = 1, or alternatively m! = (1; 0; 0; 0; 0). For the simplicity we will use the denotation m for either interpretations of the marking m when it doesn't cause any troubles. We say t is enabled in m, and denote it m t , i® for every p 2² t; m(p) ¸ pre(p; t). In Fig. 1 t1 is enabled in m = (1; 0; 0; 0; 0) because ²t1 = fp1g and m(p1) = 1, and pre(p1; t1) = 1. In general, given PN N, a marking m of N, several transitions from T can be enabled in m. Once the transition t is enabled it can ¯re. The e®ect of the ¯ring t in m is the creation of a new marking m0 that depends on m and t. We use a denotation
m t m0 and m0 is de¯ned in the following way: m0(p) = 8 m(p) ¡ pre(p; t) p 2 ²t n t² >>< m(p) + post(p; t) p 2 t² n² t
m(p) ¡ pre(p; t) + post(p; t) p 2 ²t \ t² >>: m(p) otherwise
In PN N of Fig. 1 we can write m = (1; 0; 0; 0; 0) t1 m0 = (0; 1; 1; 1; 0). Notice transitions t3,t4 will be enabled in m0 either.
We say the sequence of transitions ¾ = t1t2:::tr is admissible ¯ring sequence in PN N, provided a sequence of markings m0; m1; :::; mr exists and such that mi¡1 ti mi , i = 1; 2; :::; r. In that case we write m0 ¾ mr , or simply m0 ? mr, when ¾ is immaterial. The marking m is to be called the reachable marking in N from m0 (via ¾). We ¯x the marking m0 to be the initial marking of PN N = (P; T; pre; post) and we denote it N0 = (N; m0) or N0 = (P; T; pre; post; m0). Given PN N0 = (P; T; pre; post; m0) we de¯ne the set of reachable markings
R(N0) = fm j m0 ¾ m; g;
and we call it PN language.
L(N0) = f¾ 2 T ¤ j m0 ¾ m; ¾ 2 T ¤g
Let N0 = (P; T; pre; post; m0) be a Petri Net with the initial marking m0. Recall m0 can be represented as a k-dimensional nonnegative integer vector, i.e. m0 2 Zk and m0 = (m0(p1); : : : ; m0(pk)). Let us ¯x an ordering of places in P and transitions in T, i.e. P = fp1; : : : ; pkg and T = ft1; : : : ; tmg.
In PN literature (e.g. [
m , m = m0 + (c ¢ ª T (¾))T and ª (¾) is the Parikh mapping over the (ordered) alphabet T, and ª T (¾) stands for the transposition of the row vector ª (¾).
Any transition t 2 T can be represented as a k-dimensional integer vector and It can be easily seen that
t = post(t) ¡ pre(t) post(t) = ((post(p1; t); : : : ; post(pk; t) pre(t) = ((pre(p1; t); : : : ; pre(pk; t)) m0 t
m , m = m0 + t
and we can construct for PN N0 = (P; T; pre; post; m0) the vector addition
system Wk = (q0; W ) an such that q0 = m0; W = ftjt 2 T g , and k = cardP . The
following result holds
Theorem 1. [
Proof:That follows from the above construction. 2.3
Reachability problem for Petri nets attracted a lot of attention of experts in
computer science community. It lasted pretty long time (almost 20 years) a
solution to RP had been obtained [
qi · qj ) Yqi µ Yqj The necessary and su±cient conditions can be formulated for a path being in¯nite with ¯nite or in¯nite set of reachable states. Based on that a theory of transformation of in¯nite paths (a graph morphism), that allows pruning in¯nite paths and replacing them by loop-like subgraphs and thus transforming the tree into a rooted graph (vector state graph-vsg). The transformation (T<Am ) has a signi¯cant property that su±x language of the root of the original V STw ¡ Yq0 is included in the su±x language of the root of the resulting vsg T<Am (q0), i.e. Yq0 µ YT<Am (q0). In the case the strong inequality holds 0 0 between the two states on the path (q · q and q 6= q ), that causes introducing so-called !-cordinates, that means replacing the cordinates of the both states in which the strong inequality (<) hol0ds, by the special value !, and thus cre0ating the !-lized state !Aq and !Aq , that become identical, i.e. !Aq = !Aq (A is the set of coordinate indices on which the relation < holds).
By that virtue, due to the properties of ! (! + a = ! ¡ a = ! for any natural number a), any such the transformation has two-side e®ect: pruning the in¯nite path by replacing it by a ¯nite (loop-like) subgraph, and lowering number of coordinates w.r.t. which a comparison satis¯ability of reachable (macro) states should be checked. That guaranties that in a ¯nite number of transformation steps a ¯nite (rooted) vsg structure Tf! can be obtained. The signi¯cant property of the vsg Tf! is that YT ¤(q0) ¶ Yq0 , provided that T ¤(q0) is the macrostate on which the initial state q0 is mapped after the sequence of transformations denoted as T ¤. 3. Vsg Tf! can be thought of as a special kind of ¯nite state automaton (fsa) with some interpretation of its states, and with the input alphabet W = n!
ti jti 2 T o. The de¯nition of the automaton (we used to call it ¯nite state automaton (fsa) (of the type) Mw) can be given as Mw = (Qf ; W; ±; ½0), provided the vsg Tf! = (Qf ; Tf ; ½0 and Tf is the graph representation of state trasition funcion ±. To characterize the behaviour of fsa Mw we introduce special regular expressions (wre-vector regular expressions(w stands here after the set W of vectors)). Any wre ® is given two semantics: [®]-vector semantics; [[ ® ]] - (ordinary) language semantics. Let L½0 be the wre that denotes the language of Mw (i.e.L(Mw)= [[ L½0 ]] ), and q0 to be the initial state of VAS Wk. Then [q0L½0 ] denotes all reachable states. To be more precise
[u] = [u] if u 2 W
[au] = a + [u] if a 2 W and u 2 W ¤
8q 2 Nk; u 2 W ¤ [qu] = q + [u] and 8i(1 · i · juij):qi = [qui] 2 Nk;
[q0L½0 ] = nq0 jq0 = [q0u] ; u 2 [[ L½0 ]] o
(5)
4. Having constructed fsa Mw it is worth to say few words about its structure
w.r.t. how it can be useful in RP solving:
{ The structure of the state diagram of Mw is, in almost all cases,
consisting of n ¸ 1 strongly connected components (scc), due to
transformations applied to V STw initially and to vsg afterwards. The class of
scclike Mws, can be divided into two subclasses. The ¯rst subclass contains
Mws whose states are labelled by simple (k-dimensional) nonnegative
integer vectors. Such Mw manifests that P/T net in question N0 (and
corresponding VAS Wk) has ¯nite set of reachable states. The second
subclass consists of Mws whose states are labelled by ! (k-dimensional)
nonnegative integer vectors (vectors having at least one ! coordinate).
Such Mw manifests that P/T net in question N0 (and corresponding
VAS Wk) has in¯nite set of reachable states.
{ The way how to solve the reachability problem w.r.t. a state q 2 Nk
will di®er depending on whether R(N0) is ¯nite or in¯nite. In the ¯nite
case RP (q; N0) can be solved trivially by inspecting the state diagram
of Mw and checking whether there is a state with the label q or not. In
the second case we have to do the following steps:
1) to ¯nd a state ½ of Mw such that q · ½; if such a state does not
exists, then RP (q; N0) has negative solution (q 2= R(N0) ).
2) assume we found such the state ½; now we have to construct a path
leading from the root state ½0 that is the image of the initial state
q0 under chain of transformations (½ = T<¤Am (q0))(for more details
see [
A = ([`1]T ; [`2]T ¢ ¢ ¢ [`m0 ]T ) provided WL = f`1; `2; :::; `m0 g. 5. ILP constructed does not express exactly conditions to hold for the reachability of the state q. The reason is that at building ILP (7) based on (6) some information is lost. Particularly the information that is connected with an ordering of loops passed, that is prescribed by de¯nition of [q0uv](all reachable states by wre uv ). To check the so called 'proper choice condition' property special test should be performed, that is expressed in the predicate conWk (A; X0; B0). So ¯nally the RP algorithm is
Given: VAS Wk = (q0; W ); q 2 INk - a state to be decided reachable or not;
Step 2 : Construct M ILPw(A; X0; B(q); r); Step 3 : if M ILPw(A; X0; B(q); r) = true then go to Step 4 else go to Step 5 ; Step 4 : q 2 R(Wk): Stop:
Step 5 : q 62 R(Wk): Stop: We use the abbreviation
M ILPWk (A; X0; B(q)) ´ ILPWk (A; X0; B(q)) ^ conWk (A; X0; B0)
RP (q; Wk) ´ M ILPWk (A; X; B(q)) Since ILP is decidable, and also due to ¯niteness of X0 establishing truth of conWk (A; X0; B0) is also decidable, so is the reachability problem. (6) (7)
Algebraic properties of Mw automaton Let us have one more look at fsa Mw = (Q; W; ±; ½0). For simplicity let us assume that Mw consists of single scc with its root state ½0. Example of such Mw is depicted in Fig. 3 Notice that all states of the state diagram are labelled with !vectors, e.g. ½0 = (1; 0; !; 0; !; 0), ½1 = (0; 0; !; 1; !; 0), ½2 = (0; 1; !; 0; !; 0), ½3 = (0; 0; !; 0; !; 1). Important feature of labels of the states of the Mw's state diagram is that they are mutually incomparable as vectors.
We can look at labels of the states of the Mw's state diagram as macrostates, that represent (cover) sets of reachable states. For that, we may call any macrostate ½ - a label of a state in Mw's state0 diagram, as the reachable macrosta0te. We will say tha0t two macrostates ½ and ½ are comparable, and we write ½ · ½ , provided that ½ covers at least those reachable states, that are covered by ½. To express it more formally, we introduce for the macrostate ½ the set of covered reachable states- denoted by S½ i.e.
S½ = fqjq 2 R(N0); q · ½g
S½ is simply partially ordered set (poset). The notion is well-known [
For the de¯nition of poset, and further properties and other results reader
can consult a specialized literature on the subject, e.g. see [
To capture the information hidden (and lost) by the original algorithm to construct the fsa of the type Mw, we have to distinguish three types of indexing ! coordinates: { !a¢ - denotes an ! coordinate in a loop-root state ½, with initial value of the coordinate a , with ¢ as a loop added value to the coordinate after each repetition of the loop; such the ! is called the independent root ! , { !bi;t;¢j - denotes so-called dependent ! coordinate in a loop-root state ½, that depends on i-th ! coordinate that should generate (via repetition of its loop) a minimal value v in i-th coordinate such that v ¸ pre(pi; t) for the transition t to be ¯rable in corresponding state while the initial value of the coordinate the dependant ! belongs to is b; ¢j is the increase of the dependent ! (in the j-th coordinate) caused by the repetition of the loop started by the transition t. { !c- denotes so-called over°owed ! coordinate with the minimal initial value of the coordinate at the time it was over°owed for the ¯rst time.
To get a °avour why we are introducing indexed !s , we are now turning our attention to properties of the poset S½ = (S½; ·; t; u) with respect to a deadlock state ¼, that can be eventually covered by a macrostate ½, i.e. ¼ · ½.
Properties of the poset S½ with respect to the deadlock analysis In the previous section we have discovered, that any macrostate ½ can be taken as the poset S½ = (S½; ·; t; u) . For the discovering a deadlock state of P/T net N0 we would like to make a use of information captured in the Mw's state diagram, speci¯cally in macrostates by which the states are labelled with.
Assume that we are given !-state ½, and to be more speci¯c, let's say that ½ = !Aq = (½1; ½2; :::; ½k) (8) where q = (q1; q2; :::; qk) is a reachable state, A µ f1; 2; :::; kg = K is the set of indices in which ½ has ! - coordinates. To put it in other words that means that ½j = ½ $ if j 2 A
qj if j 2= A and $ 2 n!a¢i ; !bi;t;¢j ; !co.
Base½ = f q½B;i = ³q10; q2; :::; qk0´ ji 2 A; q` = ½` if i 6= `; ` 2 K ¡ fig ; 0 0 (9) 0 qi = r if ½i = $ g where $ 2 n!r¢i ; !rj;t;¢i ; !ro.
That is clear that every q½B;i · ½; in a case ½ has only one ! coordinate then q½B;i is the glb(S½). In the case that jjAjj > 1 q½B;i is the macrostate covering a set of minimal elements of the poset S½.
We will call the macrostates labelling states of Mw the reachable macrostates. Any macrostate ¼ · ½ we will call also the reachable macrostate. From that point of view we may consider elements of Base½ as the collection of reachable macrostates.
Still another notion should be introduced; we de¯ne where
i;t;¢j ; !ro for some r 2 N. and $ 2 n!r¢j ; !r It is clear that q½B = ³q100 ; q2 ; :::; qk00 ´
00 00 qj = r , ½j = $ 00 qj = ½j , ½j 2 N q½B · ½ (10)
The crucial problem is to decide whether q½B is reachable state or not. In the
latter case it will be called spurious state [
Any deadlock state of P/T net
N0 = (P; T; pre; post; q0) is such a state q, that is 1. reachable state, i.e. q 2 R(N0), and 2. for any transition t 2 T and at least one p 2² t, pre(p; t) > q(p) In other words there are not enough tokens at least in one of pre-places ²t of any t 2 T .
Assume we have a deadlock state d 2 ½; that means that any reachable state q 2 ½ and such that q · d will be a deadlock state either. From that we have immediately, that if qB were reachable state, it would be a deadlock state of ½ P/T net N0 = (P; T; pre; post; q0) since it would have been either the least or minimal element of the poset S½. We can summarize the properties described. Assertion 1 Let S½ = (S½; ·; t; u) be the poset formed by the macrostate ½ of the fsa Mw representing the set of reachable states of a P/T net N0 = (P; T; pre; post; q0). Then if there exists a deadlock state d in ½, then at least one of minimal elements or the least element of the poset S½- qmin will be the deadlock state too and such that qmin · d.
So, it means that the least and minimal elements of the poset S½, if they exist, serve as a good indicator of presence and/or absence of deadlocks in the system represented by any P/T net.
In the algorithm of the construction of fsa Mw [
The issue of creating independent ! coordinate is depicted in Fig. 4.
There is a state q, having values a and b in its i-th and j-th coordinate
respectively. There are also two transitions (vectors) say ta and tb that are ¯rable
(applicable) in q. An aplication of ta at q followe d0 by other transitions leads
0
to a state q0 = (q1; :::a ; :::; b; :::qk) , where a < a is a new value of the i-th
coordinate, and according to the algorithm which construts automaton Mw the
transformation T<i applies, that creates a lo0op labelled with the string ¿a = ta®,
that replaces the path leading from q to q which is la b0elled with ¿a = ta® as
well. The e®ect of the transformation is that the state q collapses to q creating
a new state !figq = (q1; :::; !; :::; b; :::qk). Because we are interested in the data
keeping information on the value of the i-th coordinate which has been replaced
by !, we suggest to keep the data as a part of the new 'value' of the
co0ordinate. Another information which we are interested in is the value ¢i = a ¡ a
which expresses the increase of the i-th coordinate after repetition of the loop
¿a = ta®. After all we prefer to denote the new ! value of the i-th coordinate by
!a¢i , and to call such the !coordinate to be independent !coordinate. Another
independent !coordinate can be created due to ¯ring the sequencce of
transitions ¿b = tb¯ starting at the state !figq. Notice that in the intermediate state p
in the i-th coordinate so called over°owed !c cord apears. The case of creating
dependent !cords can be visualized in similar way. Due to space lack we have
to skip that and we refer the reader to [
It was already mentioned the importance of the least and minimal states with respect to (wrt) deadlock analysis of P/T net (sect.3.1). Now we return back to the problem with an aim to analyze in the depth the issue of the role least or minimal states will play in the reachability and deadlok analysis. The main problem here is to decide in any particular case of least and/or minimal state q½B whether it is reachable or not.
Let us consider that q½B;i 2 Base½; then q½B;i µ <(N0) and thus q½B;i is a
macrostate covering a set of reachable states which all have the same i-th
coordinate, say ai. Moreover, the macrostate q½B;i is the macrostate consisting of
minimal states wrt macrostate ½. The nature of the fsa of the type Mw [
The state q½B can be considered to be the least element of the poset S½, provided it is a reachable state, otherwise it can serve as a lower bound for the reachable states- elements of S½. Very often such the state q½B will be just spurious reachable state, and there will be a need for q½B to be proved its reachability. To underpin that assertion some kind of analysis should be introduced ¯rst.
The case analysis of di®erent types of n > 1 !coordinates have been
accomplished [
In the table the entry (1; 1 !; 1) stands for a dependence of !cord dep on ow, and the entry (1; Ã 1; 1) stands for a dependence of !cord dep on ind. We illustrate that only for two cases:(3,0,0).
ind!cord Bdep!cord ow!cord !¢i a
!c !bB;tb;¢j
B µ K ind!cord !¢i a !a¢;i; ¡a0 !¢i;¡;¡
a; a0 ;a00
Bdep!cord !bB;tb;¢j !bB;;tb;¢j;b¡0 !bB;;tb;¢j;b¡0 ;;b¡00
B µ K
ow!cord !c !c;c0 (11) (12)
We propose to use a generalized form to represent !coordinates, and we will call it as form (f).
where ! Here ¸ stands for empty symbol. Basically, in the case of over°owed !coordinates we will use just !c instead of !c¸ or !c¡. In the case of independent and dependent !coordinates we will use instead of empty symbol '-' to visualize the correspondence of high and low indices.
In our consideration we will use shorthand notation for indexed !coordinates ! [Ik] where Ik = µ h1; ¢ ¢ ¢ ; hk ¶ d1; ¢ ¢ ¢ ; dk The following results have been proven as far as the generalization of the process of indexed !coordinates is concerned: 1. the form (f) of !coordinates has been chosen correctly, and it will be preserved by any application of T<!A transformation, and 2. the procedure to obtain the set of minimal elements of the poset represented by a macrostate ½- Base½, is determined by a choice of proper combination of low indices. 5
In his paper [
We can see that Mw automata are isomorphic, but they di®er in !cords as far as their indices are concerned.
Let us have a closer look at the Mw automata from that perspective. In Mw automaton of PN N1 we have two macrostates: ½1 = (1; 0; !01) and ½2 = (0; 1; !0;1). If we look at ½1 = (1; 0; !01) as at the poset, we can have the only minimal and thus the least (in¯mum) state
q½B1 = (1; 0; 0) In the case of ½2 = (0; 1; !0;1) we have the basis of this poset
Base(½2) = f(0; 1; 0); (0; 1; 1)g
There are actually 2 minimal states.
Let us turn our atention to the net N2. In Mw automaton of PN N2 we have also two macrostates: ½1 = (1; 0; !02;;1¡) and ½2 = (0; 1; !0;2). If we look at ½1 as at the poset, we can have here no in¯mum state, but we still have two minimal states that creates :
Base(½1) = f(1; 0; 0); (1; 0; 1)g If we look at ½2 as at the poset, we can have also here no in¯mum state, but we still have two minimal states that creates :
Base(½2) = f(0; 1; 0); (0; 1; 2)g 5.1
In [
Let us consider PN N = (P; T; pre; post) and let t = ¡ pre(p; t) + post(p; t). For any t 2 T and p 2 P we say
p covers t ,df pre(p; t) 6= 0
p covers t ,df t 2 p² C(p) = ft 2 T jp covers t g (13) (14)
CanMi = f m 2 INkjm ·Ci mi; p 2 Ci ) mi(p) · r ¡ 1;
r = minri frijpre(p; ti) = ri; ti 2 p²g g where m ·Ci mi ,df 8p 2 Ci : m(p) · mi(p).
We can de¯ne the notion
CovT = fCijCi µ P; Ci is total cover of Tg Based on the CovT we may de¯ne now the overall set of dead markings CanM = nm 2 INkj9Ci 2 CovT : m ·Ci mi; p 2 Ci ) mi(p) · r ¡ 1; r = minri frijpre(p; ti) = ri; ti 2 p²g (15) (16) Notice that notions CanMi and CanM are based only on the structure of PN in question and nothing is known about the reachability of the states contained there. That is why we have used to call them 'deadlock candidates', or potential deadlock states. Any of such the states becomes real deadlock provided it is reachable, the issue connected with dynamic aspect of the PN in question. Now we are prepared to formalize the procedure, based on the method developed so far, as far as deadlock analysis is concerned. We do it in the form of a procedure.
DA(N0):Algorithm for doing the deadlock analysis of Nets (P/T nets). Input:
Petri Net (P/T net) N0 = (P; T:pre; post; m0), of the type Mw of PN N0 Output: yes, if D(N0) 6= © no, if D(N0) = © Method:
Method is based on the results achieved in the analysis of nature of !coordinates, that occur in ! macrostates ½ = !Aq. Approach is based on interpretation of any such ! macrostate ½ = !Aq as a representaion of the poset of reachable states in PN N0, having minimal or the least elements (MoL states). The special procedure CanM(N0 ) is used for creation of the set of potential deadlocks of PN N0.
Body of the algorithm:
The algorithm DA(N0) guarantees all MoL deadlocks will be found out and delivered as the set D(N0). Actually that can be considered as solving the problem of discovering presence or absence of deadlock states in the PN N0. 5.2
We can now continue to analyze state diagrams of the two PNs. We wil use the results of previous section and particularly the result of the Lemma ??. So according to that we have to calculate now total covers for the two PNs. In the tables below there are calculated both:the minimal total cover of T and pre-set for the net N1.
Total Cover of T for PN N1 Function pre for PN N1
t1 t2 t3 t4 Total Cover of T pre p1 p2 p3 p1 _ _ C1 = fp1; p2g t1 1 p2 _ _ t2 1 p3 _ _ t3 1
t4 1 Can M = Can M1 = f0; 0; !g
inf (1; 0; !01) = (1; 0; 0) 2= CanM inf (0; 1; !0;1)
nejestvuje
Base((0; 1; !0;1)) = f(0; 1; 0); (0; 1; 1)g \ CanM = f(0; 0; !)g = © So we jump to the conclusion that PN N1 does not contain any deadlock!
Now we are going to turn our attention to the PN N2. First we calculate minimal total cover of PN N2 and pre-set for the PN N2.
Total Cover of T for PN N2 Function pre for PN N2
t1 t2 t3 t4 Total Cover of T pre p1 p2 p3 p1 _ _ C1 = fp1; p2g t1 1 p2 _ _ C2 = fp1; p3g t2 1 1 p3 _ _ _ t3 1 2
t4 1 1 CanM1 = f(0; 0; !)g ; CanM2 = f(0; !; 0)g
CanM = f(0; 0; !); (0; !; 0)g Base((1; 0; !02;;1¡)) = f(1; 0; 0); (1; 0; 1)g Base((0; 1; !0;2)) = f(0; 1; 0); (0; 1; 2)g
Base((1; 0; !02;;1¡)) \ CanM = © Base(0; 1; !0;2) \ CanM = f(0; 1; 0); (0; 1; 2)g \ f(0; 0; !); (0; !; 0)g = f(0; 1; 0)g
So we may jump to the conclusion that PN N2 has indeed deadlock state f(0; 1; 0)g!
The issue of deadlock analysis is important for the development of discrete
statebased systems. The method of discovering a presence, or an absence of deadlocks
in the system coined and demonstrated in the paper is based on the study
of the properties of the automaton Mw. We should mention that the results
presented in the paper manifest the depth and the vitality of the new method
to deal with the issue of reachability in Petri Nets, particularly the part which
was connected with the study of the algebraic properties of interpretations of
the automaton of the type Mw. In [
Due to space we have not dealt with the issue of modi¯cation of the
algorithm of M construction, and also many details and proofs have been skipped.
There can be found in [
Acknowledgments. This work was supported by the Slovak Research and Development Agency grant on Modelling, simulation and implementation of GPGPU-enabled architectures of high-throughput network security tools,under the contract No. APVV-0008-10. Further it was also partially supported by the grants No. 1/3140/06 of the VEGA-The Scienti¯c Grant Agency of Slovakia, NATO CLG982698 grant, APVV grants No.APVV-0073-07, and SK-UA-002607.