Introduction

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 specification is about. There are two intrinsic activities of any development: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 verification process. In the paper we pay attention to the deadlock analysis.

The approach to deadlock analysis applied in the paper is based on the reachability 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 automaton of the type M w , 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 M w . 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 M w , and thus hidden in it. The modification of M w 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 concerned Petri Nets, reachability and deadlock analysis are given. The second part deals with the algebraic properties of M w . It turns out that M w is finite 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 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 introduced 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, Z k (IN k ) the set of k-dimensional (nonnegative)integer vectors. A notion of (k-dimensional) vector addition system (VAS) W k is a couple W k = (q 0 , W ) where q 0 ∈ IN k is the initial state of W k , W is a finite set of (k-dimensional integer) vectors. We call a reachable state vector of W k each q ∈ IN k such that 1. q = q 0 + w i1 + . . . + w in for some integer n ≥ 0, w ij ∈ W, j = 1, . . . , n and 2. for ∀j(1 ≤ j < n) :

q j = q 0 + w i1 + . . . + w ij ∈ IN k

Here by + we mean the operation of vector addition. We call the set of all such vectors the reachability set of VAS W k , and denote it as R(W k ). Given any VAS W k = (q 0 , W ) then or any q ∈ IN k a problem whether q ∈ R(W k ) is called the reachability problem of VAS (with respect to q). We will occasionally use the abbreviation RP (q, W k ) for it.

With any VAS W k = (q 0 , W ) we can associate a tree structure, which we call the vector state tree, V ST w , and we mean by that a double labelled oriented rooted tree V ST w = (T w , Lab(V ), Lab(E), q 0 ),

T w = (V, E, r 0 ) is an oriented rooted tree , V -a set of vertices, E ⊆ V × V -a set of edges, r 0 ∈ V -the root of T w , Lab(V ) ⊆ IN k -a set of vertex labels, Lab(E) ⊆ W -a set

of edge labels that are defined as follows: there are two labelling mappings lab 1 : V → Lab(V ), lab 2 : E → Lab(E) such that lab 1 (r 1 ) = q 0 and any vertex of

T w v ∈ V with lab 1 (v) = q has a son u ∈ V with lab 1 (u) = q and lab(v, u) = a iff q = q+a.

As a very consequence of the above definition we have that Lab(V ) = R(W k ) where W k = (q 0 , W ) is the VAS and we can alternatively write V ST w = (T w , R(W k ), Lab(E), q 0 ) 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 details on PN we refer the reader to the literature , e.g. [8]. For any P/T net N 0 = (P, T, pre, post, m 0 ), 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 −→ INpostset 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 P = {p 1 , p 2 , p 3 , p 4 , p 5 } T = {t 1 , t 2 , t 3 , t 4 }

pre and post functions are given in Table 1 and Table 2 respectively. In Fig. 2 there is a correspondence shown between the graph representation of PN N and pre and post functions. The following useful notations can be defined:

• t = {p | pre(p, t) = 0} the set of preconditions of t t • = {p | post(p, t) = 0} the set of postconditions of t p • = {t | pre(p, t) = 0} • p = {t | post(p, t) = 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) = 0. Without loss of generality we assume that P and T have k and m elements respectively.

i.e. P = {p 1 , p 2 , , ..., p k }, T = {t 1 , t 2 , , ..., t m } 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. and m(p i ) is the value of m in p i , i = 1, 2, ..., k, according to (1). In our example (Fig. 1) m(p i ) = 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 t 1 is enabled in m = (1, 0, 0, 0, 0) because • t 1 = {p 1 } and m(p 1 ) = 1, and pre(p 1 , t 1 ) = 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 m that depends on m and t. We use a denotation m t m and m is defined in the following way:

m (p) =        m(p) − pre(p, t) p ∈ • t \ t • m(p) + post(p, t) p ∈ t • \ • t 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) t 1 m = (0, 1, 1, 1, 0). Notice transitions t 3 ,t 4 will be enabled in m either. We say the sequence of transitions σ = t 1 t 2 ...t r is admissible firing sequence in PN N, provided a sequence of markings m 0 , m 1 , ..., m r exists and such that m i−1 t i m i , i = 1, 2, ..., r. In that case we write m 0 σ m r , or simply m 0 m r , when σ is immaterial. The marking m is to be called the reachable marking in N from m 0 (via σ). We fix the marking m 0 to be the initial marking of PN N = (P, T, pre, post) and we denote it N 0 = (N, m 0 ) or N 0 = (P, T, pre, post, m 0 ). Given PN N 0 = (P, T, pre, post, m 0 ) we define the set of reachable markings

