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