Dmitry A Zaitsev

Functional Petri Nets

Keywords: réseaux de Petri, réseaux fonctionnels, sous-réseaux fonctionnels, composition Petri net, functional net, functional subnet, composition

Nous introduisons dans ce travail les concepts de (sous-)réseaux de Petri fonctionnels et ceci afin de diminuer la complexité temporelle des méthodes d'analyse algébriques des réseaux de Petri. Nous montrons tout d'abord que tout sous-réseau fonctionnel s'obtient par composition de sous-réseaux fonctionnels minimaux. Puis nous proposons deux techniques de décomposition en sous-réseaux minimaux : via la résolution d'équations logiques ou à l'aide d'un algorithme ad-hoc dont la complexité temporelle est linéaire. Nous étudions ensuite les propriétés des sous-réseaux fonctionnels. Nous montrons que les invariants linéaires des réseaux de Petri s'obtiennent à partir des invariants de ses sous-réseaux fonctionnels ; des résultats similaires sont aussi valables pour l'équation fondamentale des réseaux de Petri. A partir de ces résultats nous développons une technique d'analyse de réseaux de Petri par décomposition en sous-réseaux fonctionnels. Nous démontrons que le calcul compositionnel d'invariants et de solutions de l'équation fondamentale conduit à une accélération importante des calculs. A l'aide d'une stratégie particulière de composition dite « séquentielle » nous obtenons une nouvelle accélération des calculs. La composition séquentielle est formalisée dans un contexte de théorie des graphes et se reformule sous le nom de repliage optimal d'un graphe pondéré. Finalement, nous appliquons nos techniques à l'analyse de modèles de protocoles standard de télécommunication comme ECMA, TCP, BGP.

Introduction

Linear algebra methods [Diaz 01,Murata 89,Reisig 82] based on state equation and invariants are a powerful tool for Petri net analysis. But to find linear invariants and to solve the fundamental equation of Petri net we have to solve linear diophantine systems in nonnegative integer numbers. All known methods of such systems solution [Colom 90,Contejean 97,Kryviy 99,Martinez 82,Schrejver 91,Toudic 82] possess exponential complexity with respect to space. It makes the analysis of large-scale models practically unfeasible and requires searching of new techniques, which provide essential speed-up of computations.

Two basic approaches were suggested [Berthelot 87] to handle large-scale nets: decomposition and reduction. Implementations of these approaches have been designed in the different concrete ways. Moreover, decomposition and reduction are applied not only to nets but to state space also. Reduction provides a set of rules for decreasing the dimension of net preserving its properties. Then usual methods of analysis are applied onto reduced net.

Decomposition and composition [Singh 86] are abstraction-based methods successfully applied in different fields of science and engineering. On the one hand the majority of artificial systems are composed out of its components and this process is hierarchical. So there is a decomposition of systems provided by the rules of its construction and the set of its components and elements [Cortadella 02,Girault 03,Jensen 97,Juhas 04]. The simplest way assumes the usage of such decomposition. If we know the properties of components and use special rules of composition (synthesis) preserving properties then we construct an ideal system [Juan 98,Kotov 84]. But unfortunately, it is not a prevailing case for real-life objects. On the other hand, the goals of concrete analysis often require tricky decomposition. Decomposition is justified if there are techniques allowing the determination of systems' properties on the base of properties of its components. Thus, decomposition methods always assume the following composition of system.

Let us consider approaches to decomposition used in Petri net theory. The first attempt was carried out by M. Hack [Hack 74] to decompose a free-choice net into state machines. The conditions for preserving of liveness under the composition of live state machines were studied. Berthelot [Berthelot 87] considered decomposition into S-and T-components: Scomponent shares transitions with other S-components whereas T-component shares places. Behaviour equivalence was studied. Esparza and Silva [Esparza 91] defined two special types of composition: synchronization and fusion. They considered synchronization preserving liveness of free-choice net. In [Best 92] the decomposition into T-components was applied for generation of home-states for free-choice nets. Results concerning the composition of freechoice nets were collected in the monograph of Desel and Esparza [Desel 95]. Kotov [Kotov 84] suggested composing Petri nets out of elementary nets using algebraic operations. Such nets were named regular nets. Regular nets consider separate sets of input and output places. Various kinds of composition preserving liveness, boundness and other properties were studied in [Christinsen 00, Lee 02, Lee 00, Souissi 90]. An incremental verification technique based on composition of subnets covering a formula of temporal logic was proposed in [Haddad 02].

In spite of variety of concrete definitions of components the common idea is clear enough: to pick out an interface of component and to hide its implementation [Peterson 81]. For Tcomponents composition is provided by fusion of contact places. Such a composition was used for construction of hierarchical high-level nets [Jensen 97,Juhas 04,Latvala 04,Pomello 04]. Nets containing contact places were also called IO-net [Juan 98]. At investigation of controllability of nets it was suggested to distinguish input and output places [Ichikawa 85]. Decomposition of reachability and coverability graphs was successfully applied for avoiding the state space explosion for low-level [Valmari 90] and for high-level [Haddad 96,He 91] Petri nets. Moreover, rules of state spaces composition at composition of net components were studied [Juan 98].

Functional Petri nets were introduced in [Zaitsev 97]. Like T-components, functional subnets define a partition of a set of transitions. But they distinguish from T-components and IO-nets: separate subsets of input and output places are considered and definition does not require that a place has only one input and only one output arcs. Moreover, among various suggested constraints for incident arcs of input and output places functional nets use the strictest: input places have only input arcs and output places have only output arcs [Zaitsev 03b].

Composition of Petri nets out of functional subnets [Zaitsev 04e] was applied successfully for speed-up of the processes of invariants' calculation [Zaitsev 04b] and solution of state equation [Zaitsev 04d]. It was shown that the majority of linear algebra methods of Petri net properties analysis, reducing to solution of systems of linear diophantine equations and inequalities in nonnegative integer numbers, might be efficiently realized with the aid of composition.

Note that application of composition [Zaitsev 04b,04d] allows the speed-up of solution of an arbitrary linear systems, which are solved usually with the aid of methods having the calculation complexity exceeding linear, as the complexity of decomposition and subsequent composition equals to linear function of dimension of system [Zaitsev 03b,04e]. However, the most significant speed-up we obtain at solution of diophantine systems in nonnegative integer numbers, as all known methods of such systems solution [Colom 90,Contejean 97,Kryviy 99,Martinez 82,Toudic 82] have exponential complexity.

In works [Zaitsev 04b ,04d], the simultaneous composition of all the functional subnets of a given Petri net was studied. However, in the cases the number of contact places exceed the number of places for largest of minimal functional subnets we may obtain an additional speed-up of computations at the expense of sequential organization of process of composition [Zaitsev 04g].This task is formalized in the terms of graph theory [Berge 01,Harary 71] and is named by collapse of weighted graph. The effective methods of its solution are proposed. Sequential composition has been applied for acceleration of verification of telecommunication protocols [Zaitsev 04c ,04f ].

The balance of the paper is the following: In Section 2, we introduce and discuss the concepts of functional Petri net and functional subnet. In Section 3, we study properties of functional subnets and consider the representation of decomposition with a net of functional subnets and a graph of decomposition. In Section 4, two different ways of decomposition are studied: with the aid of logical equations and using ad-hoc algorithm of linear complexity on size of the net. In Section 5, we describe the technique of composition-based calculation of linear invariants and show the exponential speed-up of calculations. In Section 6, we obtain analogous results for fundamental equation of Petri net. In Section 7, we propose to use sequential composition to provide an additional speed-up during solution of systems for contact places. Two ways of sequential composition using subgraphs and edges are discussed. Then we study in detail the edge sequential composition formalized as the task of edge collapse of the weighted graph. In Section 8, we present examples of invariants calculation via simultaneous and sequential composition of functional subnets for Petri net models of telecommunication protocols ECMA, TCP, BGP.

Concepts of Functional Petri Net and Functional Subnet

Concepts of a functional Petri net and a functional subnet are introduced for ordinary Perti nets. So they are applicable for various classes of Petri net using bipartite directed graph.