R(N 0 ) = {m | m 0 σ m, },

We can define the language of PN N 0

L(N 0 ) = {σ ∈ T * | m 0 σ m, σ ∈ T * }

and we call it PN language.

Verification of Systems: Deadlock Analysis Based on Petri Nets 2.2 VAS and Petri Nets.

Let N 0 = (P, T, pre, post, m 0 ) be a Petri Net with the initial marking m 0 . Recall m 0 can be represented as a k-dimensional nonnegative integer vector, i.e. m 0 ∈ Z k and m 0 = (m 0 (p 1 ), . . . , m 0 (p k )). Let us fix an ordering of places in P and transitions in T, i.e. P = {p 1 , . . . , p k } and T = {t 1 , . . . , t m }.

In PN literature (e.g. [6], [8]) we have the following characterization of the marking obtained (reached) in N 0 from initial marking m 0 under firing transition

sequence σ ∈ T * m 0 σ m ⇔ m = m 0 + (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 It can be easily seen that

m 0 t m ⇔ m = m 0 + t

and we can construct for PN N 0 = (P, T, pre, post, m 0 ) the vector addition system W k = (q 0 , W ) an such that q 0 = m 0 , W = {t|t ∈ T } , and k = cardP . The following result holds

Theorem 1. [6]

For any PN N 0 = (P, T, pre, post, m 0 ) there is an vector addition system W k = (q 0 , W ) and such that R(W k ) = R(N 0 ), and k = cardP . Proof:That follows from the above construction.

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 solution 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.

1. Any P/T net N 0 = (P, T, pre, post, m 0 ) can be assigned a vector adition system (VAS) W k = (q 0 , W ) via a representation of transitions of P/T net N 0 as vectors, where W = → t i |t i ∈ T , (q 0 = m 0 ) and

→ t i = (post(p 1 , t i ) − pre(p 1 , t i ), ..., post(p k , t i ) − pre(p k , t i )), provided P = {p 1 , ..., p k }.

By that virtue the computations of P/T net N 0 are in 1-1 correspondence with computations of the VAS W k and R(W k ) = R(N 0 ) (see Theorem 1). The computations of the VAS W k can be represented via rooted labelled tree, termed as vector state tree -V ST w , whose vertices are labelled by reachable states and edges are labelled by vectorized transitions. 2. Given V ST w and its vertex with the label q, it can be characterized by two languages:X q , Y q , preffix and suffix language respectively / which denotes labelling of paths leading to or from the vertex with the label q. The paths on V ST w 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 vectorstates: vertex labellings on the other side. Any path on V ST w , outgoing from the root vertex r 0 , labelled by q 0 , can be assigned a sequence of its vertex labels (reachable) vector-states

s = {q 0 , q 1 , ..., q i , ...}(3)

The states in (3) are reachable states, that are vectors, i.e. q i ∈ N k (k=||P ||), so for any pair of states in ( 3)-(q i , q j ), i < j, we can test their comparability, 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

q i ≤ q j ⇒ Y qi ⊆ Y qj(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 transforming the tree into a rooted graph (vector state graph-vsg). The transformation (T < m A ) has a significant property that suffix language of the root of the original V ST w − Y q0 is included in the suffix language of the root of the resulting vsg

T < m A (q 0 ), i.e. Y q0 ⊆ Y T < m A (q0

) . In the case the strong inequality holds between the two states on the path (q ≤ q and q = q ), that causes introducing so-called ω-cordinates, that means replacing the cordinates of the both states in which the strong inequality (<) holds, by the special value ω, and thus creating the ω-lized state ω A q and ω A q , that become identical, i.e. ω A q = ω A q (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 effect: pruning the infinite path by replacing it by a finite (loop-like) subgraph, and lowering number of coordinates w.r.t. which a comparison satisfiability of reachable (macro) states should be checked. That guaranties that in a finite number of transformation steps a finite (rooted) vsg structure T ω f can be obtained. The significant property of the vsg T ω f is that Y T * (q0) ⊇ Y q0 , provided that T * (q 0 ) is the macrostate on which the initial state q 0 is mapped after the sequence of transformations denoted as T * . 3. Vsg T ω f can be thought of as a special kind of finite state automaton (fsa) with some interpretation of its states, and with the input alphabet W = → t i |t i ∈ T . The definition of the automaton (we used to call it finite state automaton (fsa) (of the type) M w ) can be given as

M w = (Q f , W, δ, ρ 0 ), provided the vsg T ω f = (Q f , T f ,

ρ 0 and T f is the graph representation of state trasition funcion δ. To characterize the behaviour of fsa M w 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 M w (i.e.L(M w )= [[ L ρ0 ]] ), and q 0 to be the initial state of VAS W k . Then [q 0 L ρ0 ] denotes all reachable states. To be more precise will differ depending on whether R(N 0 ) is finite or infinite. In the finite case RP (q, N 0 ) can be solved trivially by inspecting the state diagram of M w 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 find a state ρ of M w such that q ≤ ρ; if such a state does not exists, then RP (q, N 0 ) has negative solution (q / ∈ R(N 0 ) ).

[u] = [u] if u ∈ W [au] = a + [u] if a ∈ W and u ∈ W * ∀q ∈ N k , u ∈ W * [qu] = q + [u] and ∀i(1 ≤ i ≤ |u i |).q i = [qu i ] ∈ N k , [q 0 L ρ0 ] = q |q = [q 0 u] , u ∈ [[ L ρ0 ]](5) 4

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 q 0 under chain of transformations (ρ = T * < m A (q 0 ))(for more details see [6]). By that way a wre u over the alphabet W L ∪ W (W L is the alphabet of (ρ 0 )-simple loops of scc, i.e. W L ⊆ W * ) can be constructed, yielding the equation

[q 0 uv] = q (6)

Wre u (under assumption of one scc in M w , rooted in ρ 0 ) has the structure u = 1 2 ... p , where i ∈ W L , i = 1, 2, ..., p and v is a path leading from ρ 0 to ρ such that q ≤ ρ. -The equation ( 6) yields integer linear programming problem (ILP)

AX = B(q), B(q) = q − q 0 − [v](7)A = ([ 1 ] T , [ 2 ] T • • • [ m0 ] T ) provided W L = { 1 , 2 , .

.., m0 }. 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 definition of [q 0 uv](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 con Wk (A, X 0 , B 0 ). So finally the RP algorithm is RP algorithm: Given: VAS W k = (q 0 , W ), q ∈ IN k -a state to be decided reachable or not;

Step 1 : Create fsa M w ;

Step 2 : Construct M ILP w (A, X 0 , B(q), r);

Step 3 : if M ILP w (A, X 0 , B(q), r) = true then go to Step 4 else go to Step 5 ; Step 4 : q ∈ R(W k ). Stop.

Step 5 : q ∈ R(W k ). Stop.

We use the abbreviation

M ILP Wk (A, X 0 , B(q)) ≡ ILP Wk (A, X 0 , B(q)) ∧ con Wk (A, X 0 , B 0 ) Finally RP (q, W k ) ≡ M ILP Wk (A, X, B(q))

Since ILP is decidable, and also due to finiteness of X 0 establishing truth of con Wk (A, X 0 , B 0 ) is also decidable, so is the reachability problem.

3 Algebraic properties of M w automaton

Let us have one more look at fsa M w = (Q, W, δ, ρ 0 ). For simplicity let us assume that M w consists of single scc with its root state ρ 0 . Example of such M w is depicted in Fig. 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 M w 's state diagram is that they are mutually incomparable as vectors. We can look at labels of the states of the M w '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 M w 's state diagram, as the reachable macrostate. We will say that 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 ρ = {q|q ∈ R(N 0 ), q ≤ ρ} S ρ is simply partially ordered set(poset). The notion is well-known [19]. For any poset, particularly for S ρ , there can be found the set of minimal, or maximal elements (states) respectively. The notions the lower bound, or the upper bound of the states of S ρ are also well defined and used. The notion the greatest lower bound (glb), and the least upper bound (lub) are also used in that context. We only mention here, that while minimal (maximal) states belong to S ρ , that might not be true for glb or lub respectively. We will use the notation , to denote the binary operation of calculating lub(q, q ) = q q , or glb(q, q ) = q q respectively.

For the definition of poset, and further properties and other results reader can consult a specialized literature on the subject, e.g. see [18], [19].

For our purpose to use the information captured in fsa M w for deadlock analysis we have to modify the algorithm of creating M w . The information that is hidden in the state diagram of M w is the value of particular coordinate of the state q at the moment when the coordinate is being ω-lized. . To capture the information hidden (and lost) by the original algorithm to construct the fsa of the type M w , 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 ω , -ω i,t,∆j b -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(p i , t) for the transition t to be firable 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 overflowed ω coordinate with the minimal initial value of the coordinate at the time it was overflowed for the first time.

To get a flavour why we are introducing indexed ωs , we are now turning our attention to properties of the poset S ρ = (S ρ , ≤, , ) 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 ρ , ≤, , ) . For the discovering a deadlock state of P/T net N 0 we would like to make a use of information captured in the M w 's state diagram, specifically in macrostates by which the states are labelled with.

Assume that we are given ω-state ρ, and to be more specific, let's say that

ρ = ω A q = (ρ 1 , ρ 2 , ..., ρ k )(8)

where q = (q 1 , q 2 , ..., q k ) is a reachable state, A ⊆ {1, 2, ..., k} = K is the set of indices in which ρ has ω -coordinates. To put it in other words that means that

ρ j = if j ∈ A q j if j / ∈ A and ∈ ω ∆i a , ω i,t,∆j b

, ω c .

Verification of Systems: Deadlock Analysis Based on Petri Nets

Now we are introducing some notions.

First we fix the macrostate ρ and its representation (8). We define

Baseρ = { q B ρ,i = q 1 , q 2 , ..., q k |i ∈ A, q = ρ if i = , ∈ K − {i} , (9)q i = r if ρ i = }

where ∈ ω ∆i r , ω j,t,∆i r

, ω r .

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 ||A|| > 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 M w 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 define

q B ρ = q 1 , q 2 , ..., q k (10)

where

q j = r ⇔ ρ j = q j = ρ j ⇔ ρ j ∈ N and ∈ ω ∆j r , ω i,t,∆j r

, ω r for some r ∈ N.

It is clear that

q B ρ ≤ ρ The crucial problem is to decide whether q B ρ is reachable state or not. In the latter case it will be called spurious state [1]. We will postpone answering that question later on.

Any deadlock state of P/T net N 0 = (P, T, pre, post, q 0 ) is such a state q, that is 1. reachable state, i.e. q ∈ R(N 0 ), and 2. for any transition t ∈ T and at least one p ∈ • 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 ∈ T . Assume we have a deadlock state d ∈ ρ; that means that any reachable state q ∈ ρ and such that q ≤ d will be a deadlock state either. From that we have immediately, that if q B ρ were reachable state, it would be a deadlock state of P/T net N 0 = (P, T, pre, post, q 0 ) 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 ρ , ≤, , ) be the poset formed by the macrostate ρ of the fsa M w representing the set of reachable states of a P/T net N 0 = (P, T, pre, post, q 0 ). Then if there exists a deadlock state d in ρ, then at least one of minimal elements or the least element of the poset S ρ -q min will be the deadlock state too and such that q min ≤ 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 M w [6] we apply some transformations to the paths of the tree of computations of the VAS W k = (q 0 , W ), which results in introducing ω values into corresponding coordinates of a state vector. We have shown above there are three types of ω coordinates (ωcords in short):independent, dependent and overflowed ωcords.

The issue of creating independent ω coordinate is depicted in Fig. 4.

Fig. 4. Path transformation creating independent ωs

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 t a and t b that are firable (applicable) in q. An aplication of t a at q followed by other transitions leads to a state q = (q1, ...a , ..., b, ...q k ) , where a < a is a new value of the i-th coordinate, and according to the algorithm which construts automaton M w the transformation T <i applies, that creates a loop labelled with the string τ a = t a α, that replaces the path leading from q to q which is labelled with τ a = t a α as well. The effect of the transformation is that the state q collapses to q creating a new state ω {i} q = (q1, ..., ω, ..., b, ...q k ). 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 coordinate. 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 = t a α. After all we prefer to denote the new ω value of the i-th coordinate by ω ∆i a , and to call such the ωcoordinate to be independent ωcoordinate. Another independent ωcoordinate can be created due to firing the sequencce of transitions τ b = t b β starting at the state ω {i} q. Notice that in the intermediate state p in the i-th coordinate so called overflowed ω 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 [7].

Analysis of creating ωcoordinates

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 ∈ Baseρ; then q B ρ,i ⊆ (N 0 ) and thus q B ρ,i is a macrostate covering a set of reachable states which all have the same i-th coordinate, say a i . Moreover, the macrostate q B ρ,i is the macrostate consisting of minimal states wrt macrostate ρ. The nature of the fsa of the type M w [6] guarantees nonemptiness of q B ρ,i . The latter guarantees an existence of at least one reachable minimal element belonging to the macrostate q B ρ,i . 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 first.

The case analysis of different types of n > 1 ωcoordinates have been accomplished [7]. In every case there that has been proven, that either Baseρ ⊆ (N 0 ), or q B ρ ∈ (N 0 ). The case of n=2 ωcoordinates is quite simple. The case of n ≥ 3 is more complicated. There is few typical situations in the case of n=3 ωcoordinates that shows the table below.

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). The results on creating ωcoordinates for the case ||A|| ≤ 3 can be generalized to any n ∈ N. The conclusion we have come to is that ωcoordinates can assume one of the following forms. We propose to use a generalized form to represent ωcoordinates, and we will call it as form (f).

ω h 1 , • • • h k d 1 , • • • d k(11)

where

h 1 d 1 ∈ ∆ i a , A, t, ∆ i b h i d i i>1 ∈ − a , λ c(12)

Here λ stands for empty symbol. Basically, in the case of overflowed ω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 as

ω [I k ] where I k = h 1 , • • • , h k d 1 , • • • , d k

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.

A case study and further analysis of ωcoordinates

In his paper [1] T.Murata studied two PNs (Fig. 5) with respect to discovering liveness or deadlock, based on the coverability graphs of Petri Nets, the structure that is widely used to represent the state space of their reachable states. He showed that two PNs having the identical coverability graphs differ what concerns of liveness or deadlock properties. In this section we will use our method based on the finite automaton M w and the properties of ωcoordinates to demonstrate the power of the approach to discover safely the deadlock of Petri nets in general and it will be demonstrated by the example Petri nets by T. Murata. Let us have a closer look at the two PNs. Comparing coverabiity graphs of the two PNs we can see they are indeed identical. Now we are going to apply the aproach based on the methodology developed, that is backed by our algorithm of constructing fsa of the type M w (in some cases state diagrams of M w and coverability graph coincide, but in some cases they look quite different). Construction of fsas of the type M w fo the two nets can be seen in Fig. 6 and Fig. 7. We can see that M w automata are isomorphic, but they differ in ωcords as far as their indices are concerned.

Let us have a closer look at the M w automata from that perspective. In M w automaton of PN N 1 we have two macrostates: ρ 1 = (1, 0, ω 1 0 ) and ρ 2 = (0, 1, ω 0,1 ). If we look at ρ 1 = (1, 0, ω 1 0 ) as at the poset, we can have the only minimal and thus the least (infimum) state q B ρ1 = (1, 0, 0) In the case of ρ 2 = (0, 1, ω 0,1 ) we have the basis of this poset Base(ρ 2 ) = {(0, 1, 0), (0, 1, 1)} There are actually 2 minimal states. Let us turn our atention to the net N 2 . In M w automaton of PN N 2 we have also two macrostates: ρ 1 = (1, 0, ω 2,− 0,1 ) and ρ 2 = (0, 1, ω 0,2 ). If we look at ρ 1 as at the poset, we can have here no infimum state, but we still have two minimal states that creates :

Base(ρ 1 ) = {(1, 0, 0), (1, 0, 1)} Fig. 6. Mw construction for the live Petri Net N1 with inexed ωcords

If we look at ρ 2 as at the poset, we can have also here no infimum state, but we still have two minimal states that creates :

Base(ρ 2 ) = {(0, 1, 0), (0, 1, 2)}

Deadlock analysis

In [6] the deadlock problem is dealt with, based on the use of original RP algorithm. We wil use of the notion 'deadlock candidates' states introduced there. The latter can be derived from the structure of PN in question.

Let us consider PN N = (P, T, pre, post) and let

→ t = − → pre(p, t) + → post(p, t).

For any t ∈ T and p ∈ P we say

p covers t ⇔ df pre(p, t) = 0(13)

In other words we are saying by ( 13) that

p covers t ⇔ df t ∈ p •(14)

The ( 13) and ( 14) simply mean that p is included in t's enabling. That is reasonable to define Obviously C(p) = p • . We are now looking for such a minimal subset C i of P, that the union of the covers of places form the subset that will give the whole set T. We propose to call such the subset C i the minimal cover of T. The notion minimal is connected with the number of places covering the set T. Notice, there can be more than one minimal cover of T.

C(p) = {t ∈ T |p covers t}

We associate with each total cover of T -C i , the set of deadlock markings, denoted as -CanM i .

CanM i = { m ∈ IN k |m ≤ Ci m i , p ∈ C i ⇒ m i (p) ≤ r − 1, r = min ri {r i |pre(p, t i ) = r i , t i ∈ p • } } where m ≤ Ci m i ⇔ df ∀p ∈ C i : m(p) ≤ m i (p).

We can define the notion

CovT = {C i |C i ⊆ P, C i is total cover of T}(15)

Based on the CovT we may define now the overall set of dead markings

CanM = m ∈ IN k |∃C i ∈ CovT : m ≤ Ci m i , p ∈ C i ⇒ m i (p) ≤ r − 1, r = min ri {r i |pre(p, t i ) = r i , t i ∈ p • }(16)

The algorithm DA(N 0 ) guarantees all MoL deadlocks will be found out and delivered as the set D(N 0 ). Actually that can be considered as solving the problem of discovering presence or absence of deadlock states in the PN N 0 .

Case study continued

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 N 1 .

Total Cover of T for PNN 1 t 1 t 2 t 3 t 4 Total Cover of T p 1 ∨ ∨ C 1 = {p 1 , p 2 } p 2 ∨ ∨ p 3 ∨ ∨ Function pre for PN N 1 pre p 1 p 2 p 3 t 1 1 t 2 1 t 3 1 t 4 1 Can M = Can M 1 = {0, 0, ω} inf (1, 0, ω 1 0 ) = (1, 0, 0) / ∈ CanM inf (0, 1, ω 0,1 )

nejestvuje Base((0, 1, ω 0,1 )) = {(0, 1, 0), (0, 1, 1)} ∩ CanM = {(0, 0, ω)} = Φ So we jump to the conclusion that PN N 1 does not contain any deadlock! Now we are going to turn our attention to the PN N 2 . First we calculate minimal total cover of PN N 2 and pre-set for the PN N 2 . CanM 1 = {(0, 0, ω)} , CanM 2 = {(0, ω, 0)} CanM = {(0, 0, ω), (0, ω, 0)} Base((1, 0, ω 2,− 0,1 )) = {(1, 0, 0), (1, 0, 1)} Base((0, 1, ω 0,2 )) = {(0, 1, 0), (0, 1, 2)} Base((1, 0, ω 2,− 0,1 )) ∩ CanM = Φ Base(0, 1, ω 0,2 ) ∩ CanM = {(0, 1, 0), (0, 1, 2)} ∩ {(0, 0, ω), (0, ω, 0)} = {(0, 1, 0)} So we may jump to the conclusion that PN N 2 has indeed deadlock state {(0, 1, 0)}!

Total

Conclusion

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 M w . 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 M w . In [6] there are some results presented on the nature of that interpretation. The automaton M w bears some similarity with coverability graphs used in Petri Nets, but as it was proven, it is more powerful to deal with deadlock analysis. Beside of that, the structure of the automaton M w plays the central role in reachability analysis of the systems (represented via PN) with infinite state space [6]. The most important property of M w is its reusability for reachability analysis of the PN in question wrt to any other state, not only wrt to that it was constructed for initially. On the other side it turns out that one automaton of the type M w , say M can serve in that role for whole class of PNs with the same number of places and some structure that induces corresponding set of transitions wich are consistent with the M structure. There is still another way how the M w structure can be used. The fsa M can be thought of as a couple M=(M,I), where M and I stand for basic fsa without interpreted states and interpretation respectively. For any k ∈ IN-the number of places and given structure of basic fsa M we can construct corresponding interpretation I consistent with M. By that virtue, the same applies wrt doing deadlock analysis.

Due to space we have not dealt with the issue of modification of the algorithm of M construction, and also many details and proofs have been skipped. There can be found in [7]. At the workplace of the author there has been environment -termed as mFDTE [16], developed. The results will be implemented in the environment. The latter combines three formal descriptions of systems: Petri Nets, process algebra, and B AMN. The latter substantiate the acronym mFDTE-multi Formal Description Techniques Environment. More details can be found in [16].