=Paper= {{Paper |id=None |storemode=property |title=Verification of Systems: Deadlock Analysis Based on Petri Nets |pdfUrl=https://ceur-ws.org/Vol-848/ICTERI-2012-CEUR-WS-SMSV-paper-5-p-321-343.pdf |volume=Vol-848 |dblpUrl=https://dblp.org/rec/conf/icteri/Hudak12 }} ==Verification of Systems: Deadlock Analysis Based on Petri Nets== https://ceur-ws.org/Vol-848/ICTERI-2012-CEUR-WS-SMSV-paper-5-p-321-343.pdf 
               Verification of Systems:
        Deadlock Analysis Based on Petri Nets

                                   Štefan Hudák

                     Department of Computers and Informatics
                              FEI TU 04011 Košice,
                            Letná 9, Slovak Republic,
                           e-mail:stefan.hudak@tuke.sk



      Abstract. T he present work is devoted to the study of deadlock prob-
      lem 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 verification, so the
      results achieved can be of some value to that. It is demonstrated that
      results presented are quite significant, and cover some gap in both, theory
      and practice of the deadlock analysis of state-based systems, particularly
      those whose specification can be expressed via Petri Nets.


      Keywords. Place/Transition Nets, deadlock analysis, reachability, fi-
      nite state representation of the state reachability set, finite state au-
      tomaton of the type Mw .


      Key Terms. Mathematical Model, Specification Process, Verification
      Process


1   Introduction
In the development of (state-based) system, the design of a system in ques-
tion, is the core of the process. The latter is actually a realization of the what
requirement specification is about. There are two intrinsic activities of any de-
velopment:validation and verification. The validation is the process of assurance
that the design will produce the right system (according to requirements), while
the verification assures that the design is carried on properly (according to a
particular design principle)[21]. Verifying the system designed on the presence
(absence) of deadlock situations (deadlock analysis-DA) might be a part of ver-
ification process. In the paper we pay attention to the deadlock analysis.
322                                                                          Š. Hudák


The approach to deadlock analysis applied in the paper is based on the reach-
ability analysis [6] made on the representation (model) of the system designed
in Petri Nets [8]. In [6] an original method (algorithm) to analyze and solve the
reachability problem (RP) for Petri Nets in general case was introduced. The
method is based on the structure, we have called it the finite state automa-
ton of the type Mw , that is created by the algoritm, and the analysis of the
structure based on results of automata theory and the convex analysis of the
state space represented by Mw . Some authors in the field of Petri Nets used to
use for representing state space of reachable states of Petri nets the structure
termed as coverability graph. The two notions coincide to some extent, but differ
in significant number of cases.
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 modification
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 first part basic notions and results con-
cerned Petri Nets, reachability and deadlock analysis are given. The second part
deals with the algebraic properties of Mw . It turns out that Mw is finite state
automaton, with some interpretations of its states via k -dimensional nonega-
tive 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 informa-
tion previously hidden, and define 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 in-
troduced by T.Murata [1] as manifestation of the fact, that using coverability
graphs as the representation of state space of PN is weak and insufficient for
disclosing deadlocks in PN. The same conclusion was jumped to in [2].


2     Some basic preliminaries to DA
In the paper we denote by IN the set of natural numbers {0, 1, 2, . . .}, 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 ∈ INk is the initial state of Wk , W is a finite set of (k- dimensional
integer) vectors. We call a reachable state vector of Wk each q ∈ INk such that
 1. q = q0 + wi1 + . . . + win for some integer n ≥ 0, wij ∈ W, j = 1, . . . , n
    and
 2. for ∀j(1 ≤ j < n) : qj = q0 + wi1 + . . . + wij ∈ 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
Verification of Systems: Deadlock Analysis Based on Petri Nets                    323


Wk = (q0 , W ) then or any q ∈ INk a problem whether q ∈ 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 ∈ V - the
root of Tw , Lab(V ) ⊆ INk -a set of vertex labels, Lab(E) ⊆ W - a set of edge
labels that are defined 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 ∈ V
with lab1 (v) = q has a son u ∈ V with lab1 (u) = q 0 and lab(v, u) = a iff q 0 = q+a.
    As a very consequence of the above definition 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 Nets (P/T Nets).

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 de-
tails on PN we refer the reader to the literature , e.g. [8]. For any P/T net
N0 = (P, T, pre, post, m0 ), where P is a finite set of places, T is a finite set of
transitions, pre : P × T −→ IN - preset function, and post : P × T −→ IN -
postset function, that all define a structure on the set P ∪ T . It is very common
to represent the P/T Net /1 by the oriented bipartite graph (Fig. 1).
 Here we have:




                       Fig. 1. Graph representation of Petri Net

1
    We will use Petri Net (PN) occasionally instead of P/T Net, so we consider them as
    synonyms
324                                                                     Š. Hudák


                              P = {p1 , p2 , p3 , p4 , p5 }
                               T = {t1 , t2 , t3 , t4 }
pre and post functions are given in Table 1 and Table 2 respectively.

      Table 1:                     Table 2:
      P T pre(p,t)                 P T post(p,t)
      p1 t 1   1                   p1 t 2    1
      p2 t 2   1                   p2 t 1    1
      p5 t 2   1                   p3 t 1    1
      p3 t 3   1                   p4 t 1    1
      p4 t 4   1                   p4 t 3    1
                                   p5 t 4    1
      otherwise     0              otherwise 0



    In Fig. 2 there is a correspondence shown between the graph representation
of PN N and pre and post functions.




Fig. 2. The correspondence between the graph representation of PN and the pre and
post functions



      The following useful notations can be defined:
      •
        t = {p | pre(p, t) 6= 0} the set of preconditions of t
      t• = {p | post(p, t) 6= 0} the set of postconditions of t
      p• = {t | pre(p, t) 6= 0}
      •
        p = {t | post(p, t) 6= 0}
By the marking of PN N = (P, T, pre, post) we mean a totally defined function

                                   m : P −→ IN                                (1)
                                                                              (2)

    We use m to describe the situation or configuration in PN N . Namely we say
the condition represented by the place p in PN N holds iff m(p) 6= 0. Without
loss of generality we assume that P and T have k and m elements respectively.
Verification of Systems: Deadlock Analysis Based on Petri Nets                     325

i.e. P = {p1 , p2 , , ..., pk }, T = {t1 , t2 , , ..., tm } and we fix 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 ∈ 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 iff 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 , iff for every p ∈• t, m(p) ≥ pre(p, t). In Fig. 1 t1 is enabled
in m = (1, 0, 0, 0, 0) because • t1 = {p1 } 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 fire. The effect of the firing
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 defined in the following way:

                                                      p ∈ • t \ t•
                     
                      m(p) − pre(p, t)
                                                      p ∈ t • \• t
                     
                       m(p) + post(p, t)
                     
            m0 (p) =
                     
                      m(p) − pre(p, t)  + post(p, t) p  ∈ • 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 σ = t1 t2 ...tr is admissible firing 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 fix 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 define the set of reachable markings

                           R(N0 ) = {m | m0 σ m, },


We can define the language of PN N0

                     L(N0 ) = {σ ∈ T ∗ | m0 σ m, σ ∈ T ∗ }

   and we call it PN language.
326                                                                         Š. Hudák

2.2   VAS and Petri Nets.

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 ∈
Zk and m0 = (m0 (p1 ), . . . , m0 (pk )). Let us fix an ordering of places in P and
transitions in T, i.e. P = {p1 , . . . , pk } and T = {t1 , . . . , tm }.
   In PN literature (e.g. [6],[8]) we have the following characterization of the
marking obtained (reached) in N0 from initial marking m0 under firing transition
sequence σ ∈ T ∗

                             σ
                       m0        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 ∈ T can be represented as a k-dimensional integer vector

                                  t = post(t) − pre(t)

and
                      post(t) = ((post(p1 , t), . . . , post(pk , t)
                       pre(t) = ((pre(p1 , t), . . . , pre(pk , t))
It can be easily seen that

                                      t
                                 m0       m ⇔ m = m0 + t

and we can construct for PN N0 = (P, T, pre, post, m0 ) the vector addition sys-
tem Wk = (q0 , W ) an such that q0 = m0 , W = {t|t ∈ T } , and k = cardP . The
following result holds


Theorem 1. [6]
For any PN N0 = (P, T, pre, post, m0 ) there is an vector addition system Wk =
(q0 , W ) and such that R(Wk ) = R(N0 ), and k = cardP .
Proof:That follows from the above construction.



2.3   Reachability Problem

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 so-
lution to RP had been obtained [9],[10],[11],[12],[4]. A full account of the solution
of RP by the author, including the complexity issue of RP- the upper bound of
the worst-case time complexity of the solution, can be found in [6].
We are going now to describe shortly main steps of the author’s RP solution.
Verification of Systems: Deadlock Analysis Based on Petri Nets                           327

1. Any P/T net N0 = (P, T, pre, post, m0 ) can be assigned a vector adition
   system (VAS) Wk = (q0 , W n
                             ) via a representation of transitions of P/T net
                                      → o                              →
   N0 as vectors, where W = ti |ti ∈ T , (q0 = m0 ) and ti = (post(p1 , ti ) −
   pre(p1 , ti ), ..., post(pk , ti ) − pre(pk , ti )), provided P = {p1 , ..., pk }. By that
   virtue the computations of P/T net N0 are in 1-1 correspondence with com-
   putations of the VAS Wk and R(Wk ) = R(N0 ) (see Theorem 1). The com-
   putations of the VAS Wk can be represented via rooted labelled tree, termed
   as vector state tree - V STw , whose vertices are labelled by reachable states
   and edges are labelled by vectorized transitions.
2. Given V STw and its vertex with the label q, it can be characterized by two
   languages:Xq , Yq , preffix and suffix language respectively/ which denotes
   labelling of paths leading to or from the vertex with the label q. The paths
   on V STw can be classified, based on the length of the paths: finite and
   infinite, on the one side, and also based on the finite or infinite set of vector-
   states: vertex labellings on the other side. Any path on V STw , outgoing from
   the root vertex r0 , labelled by q0 , can be assigned a sequence of its vertex
   labels (reachable) vector-states

                                    s = {q0 , q1 , ..., qi , ...}                        (3)

   The states in (3) are reachable states, that are vectors, i.e. qi ∈ Nk (k=||P ||),
   so for any pair of states in (3)- (qi , qj ), i < j, we can test their comparabil-
   ity, w.r.t. the relation ≤ defined on vectors. (of the same dimension). The
   sequence (3) can be accompanied by the sequence of suffix(prefix) languages
   associated with the states of the sequence (3) . By the nature and due to
   properties of VASs and their computations that is clear that

                                   qi ≤ q j ⇒ Y q i ⊆ Y q j                              (4)

   The necessary and sufficient conditions can be formulated for a path being
   infinite with finite or infinite set of reachable states. Based on that a theory
   of transformation of infinite paths (a graph morphism), that allows pruning
   infinite paths and replacing them by loop-like subgraphs and thus transform-
   ing the tree into a rooted graph (vector state graph-vsg). The transformation
   (T