Multiplicity of arcs will be considered only at calculation of linear invariants and solution of the fundamental equation of Petri net. We use the special notations for the sets of input, output and incident nodes of a place:

}, ) , ( | { F p t t p ∈ ∃ = • , • . } } , ( | { F t p t p ∈ ∃ = • • • • = p p p U
Similarly we may define the sets of input, output and incident nodes of a transition and moreover of an arbitrary subset of places (transitions).

Definition 2. Net with input and output places

Net with input and output places is a triple ), , , (

Y X N Z =
where N is Petri net, -input places, -output places and the sets of input and output places are disjoint:

P X ⊆ P Y ⊆ ∅ = Y X I = .
Places from the set of Q we name internal. Input and output places C are named contact ones.

) ( \ Y X P U = Y X U
There are known also definitions [Ichikawa 85,Christinsen 00] of Petri nets with contact places which are not subdivided into input and output subsets.

Definition 3. Functional net

Functional net is a net with input and output places such that input places do not have input arcs and output places do not have output arcs:

. We denote functional net as or

∅ = ∈ ∀ • p X p :, ) , , , F T Y Q ∅ = ∈ ∀ • p Y p : ) , , , ( Y Q X N Z = , (X Z =
with the respect to correspondent elements of Petri net N.

Proposition 2.1. An arbitrary Petri net N may be considered as functional net, where the set X is formed with sources of net N, and the set Y is formed with drains of net N:

) , , , , ( ) ( F T Y Q X N Z = , , , . • • ∩ = T T Q Q T X \ • = Q T X \ • =
Therefore, in further statement, not limiting a generality, we shall consider functional Petri nets only allowing the empty sets of contact places. In [Zaitsev 97] the transmission functions of functional timed Petri nets were studied and methods of equivalent transformations based on algebraic transformations of transmission function were investigated.

Let us consider the following concepts according to standard definitions of graph theory [Berge 01,Harary 71]: , where

-a Petri net ) , , ( F T P N ′ ′ ′ = ′ is a subnet of N, iff )) ( ) (
• • ′ ∪ ′ = ′ T T P .
In other words, together with the transitions from T ′ , subnet ) (T B ′ contains all the incident places and is induced by these nodes. Further we shall consider mainly all the arcs connecting specified nodes in the source net; that is, we shall consider subnets generated by the set of nodes. Therefore, for brevity we shall omit flow relation implying the source relation F.

Definition 4. Functional subnet

A functional net is a functional subnet of net N and is denoted as , iff is a subnet of N induced by a set ) , , , ( Y Q X N Z ′ = N Z f N ′ T ′ : ) (T B N ′ = ′
and moreover Z is connected with the residuary part of the net only by arcs incident with contact places so that input places have only input arcs and output places have only output arcs:

∅ = ′ ∈ ∈ ∀ } \ | ) , {( : T T t t p X p , ∅ = ′ ∈ ∈ ∀ } \ | ) , {( : T T t p t Y p , ∅ = ′ ∈ ∧ ∅ = ′ ∈ ∈ ∀ } \ | ) , {( } \ | ) , {( : T T t p t T T t t p Q p .
These conditions may be represented also as:

∅ = ′ ∩ • ) \ ( T T X , , . ∅ = ′ ∩ • ) \ ( T T Y ∅ = ′ ∩ • • ) \ ( T T Q
Notice that in the same way we may introduce the concept of dual functional subnet induced by the specified set of places and using contact transitions. But furthermore we prefer to consider functional subnet according to Definition 4 for dual Petri net.

A subtraction of Petri net and its functional subnet

N Z′ is denoted the net Z N Z ′ - = ′ ′
, where

) \ , ), ( \ , ( ) \ ( T T X Q Y X P Y T T B Z ′ = ′ = ′ ′ U U . Proposition 2.2. (Symmetry). iff N Z f ′ N Z N f ′ - . To prove the proposition note that Z N ′ -
is connected with residuary part of net only by means of contact places and moreover constraints of arcs in definition of functional subnet correspond to constraints of arcs in definition of functional net.

Definition 5. Minimal functional subnet

Functional subnet is a minimal iff it does not contain any other functional subnet of Petri net N.

N Z f ′

Set of minimal functional subnets of Petri net (Fig. 2.1) is presented in Fig. 2.2. Notice that these functional subnets have only input and output places. For example, subnet has ,

1 N { } ) , , ( 5 3 2 2 t t t B Z = { } 3 2 , p p X = { } 5 4 , p p Y =
.

More complex examples of decomposition are considered in Section 7. In the same way we may introduce and study various subclasses of Petri nets with contact places. Contact places may be subdivided not only into input and output subsets. We propose to classify such nets in the following way. At first, we consider connections of a contact place with inside (I) of subnet and outside (O). At second, we distinguish three types of connections: only input arcs, only output arcs, input and output arcs. In such a way it may be introduced nine types of contact places presented in Fig. 2

(R B T R ⊆ R R R ⊆ ∪ • • • • ) ( ) (. Proof. A) Sufficiency. Let's ) (R B Z =
be a functional subnet. We prove that from the contrary. Let's and consider place such as . In all the cases: q , , we obtain the contradiction. In the same way we may prove

R R ⊆ • • ) ( p • ∈ R t R ∉ ∧ • ) t t ∈ ∃ • ( : Q q ∈ • ∈ R p t X ∈ (. Y q ∈ R R ⊆ • • ) B) Necessity. Let'
R R R ⊆ ∪ • • • ) ( ) ( Q • ∪ ∈ ∅ = ′ ∩ • ) \ ( T T Y • • ∪ ∈ X Q t ∪ Y R X • ⊂ ∪ R ∈ • • ) ′ ∩ • ) \ ( T T T R t ⊂ ∈ • • ) ( ′ ∩ • ) \ ( T T X Y • • ⊂ R T ⊂ (. ∅ = • Q ∅ =
Remark. If we would not consider functional subnets consisting of an isolated transition we might write the condition of Lemma 3.1 as:

R R R = ∪ • • • • ) ( ) (.
Theorem 3.1. Sets of transitions of two arbitrary minimal functional subnets Z′ and Z ′ ′ of Petri net N do not intersect.

Proof. Let and

) (T B Z ′ = ′ ) (T B Z ′ ′ = ′ ′
be minimal functional subnets. We assume the contrary, namely T and consider the net induced by the set

∅ ≠ ′ ′ ∩ ′ T T T ′ ′ ∩ ′
. Using the monotony of the dot operation we construct the following sequence:

T T T ′ ⊂ ′ ′ ∩ ′ then • • ′ ⊂ ′ ′ ∩ ′ T T T ) ( thus, according to Lemma 3.1 T T T T ′ ⊂ ′ ⊂ ′ ′ ∩ ′ • • • • ) ( ) ) ((
. In analogous way we may obtain

T T T T ′ ′ ⊂ ′ ⊂ ′ ′ ∩ ′ ) ) (( . Notice that also the following condition holds true T T T T ′ ′ ∩ ′ ⊂ ′ ′ ∩ ′ • • )) ( (. Therefore we have T T T T T T ′ ′ ∩ ′ ⊂ ′ ′ ∩ ′ ∪ ′ ′ ∩ ′ • • • • )) ( ( ) ) (( .

That is why

, is a functional subnet of Petri net , which contradict with minimality of subnets and

) ( T T B ′ ′ ∩ ′ Z ′ N ) (T B ′ = ) (T B Z ′ ′ = ′ ′ . Corollary 1.
{ j Z = N Z j f j T such as T , T , j j T U = ∅ = j k j T I k ≠ .
To represent the interconnection of minimal functional subnets we construct the high level net of minimal functional subnets. Transitions of this net correspond to minimal functional subnets. Set of places consists of contact places of decomposed net. High level net of Petri net is presented in Fig. 3.1. Let us implement the formal definition of these nets.

C P = ′ , T , } , | { N Z Z t t Z Z f ↔ = ′ F t p Z T t F t p Z ∈ ′ ∈ ∃ ⇔ ′ ∈ ′ ) , ( : ) ( ) , (, (. F p t Z T t F p t Z ∈ ′ ∈ ∃ ⇔ ′ ∈ ′ ) , ( : ) ( ) ,
Notice that the net of functional subnets may be defined for decomposition consisting of non-minimal functional subnets.

Definition 7. Completeness Subnet of Petri net N is the complete in N iff the following conditions: , • , • are held in N. ) , , , ( ) ( R Y Q X R B Z = = R X ⊆ • R Y ⊆ Q R ⊆ • Lemma 3.2. Subnet Z is the complete in Petri net N iff it is a functional subnet of N.
Proof. We start with proof of necessity of the completeness. So, let Z be a functional subnet of N:

. Then conditions of completeness are held for adjacent transitions of places Q according to definition of internal places, while for output transitions of input places and input transitions of output places according to constrains on arcs in definition of functional subnet.

N Z f

8

Let us prove the sufficiency. It is known that Z is subnet of N generated by the set of transitions R and Z is a functional net. It is remained to prove that constrains on arcs connecting places of subnet Z with residuary part of net are held. We denote residuary part of net as

) , , , ( ) ( R X Q Y R B N Z ′ ′ = - = ′ , where Q ) ( \ Y Q X P U U = ′ , R T R \ = ′
. We assume a contrary. Let N contains one or few no legal arcs of possible six types: a) • Therefore, in each of enumerated cases we obtain contradiction. This fact finishes the proof of sufficiency for subnet completeness. Lemma 3.3. Each contact place of the decomposed Petri net has no more than one input minimal functional subnet and no more than one output minimal functional subnet.

( ; b) ; c) ) ,r x ′ ) , ( y r′ ) , ( q r ′ 9 ; d) ( ; e) ; f) ) , r q′ ) , ( r q ′ ) , ( q r′ , where R r R r Q q Q q Y y X x ′ ∈ ′ ∈ ′ ∈ ′ ∈ ∈ ∈ , , , , ,. R X ⊄ • R ⊄ R Q ⊄ • R ⊄ • Z Z W e shall consider each of types mentioned separately: F r x ∈ ′) , F y r ∈ ′ ) , F q ∈ ′) , F r q ∈ ′ ) , F r q ∈ ′) , F q ∈ ′ ) , ∈ ′ r r • ∈ ′ q ∈ ′ q ∈ ′ ∈ ′ r r • ∈ ′ C p ∈ p ∈ ′ ′ ′, N Z ) p • ∈ ′ ′ , p t • ∈ ′ ′ t t ′ ′ ′, ( t′ ∃ Z t ∈ ′ ′ ∃ ′ ′ ′, ) , ( • ∈ ′ ′ ′ ′ ∈ ′ ′ ∃ p t Z t , ( E ℑ = , ′ ∈ t Z } k ( z N , j p Y ∈ | ) k p Z ∃ {( E = { w a) If (,
Proof. Suppose the contrary. We have to consider two cases: a) a contact place that has more than one input minimal functional subnet exists; b) a contact place that has more than one output minimal functional subnet exists.

C

In case a) there are minimal functional subnets such as , ( )

t Z ′ ′ ∧ ∈
. As according to Lemma 3.2 each minimal functional subnet is complete in so transitions according to the definition of completeness belongs to the same minimal functional subnet. Thus we obtain a contrary.

In case b) there are minimal functional subnets Z such as

) • ∧ ∈ ′ ′ ∃ p t
. And we obtain a contrary in such a manner as in the case a). The contrary obtained in the both cases proves the lemma.

The immediate conclusion of Lemma 3.3 and a marked graph definition [Diaz 01,Murata 89,Peterson 81] is the following theorem.

Theorem 3.2. The net of minimal functional subnets of a given Petri net is a marked graph.

Described above net is detailed enough representation of subnets' interconnections. It contains parallel paths in the case a few contact places connect a pair of subnets. For more brief representation we may hide contact places considering only interconnections of subnets. In this case we obtain a following graph.

Definition 8. Graph of functional subnet

Graph of functional subnets of a given Petri net N is a directed weighted graph G , where set of nodes ℑ is formed with minimal functional subnets of net N and arcs E connect nodes in the case corresponding subnets have common contact places in such a manner that: ,

) ,W : p , j X Z ∈ } F r q F ∈ ) , ( , (. q t T r T t q Z Z k j k j ∈ ∈ ∃ ∈ ∃ = ) , ( : , ) ,
Graph allows the scheme representation of functional subnets' interconnections for source net. At Fig. 3.2 a) graph of functional subnets of Petri net is presented.

1 N 2 2 2 Z 3 Z 1 Z a) directed 2 2 2 Z 3 Z 1 Z b) undirected Fig. 3.2. Graph of functional subnets of Petri net 1 G 1 N
Furthermore we will use also undirected graph of decompositions (Fig. 3.2 b) adding weights of arcs with contrary directions.

It should to be noted that minimality in general case does not mean a presence of a little quantity of places and transitions but only assumes that subnet may not be divided further in (internal) functional subnets. Moreover, non partitionable net may consist of an arbitrary number of nodes. An example of non partitionable net is presented at Fig. 3.3. Chain of places and transitions connected with arcs of pointed type may contain no limited number of nodes. Proof. Let us assume the contrary and exactly that exists functional subnet Z ′ of Petri net N that is not a union of minimal subnets. As ℑ defines partition of set T, so T ′ contains parts of subsets j T . Formally it may be represented as:

10 i R I i T ∈ = ′ U
, where I is a set of subnets' numbers transitions of which contains in T ′ , and, moreover, there exists at least one set

i i T R ⊆ j j T R ⊂
for any I j ∈ . Let us consider set of transitions and show that it generates functional subnet of Petri net N. As

j j R T S \ = ) (S B Z ′ is functional subnet of N,
T P P P = 1 Z Z
is also functional subnet of N. We have for transitions: In the same way it may be constructed equations defining the set the places belong to:

     ∈ ∨ ∈ ∈ ∀ ∧ ∈ ∨ ∈ ∈ ∀ ≡ ∈ ∈ ∨ ∈ ∈ ∀ ∧ ∈ ∨ ∈ ∈ ∀ ≡ ∈ • • • • )) ( ) )(( ( )) ( ) )(( ( ) ( )) ( ) )(( ( )) ( ) )(( ( ) ( 2 1 3 1 1 3 0 2
       ∈ ∈ ∀ ∧ ∈ ∈ ∀ ≡ ∈ ∈ ∈ ∀ ∧ ∈ ∈ ∀ ≡ ∈ ∈ ∈ ∀ ∧ ∈ ∈ ∀ ≡ ∈ ∈ ∈ ∀ ∧ ∈ ∈ ∀ ≡ ∈ • • • • • • • • ) )( ( ) )( ( ) ( ) )( ( ) )( ( ) ( ) )( ( ) )( ( ) ( ) )( ( ) )( ( ) ( 1 0 3 0 1 2 1 1 1 0 0 0 T t p
T T = 1 0 U ∅ = 1 0 T T I 1
T . We obtain the following system:

))) )( ( ) )( (( )) )( ( ) )( )((( ( ))) )( ( ) )( (( )) )( ( ) )( )((( ( ) ( 0 1 1 1 1 0 1 1 1 T t p s T s p s T s p s T s p s t p T t p s T s p s T s p s T s p s t p T t ∈ ∈ ∀ ∧ ∈ ∈ ∀ ∨ ∈ ∈ ∀ ∧ ∈ ∈ ∀ ∈ ∀ ∧ ∈ ∈ ∀ ∧ ∈ ∈ ∀ ∨ ∈ ∈ ∀ ∧ ∈ ∈ ∀ ∈ ∀ ≡ ∈ • • • • • • • • • • (4.3)
Using the finiteness of places' and transitions' sets, we replace the quantifiers of generality with conjunction on corresponding subsets of elements. Besides, we introduce indicators t τ of the belonging of transition to subsets in such a way that . Note that

j t T t j ∈ ⇔ = τ } 1 , 0 { ∈ t τ
; so, these values may by used in logical equations. And, as T , so

, and also . Therefore, equations (4.3) may be represented in Boolean algebra in the following form:

∅ = 1 T 0 I ) 1 T (t t ∈ ⇔ τ ) ( 0 _ T t t ∈ ⇔ τ ) ( ) ( ) ( ) ( _ _ s p s s p s s p s s p s t p s p s s p s s p s s p s t p t τ τ τ τ τ τ τ τ τ • • • • • • • • • • ∈ ∈ ∈ ∈ ∈ ∈ ∈ ∈ ∈ ∈ ∧ ∨ ∧ ∧ ∧ ∨ ∧ ≡ (4.4)
Thus, we have proved the following theorem. Theorem 4.1. A partition of an arbitrary Petri net into functional subnets is completely defined with a system of logical equations (4.4).

In the process of solution system (4.4) may be replaced with one equation that is the conjunction of equations corresponding to each transition of net. Methods of logical equations solution are well studied, for example, in [Glushkov 62]. Let us consider an example of net (Fig. 2.1) decomposition. We construct the system of logical equations of form (4.4):

1 N            ∨ ∨ ≡ ∨ ∨ ≡ ∨ ∨ ≡ ∨ ∨ ≡ ∨ ∨ ∨ ≡ ∨ ∨ ∨ ≡ ) )( ( ) )( ( ) )( ( ) )( ( ) )( )( ( ) )( )( ( 6 4 1 6 4 1 6 2 5 6 2 5 6 6 2 5 6 2 5 2 5 1 2 5 1 5 6 4 1 6 4 1 4 3 4 3 4 4 3 4 3 3 2 1 3 2 1 3 6 2 5 6 2 5 3 2 1 3 2 1 2 5 1 2 5 1 2 3 2 1 3 2 1 2 5 1 2 5 1 1 4 6 1 4 6 1 τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ
Let us construct the conjunction of equations, simplify it and bring to the disjunction perfect normal form. We obtain:

6 5 4 3 2 1 6 5 4 3 2 1 6 5 4 3 2 1 6 5 4 3 2 1 6 5 4 3 2 1 6 5 4 3 2 1 6 5 4 3 2 1 6 5 4 3 2 1 τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ τ ∨ ∨ ∨ ∨ ∨ ∨ ∨ v
Note that first of terms corresponds to empty subnet, next three terms correspond to minimal subnets represented in Fig. 2.2: T , , . Residuary terms describe the sums of minimal subnets. So, for instance, sixth term describes subnet represented in Fig. 2.6.

} { 1 1 t = } , , { 5 3 2 2 t t t T = } , { 6 4 3 t t T =
It should to note that algorithmic complexity of an arbitrary Petri net decomposition in functional subnets with logical equations described is in general case asymptotically exponential that concerned with estimations of logical equations' solution complexity [Glushkov 62]. But this technique is universal and may be applied also for decomposition of Petri net into other kinds of subnets with contact places mentioned in Section 2 (Fig. 2.3).

Decomposition with an ad-hoc algorithm

Let us consider the following algorithm.

Algorithm 4.1:

Step 0. Choose an arbitrary transition T t ∈ of net N and include it into the set of chosen transitions . } { : t R =

Step 1. Construct subnet Z that is induced by set R:

) , , , ( ) ( R Y Q X R B Z = = . Step 2. If Z is the complete in N, then Z is subnet sought, stop.
Step 3. Create the set of absorbing transitions:

} | { R t Q t R t Y t R t X t t S ∉ ∧ ∈ ∨ ∉ ∧ ∈ ∨ ∉ ∧ ∈ = • • • • . Step 4.
∈ X v Y • ∈ • • ∈ S X x ∈ • ∈ x v Z ′ .
Contradiction has been obtained. In the same way we come to contrary in second and third cases.

∉ • v ∈ v Y v X • ∈ x Z ′ 1 := Z i Z : + = i i ), ,W Z ,..., ( = F T , , → F : Ν m n T = + A , 1 = n j , 1 = ∈ ) j m , 1 = ∈ ) i . - 0 Ν M b) Let t
. We consider the first transition v of the set T ′ ′ T ′ ′ , which was included into set S on any pass of Algorithm's 1 main loop. Thus, according to description of Step 3, is possible one of three cases: or , or . In the first case a place , such as

X • ∈ • • ∈ S x ∈ v
may not be neither input, nor output, nor internal place of net . Contradiction has been obtained. In the same way we come to contrary in second and third cases.

Thus, Algorithm 4.1 allows the construction of minimal functional subnet Z of Petri net N. Let us assign i и . Than we assign

= : Z N N - = :
and repeat execution of Algorithm 1 in the case the set T is not empty. Continuing in such a manner and assigning we shall have constructed the set of minimal functional subnets of net N which represent the sought partition of source net.

1 k Z Z , 2 1
Implementation of algorithm over net represented in Fig. 2.1 gives us the result coinciding with one obtained in the previous section on the base of logical equations and represented in Fig. 2.2.

Since each arc is processed by algorithm only once, the following theorem is valid. Theorem 4.3. The complexity of Algorithm 4.1 is linear with respect to size of the net. Described algorithm of decomposition has been implemented in command line tool Deborah (www.geocities.com/zsoftua/softe.htm), which was developed as plug-in for Tina system [Berthomieu 04] (www.laas.fr/tina).

Compositional Analyses of Petri Nets

Further we consider Petri nets with multiply arcs [Murata 89] , , F T P N where are as in Definition 1 and

P Ν W
defines the multiplicity of arcs, is a set of natural numbers.

Let us P = , and the sets of places and transitions are enumerated. We introduce matrices , of input and output arcs of transitions correspondingly:

-

A j i a A , - -= , m i , ;    = - , , 0 , , ( ), , ( , otherwise F t p t p w a i j i j i j i a A , + + = , i , n j , 1 = ;    = + . , 0 , , ( ), , ( , otherwise F p t p t w a j i j j i

And finally we introduce incidence matrix A of Petri net as

+ - = A A A Marking of net is a mapping 0 : Ν → P µ , defining a distribution of dynamic elements named tokens over places; is a set of nonnegative integer numbers. Marked Petri net is a couple ) , ( 0 µ N = or a quintuple ) , , 0 , , ( µ W F T P M =
, where 0 µ is initial marking. Further we present markings as vectors.

Linear Invariants' Calculation

P-invariant of Petri net is an integer nonnegative solution x (vector-row) of the system

0 = ⋅ A x . (5.1)
T-invariant of Petri net is an integer nonnegative solution y (vector-column) of the system 0 = ⋅ y A . Petri net is p-or t-invariant, if it has a corresponding invariant with all positive components.

So, according to [Murata 89], each t-invariant of Petri net is p-invariant of dual net, we shall consider further p-invariants only. Notice that dual net has transposed incidence matrix. In other words places of dual net correspond to transitions of source net and vice versa. Examples of Petri net and dual net are presented in Fig. 5.1, 5.2. Let us consider the structure of the system of equations (5.1). Every equation i L :

0 = ⋅ i A x
, where i A denotes i-th column of matrix A , corresponds to the transition i t . It contains terms for all the incident places. Coefficients are the weights of arcs. The terms for input places have the sign minus and the terms for output places have the sign plus. So, the system (5.1) may be represented as

n L L L L ∧ ∧ ∧ = ... 2 1 .
(5.2)

Theorem 5.1. An arbitrary invariant x′ of Petri net N is the invariant of every functional subnet Z ′ , . N Z f ′ Proof. So x′ is the invariant of Petri net , then N x′ is a nonnegative integer solution of (5.2) and consequently x′ is nonnegative integer solution of each . Therefore, i L x′ is the solution of an arbitrary subset of the set { . } i L A functional subnet Z ′ , is generated by the set of its transition N Z f ′ T ′ .
Thus the equation corresponding to transition has the same form as for entire net since subnet contains all incident places of source net. Therefore, the system for invariant of a functional subnet

i L Z ′ , is subset of the set { and vector N Z f ′ } i L x′ is its solution. Consequently, x′ is the invariant of functional subnet Z ′ . Arbitrary choice of N Z f ′
in the above reasoning proves the theorem.

Corollary. If a Petri net is invariant, then all its functional subnets are invariant too.

Theorem 5.2. Petri net is invariant iff all its minimal functional subnets N j Z , are invariant and there is a common nonzero invariant of contact places.

N Z j f

Proof. We shall use only equivalent transformations to not prove separately necessary and sufficient conditions. According to Theorem 3.1, the set of minimal functional subnets , of an arbitrary Petri net N defines the partition of the set T into nonintersecting subsets

} { j Z = ℑ N Z j f j T .
Let us the number of minimal functional subnets is k . As it was mentioned in the proof of Theorem 5.1, equations contain terms for all incident places. So we have

k L L L L ∧ ∧ ∧ ⇔ ... 2 1
, where is the subsystem for minimal functional subnet

j L j Z , .
Notice that if has no solution, then has no solution too (except trivial, of course).

N Z j f j L L Let us j
R is the matrix of basis solutions of subsystem . Then we write the general solution of the subsystem in the form

j L j L j j G z x ⋅ = , (5.3) where j
z is an arbitrary nonnegative integer vector. Thus

k k G z G z G z x L ⋅ = = ⋅ = ⋅ = ⇔ ... 2 2 1 1 . So the system k k G z G z G z x ⋅ = = ⋅ = ⋅ = ... 2 2 1 1
(5.4) is equivalent to the source system (5.1). Further we shall demonstrate, that solution of above system (5.4) involves enough little number of equations. Let us consider a set of places of Petri net with the set of minimal functional subnets { :

N } | N Z Z j j f C Q Q Q P k U U U U ... 2 1 = , where
is the set of internal places of subnet • Now we shall construct equation for the contact place C p ∈ so it is incident more than one subnet. According to Lemma 3.3, each contact place C p ∈ is incident not more than two functional subnets. So we have equations

j p j i p i G z G z ⋅ = ⋅ , (5.5)
where j i, is a numbers of minimal functional subnets incident to contact place , is a column of matrix corresponding to the place

C p ∈ j p R j R
p . Equation (5.5) may be transformed to the form 0

= ⋅ - ⋅ j p j i p i G z G z . So the system      ∈ = ⋅ - ⋅ ∈ ∨ ∈ ⋅ = C p G z G z C p Q p G z x j p j i p i j j p j p , 0 , (5.6)
is equivalent to the source system (5.1). This fact proves the theorem. Conclusion 1. To calculate Petri net invariants we may to calculate invariants of its minimal functional subnets and then to find common invariants of contact places.

Notice that in both mentioned cases according to (5.6) we have to solve a linear homogeneous system of equation in nonnegative integer numbers.

Conclusion 2. The above theorem 5.2 is valid for an arbitrary set of functional subnets that defines a partition of the set of the transitions of source Petri net.

Therefore, a compositional method for Petri net invariants calculation may be presented as:

• Stage 1. Decompose Petri net into functional subnets.

• Stage 2. Calculate invariants for each of functional subnets -find general solutions (5.3). • Stage 3. Compose subnets -find the common solution for the set of contact places (5.5). Note that stages 2, 3 consist in solution of systems of linear homogeneous Diophantine equations in nonnegative integer numbers. It ought to find common solution of a system in the form of linear combination of basis solutions. For these purposes may be applied methods described in [Colom 90,Contejean 97,Toudic 82].

Let us extract out of system (5.6) equations for contact places 0

= ⋅ - ⋅ l i l j i j G z G z . Or in the matrix form 0 = - ⋅ l i j i l j G G z z .
Let us enumerate all the variables j z in such a way to obtain united vector

k z z z z ... 2 1
= and assemble matrices , in united matrix

j i G l i G - K . Then we obtain system 0 = ⋅ K z
. System obtained has the form (5.1), consequently, its general solution has the form (5.3):

R v z ⋅ = .
(5.7) Let us construct united matrix G of solutions (5.3) of systems for all functional subnets in such a manner that

j L G z x ⋅ = .
(5.8) We substitute (5.7) in (5.8):

G R v x ⋅ ⋅ = . Thus H v x ⋅ = , G R H ⋅ = .
(5.9) Since only equivalent transformations were involved, the reasoning represented above proves the following theorem.

Theorem 5.3. Expressions (5.9) represent the general solution for invariant (5.1).

Now we estimate the total speed-up of computations under obtaining of invariants with decomposition. Let r be a maximal number either contact places or places of subnets

( )    = j j P C r max , max    . Note that n r ≤ .
Then complexity of invariants calculation with decomposition may be estimated as r 2 ~, so the complexity of decomposition according theorem 4.6 is linear.

Thus, speed-up of computations is estimated as

r n r n - = 2 2 2 .
(5.10) Therefore, obtained speed-up of computations is exponential with respect to dimension of net.

Now we apply introduced technique to the calculation of invariants of Petri net (Fig. 5.1). Notice that, this net is a weighted variant of the net (Fig. 2.1).

2 N 1 N I. As it was represented in Fig. 2.2, Petri net is decomposed into three minimal functional subnets completely defined by the sets of its transitions T , , .

1

N 3 2 1 , , Z Z Z } , , 5 3 t t } , { 6 4 1 t t = } { 1 2 t T = { 2 3 t T = II.
Let us calculate invariants of the minimal functional subnets.

Subnet 1 Z .
The system of equations is

   = + ⋅ - = + ⋅ - . 0 2 , 0 6 1 4 1 5 x x x x
The general solution is

(

).

1 3 0 0 6 1 1 ⋅ = z x Subnet 2 Z .
The system of equations is

{ . 0 3 3 2 1 = + ⋅ + - x x x
The general solution is

        ⋅ = 0 0 1 0 1 0 0 0 1 3 ) , ( 2 2 2 1 z z x .
Subnet 3 Z . The system of equations is

     = + - = + - = ⋅ + - ⋅ - . 0 , 0 , 0 6 3 5 2 4 3 5 3 2 x x x x x x x
The general solution is ( )

1 3 3 1 0 3 1 ⋅ = z x . III.
Let us write the system of equations for the contact places. Notice that in net all places are contact ones

1 N          ⋅ = ⋅ = ⋅ = ⋅ = ⋅ = ⋅ = ⋅ = ⋅ = ⋅ = ⋅ + ⋅ = . 1 1 , 3 3 , 3 1 , 1 1 , 6 1 3 1 1 2 1 5 1 1 3 1 4 3 1 2 2 3 3 1 2 1 2 1 1 2 2 2 1 1 z z x z z x z z x z z x z z z x
We may write this system in the form (5.1) and solve it with Toudic method [Toudic 82]

         = ⋅ - ⋅ = ⋅ - ⋅ = ⋅ - ⋅ = ⋅ - ⋅ = ⋅ - ⋅ + ⋅ . 0 1 1 , 0 3 3 , 0 3 1 , 0 1 1 , 0 6 1 3 1 1 3 1 1 1 3 1 3 1 2 2 3 1 2 1 1 1 2 2 2 1 z z z z z z z z z z z
The general solution with the respect to the vector ) , , , (

3 1 2 2 2 1 1 1 z z z z z = is ( ) 1 3 1 1 ⋅ = r z
. And the general solution of source system is ( )

1 3 3 1 6 ⋅ = r x
. Notice that in this example we have not obtained any speed-up of computations, so Petri net is tiny and all its places are contact ones. Real-life examples are considered in Section 7.

Fundamental Equation Solution

A fundamental equation of Petri net [Murata 89] may be represented as follows

µ ∆ = ⋅ A x , (5.11) where 0 µ µ µ - = ∆
, x is a firing count vector, A is a transposed incidence matrix or incidence matrix of dual Petri net [Murata 89]. Notice that each equation of this system corresponds to a transition of dual Petri net.

According to [Schrejver 91,Kryviy 99] we represent a general solution of homogeneous system as the linear combination of basis solutions with nonnegative integer coefficients. Notice that a basis consists of minimal in integer nonnegative lattice solutions of system. As distinct from classic theory of linear systems for representation of general nonnegative integer solution of nonhomogeneous system it is necessary to involve not one arbitrary but a set of minimal particular solutions.

Let us consider the structure of system (5.11):

µ ∆ = ⋅ A x
. We apply the technique described in the previous subsection 5.1 to nonhomogeneous systems. Each equation :

i L i i A x µ ∆ = ⋅
, where denotes i-th column of matrix i A A , corresponds to transition (of dual net). Equation contains the terms for all the incident places. At that the coefficients are equals to weights of arcs and the terms for input places have sign minus and for output places -plus. i t Therefore the system (5.11) may be represented as

n L L L L ∧ ∧ ∧ = ... 2 1
(5.12) Proof. We shall use equivalent transformations of systems of equations to not prove separately necessary and sufficient conditions. According to Theorem 4.4, a set of minimal functional subnets , of an arbitrary Petri net defines a partition of set }

{ j Z = ℑ N Z j f N T into nonintersecting subsets j
T . Let number of minimal functional subnets equals . As it was mentioned in the proof of Theorem 5.3, equations contain the terms for all the incident places. Therefore,

k k L L L L ∧ ∧ ∧ ⇔ ... 2 1 , (5.13)
where is a subsystem for a minimal functional subnet j L j Z , . Notice that if has not solutions, than has not solutions also.

N Z j f j L L
Let us a general solution for each functional subnet has the form

j j j j G z x x ⋅ + ′ = , (5.14) where j j G z ⋅
is the general solution of homogeneous system,

j j X x ′ ∈ ′
, where j X ′ is the set of minimal particular solutions of nonhomogeneous system of equations. According to (5.13):

k k k G z x G z x G z x x L ⋅ + ′ = = ⋅ + ′ = ⋅ + ′ = ⇔ ... 2 2 2 1 1 1 . Therefore system k k k G z x G z x G z x x ⋅ + ′ = = ⋅ + ′ = ⋅ + ′ = ... 2 2 2 1 1 1
(5.15) is equivalent to source system of equations (5.11). We shall demonstrate further that the solution of system (5.15) requires essentially smaller quantity of equations. Let us consider a set of places of Petri net with the set of minimal functional subnets { :

N } | N Z Z j j f C Q Q Q P k U U U U ... 2 1 =
, where Q is a set of internal places of subnet Now we construct equations for contact places of net C p ∈ , so only they are incident more than one subnet. According to Lemma 3.3, each contact place is incident not more than two functional subnets. Therefore, we have equations

C p ∈ l p l l p j p j j p G z x G z x ⋅ + ′ = ⋅ + ′ , (5.16)
where is the numbers of minimal functional subnets incident to contact place and is a column of matrix corresponding to place

l j, C p ∈ j p G j G
p . Equation (5.16) may be represented in form

j p l p l p l j p j x x G z G z ′ - ′ = ⋅ - ⋅ . Thus, system      ∈ ′ - ′ = ⋅ - ⋅ ∈ ∨ ∈ ⋅ + ′ = C p x x G z G z C p Q p G z x x j p l p l p l j p j j j p j j p p , , , (5.17)
is equivalent to source system (5.11). This fact completes the proof of theorem. Notice that in both cases described in proof according to (5.17), we have to solve a linear homogeneous system of equations.

Corollary 1. To solve the fundamental equation of Petri net we may solve the fundamental equations of its minimal functional subnets and then to find a common solutions for contact places.

Corollary 2. Theorem 5.5 is valid also for an arbitrary set of functional subnets defining a partition of the set of transition of Petri net. Therefore, a compositional method for solution of fundamental equation of Petri net may be presented as:

• Stage 0. Construct a dual Petri net.

• Stage 1. Decompose dual Petri net into functional subnets.

• Stage 2. Calculate solutions for each of functional subnets -find general solutions of nonhomogeneous systems of equations (5.14). • Stage 3. Compose subnets -find the common solution (5.16) for the set of contact places. Note that stages 2, 3 consist in solution of systems of linear nonhomogeneous Diophantine equations in nonnegative integer numbers. For this purpose the methods described in [Colom 90,Contejean 97,Kryviy 99,Toudic 82] may be applied.

Let us extract out of system (5.17) equations for contact places

j l l i l j i j x x G z G z ′ - ′ = ⋅ - ⋅ . Or in the matrix form i l i j i l j b G G z z ′ = - ⋅ , j l i x x b ′ - ′ = ′
Let us enumerate all the variables j z in such a way to obtain a united vector k z z z z ... (5.18) Let us construct a united matrix G of solutions (5.14) of system (5.11) for all the functional subnets in such a manner that

G z x x ⋅ + ′ = .
(5.19) We substitute (5.18) in (5.19):

( ) G R v G z x G R v z x x ⋅ ⋅ + ⋅ ′ + ′ = ⋅ ⋅ + ′ + ′ = . Thus H v x x ⋅ + ′ ′ = , G z x x ⋅ ′ + ′ = ′ ′ , G R H ⋅ = .
(5.20) Since only equivalent transformations were involved, the reasoning represented above proves the following theorem.

Theorem 5.6. Expressions (5.20) represent a general solution of fundamental equation (5.11). Now we estimate the total speed-up of calculations under the obtaining of invariants via decomposition. Let r be a maximal number either contact places or places of subnets

( )    = j j P C r max , max    . Notice that n r ≤ .
Then the complexity of fundamental equation solution for subnet may be estimated as r 2 ~, since the complexity of decomposition according to Theorem 4.3 is polynomial.

Thus, the speed-up of computations is estimated as

r n r n - = 2 2 2 .
(5.21)

Therefore, speed-up of computations obtained is exponential.

Notice that the exponential speed-up of computations represented with expression (5.21) is valid also in the case the general solutions for the functional subnets have more than one minimal particular solution. Really, let each of minimal functional subnets has not more than minimal solutions. Then during calculation of common solutions for contact places we ought to solve systems and polynomial multiplier may be omitted in the comparison estimations of exponential functions.

N ) 4 , 1 , 1 , 2 , 1 ( - - = ∆µ .
Stages 0,1. Dual Petri net 2 Ñ} { 4 t (Fig. 5.2) is decomposed into four minimal functional subnets completely defined by the subsets of its transitions: T , , T , T .

4 3 2 1 , , , Z Z Z Z } , 3 t } { 5 3 t = } { 1 1 t = { 2 2 t T = 4 = Stage 2. 1 Z : { ; 1 6 4 1 - = + + - x x x         ⋅ + = 1 0 0 0 0 1 0 0 1 0 0 1 ) , ( ) 0 0 0 0 0 1 ( 1 2 1 1 u u x . 2 Z :    = - - = - - ; 1 , 2 3 3 3 2 1 5 2 1 x x x x x x         ⋅ + = 0 0 0 0 1 1 0 3 0 1 0 1 ) , ( ) 0 1 0 0 0 1 ( 2 2 2 1 u u x . 3 Z : { ; 4 6 6 6 5 2 = - + x x x         ⋅ + = 1 0 0 0 1 0 1 6 0 0 0 0 ) , ( ) 0 4 0 0 0 0 ( 3 2 3 1 u u x . 4 Z : { ; 1 2 4 3 - = -x x ( ) 0 0 1 2 0 0 ) ( ) 0 0 1 1 0 0 ( 4 1 ⋅ + = u x . Stage 3.            = - - = - = - = - = - = - - + ; 0 , 3 6 3 , 1 , 1 2 , 0 , 0 3 2 3 1 1 2 3 1 2 1 4 1 1 1 4 1 2 1 3 2 2 2 2 2 2 1 1 2 1 1 u u u u u u u u u u u u u u u . 0 1 0 1 0 1 0 1 0 1 0 2 1 1 ) , ( ) 0 0 0 0 1 0 1 ( ) ( 2 1 4 1 3 2 3 1 2 2 2 1 1 2 1 1         ⋅ + = = = v v u u u u u u u u         ⋅ + = 1 6 1 2 0 2 1 0 0 0 1 1 ) , ( ) 0 4 1 1 0 2 ( 2 1 v v x .
Notice that the general solution of homogeneous equation constitutes t-invariant of Petri net. On the minimal solution

) 0 , 4 , 1 , 1 , 0 , 2 ( = ′ x
we may construct the friable sequence

5 1 4 3 5 5 5 1 t t t t t t t t = σ . Therefore, marking ) 4 , 0 , 1 , 2 , 0 ( = µ is reachable in net .
1 N In this tiny example all the places are contact, so we have not obtained any speed-up of computations. For real-life examples the accelerations may become rather considerable [Zaitsev 04c,04f,05].

Analysis of Petri Net Properties

We consider the role that linear invariants and fundamental equation solutions play for the analysis of Petri net properties. Then we show that a lot of tasks for Petri net properties analyses may be reduced to solution of linear Diophantine systems of equations and inequalities and solvable in the same compositional way.

Invariants take a key part at investigation of such properties of nets as boundness, conservativeness, liveness [Diaz 01,Girault 03,Murata 89]. Net is invariant if it possesses an invariant with all the natural components. It is known that p-invariant net is conservative and bounded and these properties are structural i.e. they hold true at any initial marking. Tinvariant represents persistent sequences of transitions firing. Existence of such sequences is a necessary condition for liveness of bounded net. As according to [Murata 89] each t-invariant of Petri net is p-invariant of dual net, so further without loss of generality we shall consider only p-invariants.

It is known [Diaz 01,Girault 03,Murata 89,Sleptsov 86] that the solvability of fundamental equation in nonnegative integer numbers is a necessary condition of the reachability of a given marking. Solutions of system (5.11) are used for the construction of the required firing sequences.

Notice that a majority of known tasks of Petri nets analysis is reduced to solving a linear system of equations and inequalities [Murata 89,Sleptsov 86]. Necessary and sufficient conditions for basic structural properties of Petri nets are represented in Table 5.1.

0 , 0 ≤ ⋅ > ∃ A x x Conservativeness 0 , 0 = ⋅ > ∃ A x x Repetitiveness 0 , 0 ≥ ⋅ > ∃ y A y Persistance 0 , 0 = ⋅ > ∃ y A y
During the investigation of free choice Petri nets properties [Desel 1995, Murata 89]

S N S • ⊆ • • ⊆ S S Q N } S • 1 , 0 0 ≤ ⋅ D s and 0 ≤ ′ ⋅ D q
, where and are modified incidence matrices [Murata 89].

D D′

As shown in [Kryviy 99] a linear system of equations and inequalities may be reduced to equivalent system of equations. Note that transformations mentioned correspond to modification of source net in such a manner that the task of any property determination may be considered as calculation of p-invariant for modified net. Therefore, without loss of generality we solve homogeneous equation of the form (5.1) for determination of structural properties and nonhomogeneous equation of the form (5.11) for determination of behavioural properties of Petri nets.

Notice that, for a given matrix C of a linear system we may construct a matrix of directions and consider it as the incidence matrix of a Petri net. This allows the solution of an arbitrary linear systems using described decomposition [Zaitsev 04h].

()

C sign D =
6 Sequential Compositions of Functional Subnets

Collapse of Weighted Graph

Sequential composition of Petri net out of its minimal functional subnets is aimed to provide an additional speed-up for calculation of invariants and solution of the fundamental equation. The main idea is concerned with the system of equations for contact places. If this system has dimension exceeding the maximal dimension of functional subnet then we propose to execute sequential composition of subnets solving a sequence of systems with lesser dimension. Since the complexity of system solution is exponential, we obtain an essential speed-up in that way.

We consider the presentation of decomposition with undirected graph G as it was described in Section 3 (Fig. 3 Simultaneous composition assumes instant resolution of system for all contact places. It was considered in previous Section 5; speed-up of computations is estimated by (5.10). In general case the sequential composition requires the solution of system for a few neighbor functional subnets represented by connected subgraph of , which is replaced then by a single vertex (Fig. 6.1). Continuing in such a way we transform the source graph into a single vertex. This process was called a collapse of graph. The simplest kind of sequential composition is a pairwise composition at which a pair of adjacent vertices is replaced by one new vertex as the result of the solution of system constructed for contact places used for connection of corresponding subnets (Fig. 6.2). The number of contact places is equal to multiplicity of corresponding edge. In essence this operation may be represented as a fusion of adjacent vertices of a graph. Pairwise composition (contracting) provides the smallest dimension of solving systems. Process of pinvariants calculation via edge composition is described in the next subsection 6.2.

A linear system containing equations and unknown variables is named by system. We assume that linear homogeneous system of form (5.1) is solving. In framework of Petri net place invariants, equations of system (5.1) correspond to transitions and unknownsto places of Petri net. Such an assumption does not restrict the generality as it was shown [Zaitsev 04d] in the same way the decomposition might be applied for nonhomogeneous systems at state equation solution. As a general estimation of complexity one parameter equaling to the maximum among a number of equations and a number of unknowns is considered usually:

l n ) , n m ) , ( m n max(m =
. Note that known methods of linear diophantine systems' solution in nonnegative integer numbers [Colom 90,Contejean 97,Kryviy 99,Martinez 82,Schrejver 91,Toudic 82] are exponential in time and in space. Thus, time complexity of system solution is about .

k ( k ) , ( 1 1 m n ) , 2 2 m n ) , ( k k m n i
Z it have been obtained a matrix of basis solutions containing b solutions. Then we have to solve one extra system for contact places at simultaneous composition. Estimation of dimension of this system is , as equations of system corresponds to contact places and free variables of basis solutions for subnets are unknowns. Notice that , , where с is the number of contact places in the obtained decomposition: ,2,3,4,5,6,7,8 Z1,2,3,4,5,6,7,8 Z1,2,4,5,6,7,8 Z3 11 Z1,2,3,4,5,6,7,8 Let we execute the fusion of two adjacent vertices with numbers i and representing the systems of equations with complexities and correspondingly. Then the complexity of the system solving at pairwise composition equals to ( , where is the number of contact places in composition of subnets

i G i ) , ( ∑ i i b с n n i i = ∑ с m i i + ∑ m = С с = .
Z2Z5 d=8 Z1Z2 d=9 Z1Z4 d=9 Z1Z7 d=9 Z1Z8 d=11 Z1Z6 d=11 Z1Z3 d=11 Z1Z5 d=2 Z4Z7 d=6 Z2Z6 d=6 Z2Z4 d=6 Z2Z3 d=9 Z1Z2 d=30 Z1Z8 d=30 Z5Z6 d=2 Z1Z3 d=2 Z1Z4 d=2 Z1Z8 d=4 Z5Z7 d=4 Z1Z2 d=7 Z1Z4 d=44 Z4 Z5 Z8 Z1 Z2 Z3 Z6
j i b + ) , ( i i m n ) , ( j j m n i ) , , j j i b с j i с . Z и j
Z . Further it is convenient to consider one of the parameters describing the dimension of a system, for instance, the number of equations. Let us assume that the number of unknowns differs slightly. Moreover, the number of basis nonnegative solutions is unknown beforehand that makes a priory estimation difficult. It is known that basis of solutions under set of vectors with natural components and natural generators, as a rule is characteristic by a large scale. Whereas basis constructed for rational generators has essentially low dimension [Colom 90].

It is convenient to choose as a characteristic of system's dimension a number of places. So we consider as a characteristic of dimension for a system of equations for a functional subnet the number of its places and as a characteristic of composition's dimension -the number of contact places used in composition. Contact places in such a calculation are accounted twice for each of adjacent subnets

i i i C Q m + = i
, where Q is a set of internal places and C is a set of contact places of subnet i i Z . From practical experiences we have observed that generally . Thus, we assume in the sequel that this inequality holds.

i i m n ≤ We consider diophantine linear systems of equations solving in the set of nonnegative integer numbers. As it was early mentioned, the complexity of such systems' solution is exponential. In comparison estimations of exponential functions the polynomial multiplier may be omitted. Thus, the complexity of system solution by usual methods we shall consider equals to , and complexity of solution via simultaneous composition -equals to 2, w h e r e . In other words, dimension of system is defined by maximal dimension among subsystems constructed for functional subnets and system constructed for contact places. Really, we have . Thus, speed-up of calculations at simultaneous composition equals to . At the condition we have

m 2 , m i r ) ( max с r i = ) 2 ( 2 2 r r r O k = + ⋅ r m- 2 1 > k m r <
and, consequently . Simultaneous composition advisable to apply in the cases the total number of contact places does not exceed the number of places of maximal subnet or in the cases of minor exceeding.

1 2 > -r m с m i i ≥ ) ( max
As the solution of system for each subnet is the necessary stage of compositional technique, so further constructions are aimed to decrease the complexity of solution of system for contact places. We consider sequential collapse of graph by the way of fusion (collapse) of subgraphs generated by a given subset of vertices. Not limiting the generality we consider connected subgraphs. As the width of collapse we consider the sum of weights of edges of subgraph at a step. For sequential collapse the width is equal to maximal width of all the steps. The task consists in construction such a sequence of fusions, which provides the minimal width of collapse. The width of collapse corresponds to the dimension of system and the complexity of the system solution via sequential composition is about 2 , where d is the width of collapse. Since is essentially lesser than d d r , we obtain an additional speed-up. Further we shall consider an edge collapse as more effective way of composition under exponential complexity of systems' solution. Note that, estimations obtained are asymptotic. In particular case at not great dimension of subnets when the concrete values of estimations of exponential complexity are comparable to polynomial multipliers the collapse of subgraphs often presents a lesser calculation complexity.

Case Study of Edge Collapse

Let's consider Petri net model of modified protocol ECMA presented in Fig. 6.1.

              = 1 0 0 1 0 0 1 0 0 0 0 1 1 1 0 1 1 0 1 0 0 3 , 1 2 , 1 1 , 1 12 11 10 9 3 2 1 1 z z z p p p p p p p G , G ,               = 0 1 1 0 0 1 0 0 0 1 1 1 1 0 0 1 0 0 3 , 2 2 , 2 1 , 2 12 11 10 9 7 6 5 2 z z z p p p p p p p               = 0 1 0 1 0 1 0 0 0 0 0 1 1 1 1 0 1 0 0 0 1 3 , 3 2 , 3 1 , 3 16 15 14 13 8 7 5 3 z z z p p p p p p p G , .               = 0 0 0 1 1 1 1 0 1 0 1 0 0 1 0 0 0 1 3 , 4 2 ,
     = 1 0 0 0 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 1 1 0 0 0 1 0 0 0 1 1 0 0 0 0 1 0 0 0 0 1 0 0 1 0 0 0 0 0 1 1 1 0 1 0 1 0 0 1 0 1 0 0 0 1 0 1 0 1 1 0 1 3 , 4 2 , 4 1 , 4 3 , 3 2 , 3 1 , 3 3 , 2 2 , 2 1 , 2 3 , 1 2 , 1 1 , 1 z z z z z z z z z z z z R . III. Composition of subnets ,                                       = 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 1 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 1 1 0 0 0 0 0 0 1 0 0 G                     = ⋅ = 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 0 1 0 1 1 0 0 1 0 1 0 0 0 0 0 1 1 0 1 0 0 1 1 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 0 1 1 1 0 1 1 1 0 0 0 0 1 1 1 1 1 1 0 1 1 1 0 1 G R H .
B) Sequential edge composition (Fig. 6.6) .

2 2 4 4 2 2 4 4 Z1 Z2 Z3 Z4 Z4 Z3 Z1 , 2 Z1 , 2 Z4 , 3 Z1,2,4,3 Fig. 6.6. Sequential composition of net 3 N 1) 2 , 1 2 1 Z Z Z → +        = - = - = - = - . 0 : , 0 : , 0 : , 0 : 3 , 1 1 , 2 12 3 , 2 1 , 1 11 3 , 2 1 , 1 10 3 , 1 1 , 2 9 z z p z z p z z p z z p ,                 = 0 0 0 0 1 0 0 1 0 0 0 0 1 0 0 0 0 1 0 0 1 1 0 0 3 , 2 2 , 2 1 , 2 3 , 1 2 , 1 1 , 1 2 , 1 z z z z z z R                         = 0 0 0 0 0 0 1 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 1 1 1 0 1 1 0 0 0 0 1 0 0 12 11 10 9 7 6 5 3 2 1 2 , 1 p p p p p p p p p p G ,                 = 0 0 0 0 0 0 0 1 1 1 0 0 0 0 1 1 1 0 0 0 0 1 1 0 0 0 1 1 0 0 1 0 0 1 1 0 0 0 0 1 12 11 10 9 7 6 5 3 2 1 2 , 1 4 2 , 1 3 2 , 1 2 2 , 1 1 2 , 1 p p p p p p p p p p z z z z H . 2) 4 , 3 4 3 Z Z Z → +        = - = - = - = - . 0 : , 0 : , 0 : , 0 : 2 , 4 1 , 3 16 3 , 3 1 , 4 15 2 , 4 1 , 3 14 3 , 3 1 , 4 13 z z p z z p z z p z z p ,                 = 0 0 0 0 1 0 1 0 0 0 0 0 0 0 1 1 0 0 0 1 0 0 0 1 3 , 4 2 , 4 1 , 4 3 , 3 2 , 3 1 , 3 2 , 1 z z z z z z R                         = 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 1 0 1 0 1 0 1 0 0 0 0 0 0 0 0 1 1 1 0 0 0 1 0 1 0 0 0 1 0 0 0 16 15 14 13 8 7 5 4 3 1 4 , 3 p p p p p p p p p p G ,                 = 0 0 0 1 1 1 0 0 0 0 0 0 0 0 0 1 1 1 1 0 1 0 1 0 0 0 1 0 1 0 0 0 1 0
3)

4 , 3 , 2 , 1 4 , 3 2 , 1 Z Z Z → +        = - - + = - - + = - - + = - - + . 0 : , 0 : , 0 : , 0 : 2 , 1 3 2 , 1 1 4 , 3 4 4 , 3 2 7 4 , 3 4 4 , 3 1 2 , 1 3 2 , 1 2 5 2 , 1 4 2 , 1 2 4 , 3 3 4 , 3 1 3 4 , 3 3 4 , 3 2 2 , 1 4 2 , 1 1 1 z z z z p z z z z p z z z z p z z z z p ,                         = 0 0 1 0 0 0 1 0 1 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 0 1 0 0 0 0 1 1 1 0 0 1 1 0 0 0 1 1 4 , 3 4 4 , 3 3 4 , 3 2 4 , 2 , 1 4 2 , 1 3 2 , 1 2 2 , 1 1 ) 4 , 3 ( ), 2 , 1 ( z z z z z z z z R G ,                           = 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 1 0 1 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 1 ) 4 , 3 ( ), 2 , 1 (                     = = 1 1 1 1 0 0 1 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 0 0 0 1 1 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 0 0 0 0 0 1 1 1 0 1 1 1 0 0 0 1 1 1 1 1 1 0 1 1 1 0 1 ) 4 , 3 ( ), 2 , 1 ( H H .

Properties of Edge Collapse

We consider the graph of decomposition of a given Petri net into minimal functional subnets. Weight of an edge equals to the number of contact places connecting correspond pair of subnets. Let G is a given weighted graph. Without loss of generality, we consider as a connected graph, otherwise we may provide a collapse separately on the components.

v v = . Then ) , , ( \ W E V G e G ′ ′ ′ = ′ = , where V v U v v V }) , { \ 2 1 ( = ′
, where is a new vertex representing the fusion (collapse) of vertices :

v }, , { )) } , { } , { ( \ ( 2 1 2 2 1 1 2 1 E u v E u v V u vu E u v V u u v E u v V u u v v v E E ∈ ∨ ∈ ′ ∈ ∈ ∈ ∈ ∈ = ′ U U U      ∉ ∧ ∈ ∉ ∧ ∈ ∈ ∧ ∈ + = ′ . ), ( , ), ( , ), ( ) ( ) ( 1 2 2 2 1 1 2 1 2 1 E u v E u v u v W E u v E u v u v W E u v E u v u v W u v W vu W
Thus, at the fusion of vertices of an edge the edges incident with both vertices are fused.

) 1 ( - k k k k e G G e G G e G G G G \ \ \ 2 1 2 1 2 1 0 1 0 - -= → ⋅ ⋅ ⋅ → = → = → = .
Note that, obtained as the result graph consists of a single vertex. This perfectly corresponds to the name of process, which compress the source graph into a single vertex. The process of collapse may be represented by the sequence of fusing edges

1 - k G 1 2 1 ... - = k e e e σ .
As the major parameter of collapse we consider its width equalling to maximal weight of fusing edge.

Definition 12. Width of edge collapse

Width of edge collapse is the maximal weight of edge in the process of collapse:

) ( max ) ( e w d e σ σ ∈ = .
As will readily be observed the choice of different sequences of edges e in general case leads to various values of collapse width. We are interested in the sequences possessing the minimal width. Definition 13. Optimal collapse An optimal process of collapse (or briefly optimal collapse) denotes the sequence of edges, which provide the minimal width of collapse. The corresponding width of collapse is accordingly denoted by optimal width.

Optimal width of collapse is the property of a given graph. We introduce the recurrent definition for optimal width of collapse. Let us denote the optimal width of edge collapse of graph G as . Then ) (G d

   = = )), \ ( ), ( max( ) , ( ), , ( min ) ( e G d e w e G d e G d G d e
where the function of two arguments defines the optimal width of edge collapse of graph G under the condition the collapse of edge e will be executed firstly.

) , ( e G d

Edge collapse constitutes the combinatory task for solution of which we may apply the universal method of complete choice of all the possible sequences of edges. The exact number of different sequences equals to

∏ - = = 2 , 0 ) ( k i i E G K
. As at each step a pair of adjacent vertices is fused, the maximal number of adjacent vertices occurs for a complete graph. The number of

edges of the complete k -graph equals to 2 ) 1 ( - ⋅ k k . Then 1 - 2 1 , 2 2 ) ! ( 2 )! 1 ( ! 2 ) 1 ( ) ( ˆ-= ⋅ = - ⋅ = - ⋅ = ∏ k k k i k k k k i i G K 29 10 7 , 5 ) 20 ( ˆ⋅ = K 284 10 4 , 1 ) 100 ( ˆ⋅ = K .
For example and , . Thus, a search of effective methods of the solution of the task of edge collapse is required.

9 10 6 , 2 ) 10 ( ˆ⋅ = K
The choice tree of the collapse for net (Fig. 6.3) is represented in Fig. 6.7. We conclude that even for such a simple graph of decomposition we obtain widths of collapse, which distinguish in twice (8 and 4) for various sequences of collapse.

3 N Theorem 6.1. Width of collapse for acyclic graph equals to maximal weight of edge. Proof. Operation of edge collapse of acyclic graph leads to obtaining of new acyclic graph, witch contains the number of edges lesser by unit. Moreover, this operation does not change the weights of remained edges. Thus, width of collapse does not depend on the order of edges choice and equals to maximal weight of edge.

Any simple chain may be replaced by edge with minimal weight under the width of collapse equals to the maximal weight of edge. This corresponds to the choice of the edge of maximal weight on a step. Not limiting generality we may consider compact graphs does not containing simple chains and pendent vertices.

Proposition 1. If graph has cutvertices the width of collapse is equal to the maximum width of its 2-connected components (blocks).

+

Proof. Simple circle is transformed to the circle of lesser dimension until a triangle will be obtained. At the collapse of triangle a graph consisting of single edge with a weight equaling to the sum of edges' weights different from the fusing will be obtained. Thus, a width of collapse is defined on the one hand by maximal edge before fusion of triangle and on the other hand by the weight of the last edge. Consequently, the lower bound of width is the weight of maximal edge as well as summary weight of a pair of edges. Theorem 6.3. Optimal collapse of simple circle corresponds to the choice of the edge with maximal weight at a step. Proof. Collapse of a simple circle is executed without the change of weights of edges until a triangle will be obtained. The choice of a maximal edge guarantees that at the obtaining of triangle three edges of minimal weights remain. Moreover, at collapse of triangle the choice of maximal edge provides the choice of a pair of vertices with a minimal summary weight. Really, the following expression is valid: << of edges for current and previous levels in such a way that:

) ( min ) ( min )) ( ) ( ( min 2 1 2 1 , 1 2 1 2 1 e e e
i i i i i i i v e u e u u e + = ∨ = ⇔ << + + + 1 1 1 .
Partial lattice of collapse is the vivid representation of the process of edge collapse. According to the definition of collapse operation, at each step one of edges is canceled. If the end vertices of this edge do not have common adjacent vertices (do not form triangles together with other edges), then at the next level all the edges are contained with the except of the canceling. If the edge forms one or a few triangles, then each pair of edges of triangle is replaced by a single edge. The recurrent expression for the number of edges is l r

l i i - - = -1 1 ,
where r is the number of triangles constituting by the canceling edge. The lattice illustrates the relations of edges. Thus, each edge at a step of collapse constitutes either the edge of the source graph or the sum of some edges.

The lattices for two different sequences of collapse shown in Fig. 6.7 are represented in Fig. 6.8. The canceling edges are marked by cross. Proposition 6.3. Each edge at a step of collapse is a sum of some edges of the source graph.

Thus, width of collapse equals to the weight of an edge obtained at some step. Such an edge will be named a critical edge of collapse. Critical edge either is cancelled in the process of collapse or is remained by its last edge.

Since combinatorial way of solution of the optimal collapse task requires an exponential time, we have to apply more effective methods. For the application of method of branches and bounds [Jay 98,Schrejver 91] we have to construct estimations of upper and lower bounds of collapse width. We may improve the upper bound as

      ≤ ∑ ′ ≠e e e e w e w G d ) ( ), ( max ) (.
Really, at least one edge will be cancelled and the collapse width for the remained graph will not exceed the sum of its edges. Continuing the process described not more than ( times we come to the following estimation. Let is the maximal weight of graph's edge and is the minimal one. Then on the second step of collapse the edge with the weight not exceeding will be chosen and the collapse of remained part of the graph will not exceed ∑

. Continuing the estimations till the finish of collapse we obtain:

) 1 - k max e min e max 2 e ⋅ -2 ) (e w ⋅ min e ( ) ∑ ⋅ - - ⋅ - ≤ min max ) 2 ( ) ( , ) 2 ( max ) ( e k e w e k G d
.

On the other hand at the first step the edge with the weight greater than may not appear, at the second step and so on. We have recurrent expression: all the vertices fusing with the vertex v and by symbol v all the vertices fusing with the vertex . Firstly, vertices are non-adjacent in the source graph. Secondly, graph is connected. Therefore, at any step of collapse we obtain a vertex u , which is adjacent with as well as with v . Fusion of this vertex in graph G together with one of vertices leads to creation of edge . Further this edge may participate in the constituting of critical edge or will be simply cancelled.

1 v 1 2 2 v 2 1 , v v 2 1 v 2 2 1 , v v 1 v v e = ′
Let us consider the execution of operations mentioned in graph G e + . Before the obtaining of triangle composed of the edge e and a vertex u the process does not differ from early described. At fusion of vertex u together with one of vertices v we obtain instead of edge with weight an edge with weight

2 1 , v ) (e w ′ ) e ( ) ( w e w + ′
. Further this edge either will be included in the critical edge of collapse or will be simply cancelled. In the first case the width of collapse is increased by value , in the second case -is not changed. ) e ( w Corollary.

) ( ) ( ) ( e w G d e G d + ≤ + . )) ( ), ( max( ) ( e w G d e G d ≤ +
for pending edge (i.e. its degree is unit).

)

) ( ) ( max ), ( max( ) ( e w e w G d e G d G e + ′ ≤ + ∈ ′
for non pending edge.

In order to obtain more precise upper bounds we consider the process of adding of missing edges to any spanning tree of graph . Since the width of edged collapse of acyclic graph according to theorem 6.1 equals to maximal weight of edge, we may propose the following estimation of collapse width. G Theorem 6.5. Width of a collapse does not exceed the sum of weight of maximal edge of spanning tree and weights of remained edges:

∑ ∉ ∈ + ≤ R e R e e w e w G d ) ( ) ( max ) (
, where R is a spanning tree of graph . G

To improve the estimations we may choose a spanning tree of maximal weight for minimization of sum. As a good enough approximation we may consider the standard task of a maximal weight spanning tree choice [Berge 01,Harary 71]. Note that the number of remained edges equals to cyclomatic number of graph 1

) ( + - = k l G ν
. Then we may represent the estimation as:

. ) ( ) 1 ) ( ( ) ( max max e k l e G G d ⋅ - = ⋅ + ≤ ν
Estimations of lower and upper bounds may be applied at the solution of optimal collapse task via classic method of branches and bounds [Jay 98,Schrejver 91]. In the next section we propose simple and effective heuristic technique of solution.

Heuristic Technique of Collapse

Since the complexity of combinatorial solution via complete choice is exponential and obtained estimations of upper and lower bounds for organization of solution via method of branches and bounds are rough enough, we should to find a simple and effective technique of edge collapse.

Our interest in the precise methods is limited also by the fact we have not precise enough estimation of systems' complexity at the step of collapse because the estimation of number of basis nonnegative solutions of linear diophantine system is a difficult task. So, we use the number of places as the parameter of complexity.

According to results obtained for a simple chain and a simple circle we may suggest to choose the edge with a maximal weight at a step of collapse. We may choose the first or the random edge with the maximal weight in the case there are a few edges of maximal weight. Algorithm consists in pure implementation of collapse operation according to definition supplied with the rule for choice of edge with maximal weight. The complexity of such technique is about . Really, we have to execute

2 l k ⋅ 1 - k
steps and at each step we process not more than edges, for which at collapse of triangles we process not more than l incident edges. l For comparison of various rules of edge choice at a step of collapse we generated a random graphs and executed edge collapse of them. We compared the choice of maximal, minimal and random edge at a step. Results obtained are represented in Table 6.1. For construction of Table 6.1 we used random uniformly distributed weights of edges with range from 4 to 20. Usage of different else ranges leads to another absolute values but preserves the percentage. We conclude that the worst choice is the choice of minimal edge. It becomes close to random choice of edge under the growth of number of vertices. The best choice is the choice of maximal edge, which provides the essentially lesser width of collapse. Notice that, the greedy strategy does not always lead to the optimal result; Fig. 6.9 illustrates this fact. More precise (and more expensive) techniques involve several steps estimation implementing mini-max procedures [Levin 70,Jay 98]. For instance, in two-step algorithm we choose maximal edge, which provides minimum of the maximal weights of vertices at the next step.

Telecommunication Protocols Verification Using Composition of Functional Subnets

Protocol BGP Verification

Communication protocol BGP. The Border Gateway Protocol (BGP) [Loogheed 89] is an inter-autonomous system routing protocol. It is the very significant for the whole Internet operability, so the autonomous systems constitute a backbone of the global data exchange. More than thirty RFC (Requests For Comments) are devoted to BGP protocol specification and refinement. Recently the most widespread is BGP-4 [Rekhter 95], but the distinctions in comparison with the first standard specification [Loogheed 89] are the very specific and inessential for a draft model construction.

The primary function of a BGP speaking system is to exchange network reachability information with other BGP systems. This network reachability information includes information on the autonomous systems (AS's) that traffic must transit to reach these networks. This information is sufficient to construct a graph of AS connectivity from which routing loops may be pruned and policy decisions at an AS level may be enforced.

There are five types of standard BGP messages: 1 -OPEN, 2 -UPDATE, 3 -NOTIFICATION, 4 -KEEPALIVE, 5 -OPEN CONFIRM. After a transport protocol connection is established, the first message sent by either side is an OPEN message. If the OPEN message is acceptable, an OPEN CONFIRM message confirming the OPEN is sent back. Once the OPEN is confirmed, UPDATE, KEEPALIVE, and NOTIFICATION messages may be exchanged.

UPDATE messages are used to transfer routing information between BGP peers. The information in the UPDATE packet can be used to construct a graph describing the relationships of the various autonomous systems. By applying rules to be discussed, routing information loops and some other anomalies may be detected and removed from the inter-AS routing.

BGP does not use any transport protocol based keepalive mechanism to determine if peers are reachable. Instead KEEPALIVE messages are exchanged between peers often enough as not to cause the hold time (as advertised in the BGP header) to expire. The KEEPALIVE message is a BGP header without any data.

NOTIFICATION messages are sent when an error condition is detected.

Model of protocol BGP. Petri net model of protocol BGP is represented in Fig. 7.1. The model describes asymmetric interaction of two systems. First system is represented with places and transitions t , second system -with places and transitions . Places correspond to communication subsystem and model standard messages: OPEN, OPENCONFIRM, and KEEPALIVE. Notice that the model represents only procedures of connection establishment and maintenance, abstracting of data transfer for adjustment of routing tables. Date interchange is implemented in state ESTABLISHED with the aid of standard messages UPDATE. This process is not displayed in model constructed. Semantic description of elements of the model is represented in Table 7.1. Invariants of places. With the help of tool Tina [Berthomieu 04] we obtain the following basis invariants of the subnets enumerated in Fig. 7.2:

    = ⋅ = 1 1 1 1 0 1 0 0 1 1 1 1 1 1 1 2 1 1 12 11 5 3 2 1 1 , ) , ( ) , , , , , ( : G
G z z x x x x x x Z ,           = ⋅ = 0 1 0 0 1 1 0 1 0 0 0 0 1 1 1 2 2 2 3 2 2 2 1 14 13 5 4 3 2 , ) , , ( ) , , , , ( :
G G z z z x x x x x Z ,     = ⋅ = 1 1 0 0 1 0 0 0 1 1 1 1 3 3 3 2 3 1 12 11 10 8 7 6 3 , ) , ( ) , , , , , ( : G G z z x x x x x x Z ,        = ⋅ = 1 0 1 0 1 1 1 0 0 0 1 1 0 1 1 1 4 4 4 4 4 3 4 2 4 1 14 13 10 9 8 4 , ) , , , ( ) , , , , ( :
G G z z z z x x x x x Z .
The composition of the model is defined by fusion of eight contact places indicated in Fig. 7.2. Let us construct the system of equations for contact places:

             = - - = - - = - = - = - - = - - = - - + = - - + . 0 :
2 4 1 3 1 8 2 2 2 1 1 2 1 1 5 2 3 2 1 1 2 1 1 3 z z z p z z z p z z p z z p z z z p z z z p z z z z p z z z z p
The basis solutions of the system with respect to vector have the form

) , , , , , , , , , , ( 4 4 4
3 4 2 4 1 3 2 3 1 2 3 2 2 2 1 1 2 1 1 z z z z z z z z z z z                       = 0 1 1 0 1 1 1 1 0 1 0 0 1 1 0 0 1 1 1 0 0 1 1 0 0 0 1 0 1 1 0 1 0 1 0 0 0 0 0 1 1 0 0 1 0 0 0 0 1 0 0 0 1 1 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 R .
Let us assemble the joined matrix G of matrices G , , , . Notice that matrix may be constructed in different ways depending on the order of calculation of invariants for contact places. As each contact place is incident to two subnets, so its invariant may be calculated by two different ways.

1 2 G 3 G 4 G G                         = 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 1 0 1 1 1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 1 1 0 0 0 0 0 1 0 1 0 1 0 0 0 0 0 0 0 0 0 1 0 1 1 1 G .
After multiplication of matrices we obtain:

                      = ⋅ = 1 1 1 1 1 2 1 2 1 1 0 1 0 1 1 1 0 0 1 2 1 1 1 1 0 1 1 1 1 1 1 1 0 1 0 1 0 1 0 1 0 1 1 1 0 0 0 1 0 0 0 1 0 1 1 1 0 0 1 1 0 0 0 1 0 1 1 1 0 1 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 G R H .
Notice that the source system has five basis solutions so sixth solution is the sum of second and fourth, and seventh -the sum of second and fifth.

Therefore, the model of BGP protocol is p-invariant so, for instance, invariant, ( )

1 1 1 1 1 2 1 2 1 2 1 2 1 2 = * x ,
which is the sum of second, third and fourth basis invariants, contains all the natural components. Consequently, the model of protocol is safe and bounded. For any reachable marking it holds that 3 * = ⋅ µ

x .

p

Invariants of transitions.

To calculate invariants of transitions we construct the dual Petri net (Fig. 7.3), decompose it (Fig. 7.4) and implement the technique described for place invariants. The decomposition contains six minimal functional subnets. For calculation of invariants, it is convenient to consider the decomposition into two functional subnets. Since subnet 1 Z ′ consists of 9 transitions, we may compose remained minimal subnets into one subnet with 5 transitions.

The following matrix represents the basis invariants of transitions:

        0 1 1 1 0 0 0 1 1 1 0 0 1 0 1 1 1 1 1 0 1 1 1 1
As, for instance, the sum of two basis invariants ( ) , where is the number of nodes of net. q 2 q Notice that even such rather tiny model allows the speed-up of computations. At calculation of place invariants, instead to solve the system of dimension 12, we solved five systems with the dimension not exceeding 8. If we not take into accounting polynomial multipliers, then we obtain sixteen fold ( 16 2 2 8 12 = ) speed-up of computations.

1 1 2 2 1 1 1 1 2 2 1 1 * =
Notice that, speed-up have been obtained for the net numbering about dozen of nodes. At investigation of large-scale nets, the speed-up may be rather huge [Zaitsev 04f,05], so it is estimated (5.10) as exponential function , where

Protocol ECMA Verification

Model of communication protocol ECMA. Protocol ECMA (European Computer Manufacturer Association) is transport protocol situated between network and session levels of ISO model. Further, the model of protocol represented in [Berthelot 82] will be used. On the one hand, the model is simplified enough to be studied in article, on another hand, it allow the implementation of decomposition technique. Further studying model represents only connection-disconnection processes and abstracts of the concrete way of data transmission.

Petri net model of protocol ECMA is represented in Fig. 7.5. Three basic parts of model is considered: left interacting system -places Z and also decomposition in subnets of connection establishing and disconnecting 1 Z′ , 2 Z′ , where

2 , 1 1 1 , 1 Z Z Z + = , 2 , 2 1 , 2 2 Z Z Z + = , 1 , 2 1 , 1 1 Z Z Z + = ′ , 2 , 2 1 , 2 2 Z Z Z + = ′ .
Invariancy of protocol ECMA. We use the isomorphism of subnets 1 Z and 2 Z . Firstly, we calculate invariants of subnet 1 Z . Then we construct invariants of isomorphic net 2 Z . And finally, we calculate invariant of whole given Petri net.

Invariants of subnets where matrices and G have the following form:

1 , 1 G 2 , 1 0 1 1 0 0 0 0 0 0 0 0 1 1 1 0 0 1 1 0 0 1 1 1 0 0 1 0 0 1 0 0 1 1 0 1 1 , 1 = G , 0 0 0 0 1 1 1 0 1 0 1 0 0 1 1 0 1 0 0 1 0 2 , 1 = G .
Note that, components of vector x , corresponding to subnets . We construct the system of equations of form (5.6) for contact places:

   = - - + + = - - + + . 0 , 0 2 3 2 1 1 4 1 2 1 1 2 3 2 2 1 4 1 3 1 1 z z z z z z z z z z
Note that, in composition of subnets G and G places and are contact ones. General solution has the following form

1 , 1 2 , 1 1 p 3 p 1 2 3 2 2 2 1 1 5 1 4 1 3 1 2 1 1 ) , , , , , , , ( R y z z z z z z z z ⋅ = , 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 1 0 0 1 0 0 0 1 0 0 1 0 0 0 1 0 0 1 0 0 0 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 1 0 0 0 1 = R .
For calculation of basis invariants of net 1 Z according to (4) we construct of subnets' invariants G and G a joined matrix G :

1 , 1 1 , 2 1 0 0 0 0 0 0 0 0 1 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 1 1 0 0 0 1 0 0 0 0 1 1 0 0 0 1 0 0 0 0 0 0 1 0 0 1 0 1 0 1 1 = G or 0 0 0 0 0 0 0 0 1 1 0 1 0 1 0 1 0 0 0 0 0 0 0 1 1 0 1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 1 = G .
Note that, the difference between matrices is contained in columns corresponding to contact places ( and ). In the first case invariants of contact places are calculated according to matrix G , and in the second case -according to . Indexation of columns corresponds to vector ( .

1 p 3 p , , 2 x 1 , 1 1 x 1 , 2 G ) , , , , , , , ,
0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 1 0 0 1 1 1 0 1 1 0 1 0 1 1 0 0 0 1 0 0 0 1 0 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 0 0 1 0 1 0 1 1 1 1 1 0 0 0 0 0 1 1 1 1 = H .
Note that, after a calculation of product G R ⋅ according to (5.9) we have deleted linearly dependent rows in matrix.

Further, in the same way, we construct invariants of whole net, that is the composition of subnets 1

Z and 2 Z . System of equations for contact places has the following form:

             = - - - + + = - - - + + = - - - + + = - - - + + = - - + + = - - - + = - - - + = - - + + . 0 : , 0 : , 0 : , 0 : , 0 : , 0 : , 0 : , 0 : 2 4 2 2 2 1 1 5 1 2 1 1 16 2 5 2 2 2 1 1 4 1 2 1 1 15 2 4 2 2 2 1 1 5 1 2 1 1 14 2 5 2 2 2 1 1 4 1 2 1 1 13 2 7 2 4 1 6 1 5 1 2 12 2 6 2 4 2 2 1 7 1 5 11 2 6 2 5 2 2 1 7 1 4 10 2 7 2 5 1 6 1 4 1 2 9 z z z z z z p z z z z z z p z z z z z z p z z z z z z p z z z z z p z z z z z p z z z z z p z z z z z p
Let us solve a system, calculate a product G R ⋅ and delete linearly dependent rows. We obtain basis invariants of Petri net as follows:

0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 0 1 1 1 0 1 1 1 0 1 0 1 0 0 1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 0 0 0 0 1 0 1 0 0 0 0 0 0 1 0 0 1 0 0 0 0 1 1 0 1 0 0 0 0 0 1 1 0 1 1 0 1 0 0 0 0 1 1 1 1 0 1 1 0 0 1 0 1 0 1 1 1 1 1 1 1 1 0 0 1 0 1 1 1 0 1 0 1 = H .
Result obtained coincides with invariants calculated with usual methods for whole net and also with invariants obtained with direct composition of four minimal functional subnets.

Thus, Petri net is invariant so, for instance, the invariant ( ) Source net contains 16 places, thus, direct calculation of invariants require solving a system with 16 unknowns. Composition of four minimal subnets requires solving system of the size 7 to obtain invariants of minimal subnets and to solve a system of the size 12 to obtain invariants of contact places. Sequential composition assumes solving system of the size 7 to obtain invariants of minimal subnets, solving system of the size 5 to obtain invariants of contact places of first composition and solving system of the size 8 to obtain invariants of contact places of second composition. Note that, at the exponential growth of functions, the complexity of matrices multiplication representing by polynomial of third degree is irrelevant and will not be considered.

1 1 1 1 1 1 1 1 1 2 1 2 1 2 1 2 * = x ,
Complexities of calculation for each of enumerated three ways of invariants obtaining may be estimated by following expressions: It should to be noted, that speed-up has been obtained for net numbering three tens of nodes. At research of large-scale nets, the acceleration may be rather huge, so it is estimated as exponential function (5.10).

Protocol TCP Verification

Specifications of protocol TCP. TCP is the major transport protocol of Internet. Namely via protocol TCP more than two hundreds petabits of public and private information is transferred per day. Therefore, a formal proof of TCP protocol correctness has a key significance for the grounding of modern global networks reliability.

Standard specification of protocol TCP has been presented in year 1981 in RFC 793 [Postel 81]. This document had become the result of prolonged discussions reflected, for instance, in RFC with numbers 44, 55, 761. In the process of exploitation, it was made alterations concerned with such items as slow start RFC 1122, quick recovery RFC 2001, repetitive transmission RFC 2988. The improvement of standard is not ceased at present. It is confirmed, for instance, by RFC 3360, 3481, 3562, which propose technique of reliable interaction at connection reset, special rules for wireless lines connections, algorithms of keys exchange for protection of information.

Petri

G z z z z z z x x x x x x x x x ⋅ =
where the matrices have the form

0 1 1 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0 1 1 0 0 1 0 1 1 0 0 0 0 1 0 0 0 0 1 1 1 0 0 0 0 1 1 1 1 1 2 1 = = G G ,
Notice that, components of vectors j x corresponding to subnets 1 Z and 2 Z are written in explicit form. They define the indexation of columns of matrices constructed. Indexes of rows correspond to components of vectors ) , , , , , (

1 6 1 5 1 4 1 3 1 2 1 1 1 z z z z z z z = , ) , , , 2 6 2 5 2 4 2 2 2 z z z z z , , 2 3 z ( 2 1 z = .
Let's construct the system of equations with the form (5.6) for contact places:

3 1 2 1 1 ) , , , , , , , , , , , ( R y z z z z z z z z z z z z ⋅ = , 0 0 0 0 1 0 0 1 0 0 0 0 1 0 0 0 0 0 0 1 1 0 0 0 0 1 0 0 0 0 0 0 0 0 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 = 2 , 1 R .
For calculation of basis invariants of net according to (5.9), we construct the joint matrix G out of invariants of subnets and G :

2 , 1 Z 2 2 , 1 1 G 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 0 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 0 1 0 1 1 0 0 0 0 0 0 0 0 0 1 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 0 1 1 1 1 1 = 2 , 1 G .
The indexation of columns corresponds to vector

, 1 2 , 1 2 , 1 G R H ⋅ = 0 0 1 1 1 1 0 0 0 1 0 0 0 0 0 0 0 0 0 1 0 0 1 1 0 0 1 1 1 0 0 0 0 0 1 0 0 0 0 1 1 1 1 0 0 1 1 0 1 1 0 0 0 0 0 0 0 0 0 1 1 0 0 1 0 1 1 0 0 0 1 1 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 = 2 , 1 H . • Composition: Z4+Z3
The invariants of subnets 4 Z and may be represented as

G z z z z z z x x x x x x x x x x x x ⋅ =
where the matrices have the form

0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1 0 0 0 0 0 1 0 1 0 0 0 1 0 0 1 0 1 0 0 0 1 0 1 0 1 1 0 1 0 1 0 0 0 0 1 1 1 1 1 1 1 1 3 4 = = G G .
System of equations for contact places has the form: The general solution of system may be represented as

1 0 0 1 1 1 1 1 1 1 1 0 0 1 1 0 0 0 0 0 1 1 1 0 0 0 0 0 1 0 0 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0 0 0 0 0 1 1 0 0 0 0 0 0 1 0 0 1 0 0 1 0 1 1 0 1 0 0 1 1 1 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 1 1 0 0 0 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 1 0 0 1 1 1 0 0 0 1 1 0 0 1 1 0 1 0 0 1 0 1 1 0 0 0 1 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 1 1 0 1 0 0 1 0 1 0 0 0 0 1 0 0 0 0 1 0 0 1 1 0 0 0 0 0 0 1 1 1 = H
Since, for instance, the sum of all the rows has all the natural components, model of protocol is p-invariant and, consequently, it is bounded and safe net.

In the same way, using dual net and decomposition, it may be shown that model is tinvariant also. It means that net is persistent and constitutes the necessary conditions for its liveness.

Notice that, expenses of time for invariants calculation via stepwise composition of functional subnets completely corresponds to exponential estimations of speed-up (5.10). The total time for construction of basis invariants of places did not exceed 10 seconds on computer Pentium (3.2 GHz CPU, 0.5 Gb memory).

Conclusions 58

In present work the concept of functional subnet of Petri net was introduced and studied. The properties of the set of functional subnets were investigated. Two different techniques of generating set of functional subnets construction were studied: with logic equations and with an ad-hoc algorithm. It was shown that the time complexity of algorithm is linear. Program realization of algorithm was implemented. Together with [Zaitsev 90,97], where formal description of transmission function for functional timed Petri net was obtained, the present work gives the complete technique of nets' properties analysis based on obtaining of functional subnets, algebraic description of their transmission function and consequent equivalent transformations.

Basis of compositional analysis of Petri nets is constructed. It is aimed to speed-up of Petri net properties determination with the aid of linear algebra methods based on fundamental equation of net and invariants. For investigation of Petri nets properties it is requires to solve systems of linear Diophantine equations over nonnegative integer numbers. All known methods of such systems solution have exponential calculation complexity. The technique proposed and studied in paper allows the speed-up of calculation of invariants. This technique is based on the decomposition of Petri net into functional subnets and consequent composition. The speed-up obtained is exponential with respect to the number of places of source Petri net. The technique also allows the speed-up of the fundamental equation solution.

Analysis of real-life models of systems and processes numbering thousands of elements with early known methods was practically unrealisable task so it required calculation expenses measuring by years. Application of compositional analysis allows the exponential speed-up of computations and in that way to cut essentially a time of tasks solution.

Decomposition-based solution of state equation and calculation of invariants consists in two major stages: solution of systems for minimal functional subnets and solution of system for contact places. At large-scale nets analysis the number of contact places may be huge enough. This implies the increase of overall calculation complexity.

Sequential composition is aimed to decrease the dimension of solving systems. Instead of one system of a huge dimension for contact places we propose to solve a sequence of systems with essentially lesser dimension. At exponential complexity of system solution this technique provides a considerable additional speed-up of computations. Decomposition was presented with weighted graph, which is transformed to a single vertex at sequential composition. The corresponding task was named a collapse of weighted graph. Edge or pairwise collapse has been chosen as the most effective kind of collapse. Width of collapse equals to maximal weight of edge and corresponds to maximal dimension of solving system.

Properties of edge collapse were studied. Upper and lower bounds for width of collapse, which may be applied in the solution of the task with methods of branches and bounds, were obtained. Simple and effective heuristic algorithm of edge collapse based on maximal weight edge choice was proposed. It was applied to a series of automatically generated random graphs. For small graphs we showed that result is close to optimal. For huge graphs we obtained results essentially better than for random collapse. Results obtained prove the practical value of sequential composition for additional speed-up of state equation solution and invariants calculation.

The obtained results are illustrated by examples of telecommunication protocols verification with the help of the decomposition of Petri net models into functional subnets and their composition. Speed-up of invariants calculation was obtained for such well-known protocols as BGP, ECMA, TCP.

  Fig. 2.2. Decomposition of Petri net into minimal functional subnets 1 N

  Fig. 2.3. Types of contact places

  Fig. 3.1. Net of minimal functional subnets of Petri net z N 1

Fig

  Fig. 3.3. Non partitionable net 2 N

  Fig. 5.1. Petri net 2 N Fig. 5.2. Dual Petri net 2 Ñ

Z

  and C is the set of contact places. According to definition, any place is incident only to transitions from the set place will appear only in the one subsystem . That is why we have to solve only equations for contact places from the set C .

Z

  and C is a set of contact places. According to definition each internal place is incident only to transitions from set corresponding to this place is contained only in system . Consequently, we have to solve only equations for contact places from set C .

  the form (5.11), consequently, its general solution has the form (5.14):

  2

  .2 b). Let us consider the basic ways of composition of functional composition.II. Sequential composition: 1) Pairwise (edge); 2) Subgraphs.

  Fig. 6.1. Collapse of Subgraphs

  the decomposition of Petri net into minimal functional subnets. We consider the dimensions of systems used at compositional solution of source system. It is required

  Fig. 6.2. Process of Edge Collapse

  Fig. 6.3. Petri Net -Model of Telecommunication Protocol 3 N

  Operation of edge collapse We define the operation of edge collapse G for an edge e \ E e ∈ in such a way. Let e 2 1

  Fig. 6.3. Partial Lattice of Collapse

  are rough enough, we consider the process of addition of the edges connecting a pair of non-adjacent vertices. Let us study the influence of this operation on the width of collapse.Theorem 6.5. The addition of edge connecting non-adjacent vertices increases the width of collapse not more than by the weight of edge added.Proof. Let the width of collapse of graph G equals to and is reached by the sequence) (G d σ . Let us consider graph G e+ and execute its collapse with the help of the same sequence σ Under the execution of collapse operation we shall mark by symbol

  Fig. 6.9. An Example of Collapse

  Fig. 7.1. Petri net model of protocol BGP

  Fig. 7.2. Decomposition of BGP protocol model

Fig. 7

 7 Fig. 7.4. Decomposition of dual Petri net into functional subnets

  is the number of contact places.

Fig. 7

 7 Fig. 7.5. Model of protocol ECMA

Fig. 7

 7 Fig. 7.6. Decomposition of protocol ECMA

Z

  , are written in explicit form; they define indexation of columns of constructed matrices. Indexes of rows correspond to components of vectors )

  allowed the acceleration more than ten times in the comparison with traditional methods. Moreover, sequential composition allowed the additional tenfold speed-up.

  Fig. 7.7. Petri net model of protocol TCP

}

  This system has 48 basis solutions constituting matrix R : Let us construct the joint matrix G out of invariants of subnets G and :

  Sets of internal places of two arbitrary minimal functional subnets Z′ and Z ′ ′ of Petri net N do not intersect.

	Corollary 2. Set of minimal functional nets ℑ	}	,	defines a partition of set T
	into no intersected subsets

4 Technique of Decomposition into Functional Subnets 4.1 Decomposition via Logical Equations

  The partition of set T defined by the set of minimal functional subnets is the generating family for the set of functional subnets of Petri net N.

																								1 p
									1 Z +				Z	2			1 t
														p	2							p	3
										t	5											t	2	t	3
																								p	5	p
							Fig 3.4. Functional subnet	1 Z +	Z	2	of Petri net 1 N
	The above theorem may be illustrated with Fig. 3.4 showing a net that is the sum of two
	minimal functional subnets of Petri net				presented in Fig. 2.2.
	A functional subnet	0 Z =	(	P	2	,	P	0	,	P	3	,	T	0	)	of a Petri net	N =	(	P	,	T	,	F	)	will be considered.
	Let				, according to Proposition 2.2, be a functional subnet	.
	Interconnection of pointed subnets is illustrated in Fig. 4.1.
										so		B	(S	)	is connected with nodes of subnet	Z ′ only by means of
	contact places and, moreover, since j Z is functional subnet of N, so	B	(S	)	is connected with
	nodes of subnet	N -	Z	j	also only by means of contact places. Besides, for input and output
	places	B	(S	)	are held all the constraints of functional subnet. Therefore, functional subnet	Z	j
	contains functional subnet	B	(	S	)			that contradicts with minimality of	j Z . Contradiction
	obtained proves the false of source assumption about that	S	≠	∅	. Thus, T ′ contains set j T
	entirely that according to arbitrary choice of j T proves the theorem.

1

N

Corollary.

Let us construct equations in predicate calculus of the first order defining what subset the place or transition belongs to. It will be used definition of functional subnet and also that according to Proposition 2.2 net

	N -	Z	0	1	(	3	,	1	,	2	,	1	)

  Theorem 5.4. Solution x′ of fundamental equation for Petri net is the solution of fundamental equation for each of its functional subnets. As x′ is the solution of fundamental equation for Petri net , so N x′ is a nonnegative integer solution of system (2) and consequently x′ is a nonnegative integer solution for each of equations . Thus

		i L
	Therefore the system representing the fundamental equation for functional subnet Z′ ,
	Z f ′	N	is a subset of set {	i L	}	and vector	x′ is its solution. Consequently x′ is the solution of
	fundamental equation for functional subnet Z′ . Arbitrary choice of subnet	in above
	reasoning proves the theorem.

N Proof. i L

x′ is a solution for an arbitrary subset { .

} i L According to Definition 4, a functional subnet Z′ , N Z f

′ is generated by the set of its own transitions T ′ . Thus, an equation corresponding to a transition of subnet has the same form as for the entire net, so subnet contains all the incident places of source net.

N Z f ′

Theorem 5.5. Fundamental equation of Petri net is solvable if and only if it is solvable for each minimal functional subnet and a common solution for contact places exists.

Table 5 .

 5 1. Necessary and sufficient conditions for structural properties of Petri nets

	Structural property	Necessary and sufficient conditions
	Boundness

  Proposition 6.1. Edge collapse preserves the connectivity of graph.

	S	Proposition 6.2. The following expression for the sum of edges' weights is valid . ) ( ) ( ) e w G S G ( + ′ =
		According to terminology [Berge 01, Harary 71], graph with	k V = and	l E = we call
	, ( l k	)	-graph or -graph. Since at execution of edge collapse operation a pair of adjacent k
	vertices is fused, the edge collapse of entire graph consists in sequential execution of	( -k	) 1
	operations of edge collapse.

Definition 11. Process of sequential edge collapse Process of sequential edge collapse of -graph (or briefly edge collapse) is a sequence of operations of edge collapse: k

Table 6 .

 6 1. Comparison of Collapses for Random Graphs

	Number	Density	Simultaneous			Sequential Collapse
	of	(%)	Collapse,	Maximal Edge	Random Edge	Minimal Edge
	Vertices		Width	Width	Percent	Width	Percent	Width	Percent
			442	35	7.9	191	44.6	231	52.3
	20		869 1372	66 102	7.6 7.4	367 651	42.2 47.4	533 829	61.3 60.4
			1825	160	8.8	876	48.0	990	54.2
			1836	73	4.0	632	34.4	1002	54.6
	40		3699 5539	139 214	3.8 3.9	1664 2665	45.0 48.1	2133 2948	57.7 53.2
			7354	314	4.3	3608	49.0	3908	53.1
			11602	160	1.4	4827	41.6	5829	50.2
	100		22973 34334	316 501	1.4 1.5	7617 13282	33.2 38.7	12341 17559	53.7 51.1
			45582	754	1.7	17144	37.6	23008	50.5
			46073	288	0.63	19673	42.7	23781	51.6
	200		91715 137684	612 997	0.67 0.72	42260 67609	46.0 49.1	91715 68957	50.5 50.0
			183652	1486	0.81	91015	49.6	91669	49.9

Table 7

 7 Z constitutes a sum of two minimal subnets induced by transitions t and correspondingly. Problems of the functional subnets composition out of the minimal functional subnets were studied in[Zaitsev 04b, 04e].

	.1

  It may be easily explained by the model does not represent timeouts provided by the source specifications. With additional transitions returning each system from the ESTABLISHED to the IDLE state the model becomes live.

				y
	contains all the natural components, so the model of protocol BGP is t-invariant. Therefore,
	the model is consistent. Sequence	σ	*	=	1 t t	7	t	8	t	2	t	3	t	9	10 t	11 t t	4	t	5	t	3	t	9	10 t	12 t	t	4	t	6	, corresponding to
	invariant	* y , provides	µ	0	0 → . * µ σ
	Notice that, though the model of protocol BGP is invariant, it contains deadlocks and ) 11 8 2 , , p p ( ) 13 6 4 , , p p p , reached via sequences t and 6 11 4 10 9 3 2 8 7 1 t t t t t t t t t t correspondingly. 1 3 5 12 4 t t t 10 9 3 2 8 7 p 1 ( t t t t t t t t
					p' 6
																		t6'
		p' 11
	t' 1				t' 7													p1'											t7'
	p' 2																		t1'												p7'	t9'
																					Z2'
		p' 12
	t' 2				t' 8																										t8'	p9'
																															Z3'
					p' 8			t' 12
																															t10'
		p' 13																													Z4'
	t' 3				t' 9															t5'											t2'
	p' 4			t' 11															p3'											t4'	Z6'
		p' 14
	t' 4				t' 10															t3'									Z5'	p5'
					p' 10			Z1'																						t5'	t6'

Table 7

 7

	.2

  that is the sum of basis invariants with numbers 1, 3 and 9, contains all natural components. Therefore, model of protocol ECMA is safe and bounded.It should to note, that though net is also t-invariant one, it contains a deadlock with tokens in places and . Net reaches this deadlock as a result of firing sequence t or t . Let us estimate obtained speed-up of computations in the assumption of exponential complexity of algorithms[Kryviy 99] for solving of linear Diophantine systems in nonnegative integer numbers. Let the complexity is , where is number of nodes of net.

	p	9	11 p	1 t	5	1 5 t
	Speed-up of invariants calculation.

& & & & ( & ) & & & & ( &

, v 1 v

p p -

t t -

p p -

Z

Acknowledgement of disconnection

Acknowledgement

Thanks a lot to Paris-Dauphine University, Lamsade and especially to Serge Haddad for invitation and brilliant conditions for scientific work. Smart comments of colleagues allow the refinement of early collected papers during preparation of this report.

Decomposition of protocol ECMA. We decompose the source model of ECMA protocol represented at Fig. 7.5 in minimal functional subnets. Application of decomposition algorithm to model of ECMA protocol (Fig. 7.5) results in obtaining of set { consisting of four minimal functional subnets represented in Fig. 7

Invariance of TCP protocol model. In [Berthelot 82] it was shown that a correct telecommunication protocol has to be invariant one. Known methods of invariants calculation [Kryviy 99] have exponential complexity that makes its application difficult for investigation of real-life objects' models numbering thousands of elements. The model of protocol TCP (Fig. 7.7) allows the convincing illustration of this fact. However, net contains only 30 places and 28 transitions, the calculation of basis invariants for natural generators by known tool Tina [Berthomieu 04] had not been completed in 24 hours.

Let us consider the graph of decomposition (Fig. 7.9). In [Zaitsev 04f] the sequence shown in Fig. 7.9 a) was implemented. Maximal number of equations equals to 8 in spite of 12 for simultaneous composition. We implement stepwise composition for protocol TCP model according to optimal sequence represented in Fig. 7.9 b). It guarantees the maximal number of equations equaling to 4.

Let us enumerate places according to We implement the sequence of stepwise composition represented in Fig. 7.3 b).

• Composition: Z1+Z2

With respect to numeration of places defined by Table 7.3 the invariants of subnets 1 Z and 2 Z may be represented as:

The indexation of columns corresponds to vector

System of equations for contact places has the form:

Matrix of basis solutions after the erasing of nonminimal solutions has the form: