03964.com

文档资料库 文档搜索专家

文档资料库 文档搜索专家

INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE

On the synthesis of general Petri nets

Eric Badouel and Philippe Darondeau

N ? 3025

novembre 1996

` THEME 2

apport de recherche

ISSN 0249-6399

On the synthesis of general Petri nets

Eric Badouel and Philippe Darondeau

Theme 2 | Genie logiciel et calcul symbolique Projet Micas Rapport de recherche n 3025 | novembre 1996 | 29 pages dinello for synthesizing pure weighted Petri nets from nite labeled transition systems. The limitation to pure nets, serious in practice e.g. for modelling waiting loops in communication protocols, may be removed by a minor adaptation of the algorithm, working for general Petri nets red sequentially. The rule of sequential ring reduces also the expressivity of Petri nets, since it forces a concurrent interpretation on every diamond. This limitation may also be removed by leaving sequential transition systems and lifting the algorithm to step transition systems, which amounts to extract the e ective contents of the core ection between Petri step transition sytems and general Petri nets established by Mukund. By the way, the categorical correspondences between transition systems or step transition systems and nets are re-examined and simpli ed to Galois connections in the usual setting of ordered sets. Key-words: Synthesis Problem for Nets, Higher-Dimensional Automata, Polynomial Algorithm, Galois Connection

(Resume : tsvp)

Abstract: A polynomial algorithm was given by the authors and Bernar-

This work was partly supported by the h.c.m. Network Express. Email: fEric.Badouel, Philippe.Darondeaug@irisa.fr

Unit? de recherche INRIA Rennes e IRISA, Campus universitaire de Beaulieu, 35042 RENNES Cedex (France) T? l? phone : (33) 02 99 84 71 00 – T? l? copie : (33) 02 99 84 71 71 ee ee

Resume : Les auteurs ont donne avec Luca Bernardinello un algorithme polynomial pour la synthese de reseaux de Petri purs a partir de systemes de transitions. La restriction aux reseaux purs s'avere tres contraignante par exemple lorsque l'on veut modeliser des boucles d'attente dans des protocoles de communication. Cette limitation peut ^tre levee par une adaptation mie neure de l'algorithme, utilisable pour des reseaux de Petri generaux executes de maniere sequentielle. La regle de tirage sequentielle est elle-m^me limitae tive puisqu'elle interprete comme independentes en un etat toutes les actions qui y sont executables dans un ordre arbitraire. Cette seconde limitation peut aussi ^tre levee en adaptant l'algorithme aux systemes d'hypertransitions e (step transition systems), ce qui revient a extraire le contenu algorithmique de la core ection etablie par Mukund entre les reseaux de Petri et les systemes d'hypertransitions de Petri. Nous indiquons egalement comment les correspondances categoriques entre reseaux et automates peuvent se presenter plus simplement en terme de connexions galoisiennes. Mots-cle : Synthese de reseaux, automate de dimension superieure, algoritmes polynomiaux, connexion galoisienne

Sur la synthese des reseaux de Petri generaux

On the synthesis of general Petri nets

3

1 Introduction

Following Ehrenfeucht and Rozenberg's seminal work on regions in Partial 2-Structures ER90a], various correspondences between automata and net systems, based on regions in automata, have been established and analysed. The reference papers for the basic correspondences are ER90b] or NRT92] in the frame of C/E-nets or elementary nets, and Mu92] in the frame of P/T-nets. Variant correspondences have been studied respectively in NW94] BD95a] and in DS93] DS96]. According to the uni ed presentation of regions given in BD95b], a region in a xed automaton w.r.t. a xed type of nets is a morphism from the underlying transition system to the marking graph of a one-place net of that type, with one event representative of each typical relationship between places and events. Regions may be seen as places with attached ow arcs, thus nets may be assembled from subsets of regions. An automaton gives rise in this way to an ordered family of subnets of a maximal net whose set of places is just the set of regions of the automaton. The point is to decide whether this maximal net or some of its subnets reproduces in turn the original automaton (up to isomorphism) as the associated graph of reachable markings. The essential contribution of ER90b] and NRT92] is the isolation of two characteristic axioms for automata isomorphic to graphs of reachable markings. These axioms require from their models enough regions to separate all di erent states in an automaton and to rule out all missing events at each state. Based on the separation axioms, various core ections between categories of automata and nets have been established in the literature. These core ections may also be obtained in a systematic way as induced restrictions of a general adjunction between automata and net systems, parametric on the type of nets, restricted on models of the separation axioms BD95b]. The e ective or algorithmic contents of the above correspondences have been analysed in a handful of papers. A crucial fact was observed in DR96]: any set of regions large enough to witness for satisfaction of the separation axioms, and therefore said admissible, is the set of places of a net system which reproduces the given automaton as a graph of reachable markings. Exhibiting the net system when it exists is known as the synthesis problem. The synthesis problem for elementary nets, examined further in the case of nite automata in Ber93] and Hi94], and proved NP-complete in BBD95a], was

RR n 3025

4

E. Badouel & Ph. Darondeau

given an approximate solution in algorithmic form in CKLY95]. The precise problem decided upon by the algorithm is whether the given automaton has some quotient isomorphic to the reachable marking graph of some net system. The synthesis problem for pure Petri nets, examined further in BDPV96] in the frame of nite automata, was solved in BBD95b] in time polynomial in the size of automata. The resulting algorithm has been used in a few experiments, carried out in view of the automated distribution of protocols. In this context, the requirement to preprocess the genuine automaton which represents a given protocol, so as to split its loops into cycles, was found inconvenient. One goal of the present paper is to lift this impractical constraint: we provide an adaptation of the synthesis algorithm working in polynomial time for general Petri nets with the sequential ring rule. The other goal of the paper is to show that the algorithm is robust, by jumping from sequential transition systems to step transition systems, as de ned by Mukund Mu92]: we provide a second adaptation of the synthesis algorithm, working in polynomial time for Petri nets with the step ring rule. The remaining sections of the paper are organized as follows. Section 2 recalls from BD95b] the general de nition of regions, parametric on the type of nets, and recasts in this mould the abstract correspondence between sequential transition systems and nets with the sequential ring rule. The categorical correspondence established in BD95b] is presented here in the simpler form of a Galois connection. Section 3 focuses on Petri nets. A polynomial synthesis algorithm is produced, based on the adaptation of principles inherited from the weaker algorithm for pure Petri nets de ned in BBD95b]. Section 4 carries the abstract correspondence between transition systems and nets to step transition systems and nets with the step ring rule. Section 5 presents an upgraded version of the algorithm which solves the synthesis problem in this richer context.

INRIA

On the synthesis of general Petri nets

5

2 Galois connection between automata and net systems

A dual adjunction between automata and net systems, parametric on the type of nets, has been constructed in BD95b]. Our purpose in this section is to account for this correspondence without the help of categories. We shall therefore construct a Galois connection between automata and net systems. We shall identify the kernel of the connection, yielding a relation of duality between separated automata and saturated net systems. Given a separated automaton, the dual net system is assembled from regions in the automaton, seen as places of the net. We shall also isolate admissible subsets of regions characteristic of separated automata, and thereby lay the grounds for the investigation of algorithmic solutions to the synthesis problem, pursued in section 3. Before stating general de nitions for automata, nets and regions parametric on the type of nets, let us indicate a slight di erence between the correspondences established below and in BD95b]. Given a net system with set of events E , the set of events of the dual automaton is E in the present paper, while it was a quotient of E in the former work. The import of this distinction is not yet completely clear. We reserve the appellation of automata to initialized transition systems A = (S; E; T; s ), with set of transitions T S E S and initial state s 2 S . The underlying transition system UA = (S; E; T ) is always assumed to be e deterministic, meaning that for any state s 2 S and event e 2 E , (s ! s0 ) e 00 2 T ^ (s ! s ) 2 T ) s0 = s00. Recall that a morphism of transition systems ( ; ) : (S; E; T ) ! (S 0; E 0; T 0) is a pair of maps : S ! S 0 and : E ! E 0 e e such that (s ! s0) 2 T ) ( (s) ! (s0)) 2 T 0. Automata are always assumed to be accessible, meaning that S is the inductive closure of the singleton set fs g w.r.t. forward transitions in T . Morphisms of automata are just the morphisms of the underlying transition systems that preserve initial states. In e e e the sequel, notationse s ! and s 6! appear as shorthands for 9s0 2 S (s ! s0) 2 T and 8s0 2 S (s ! s0) 62 T .

0 0 ( ) 0

2.1 Regions in transition systems

RR n 3025

6

E. Badouel & Ph. Darondeau

We reserve the appellation of net systems to initialized nets N = (P; E; W; M ), with underlying net UN = (P; E; W ) and initial marking M . In order to give a uniform presentation for all types of nets, we depart from the traditional de nition of nets and propose now a general de nition encompassing Petri nets as a speci c type of nets (fully de ned afterwards). A marking is a map M : P ! LS from the set P of places to a set LS of local states (depending on the type of nets). The places in P and the events in E are the nodes of a complete bi-partite graph, whose edges are mapped to a set LE of local events (depending on the type of nets) by the weight matrix W : P E ! LE . The set of local states, the set of local events, and the partial action of the latter on the former, make up a type of nets. De nition 2.1 (Type of nets) A type of nets is a (deterministic) transition system = (LS; LE; ), where LS and LE are respective sets of local states and local events, and LS LE LS de nes the partial action of local events on local states.

0 0

As graphs, nets are of a static nature, but types (of nets) de ne their dynamics: the partial actions of events on markings may be inferred from the partial actions of local events on local states, using the weight matrix to control synchronized products of local events. The following de nition extends in this way the usual sequential ring rule. De nition 2.2 (Sequential marking graph) Given a net N = (P; E; W ), of type = (LS; LE; ), the (sequential) marking graph of N is the transition system (LS P ; E; T ) with set of transitions T de ned by : e (M ! M 0 ) 2 T i 8x 2 P (M (x) W x;e M 0 (x)) 2 ?! (1) Given a net system N = (P; E; W; M ), the (sequential) marking graph of N is the automaton N = (S; E; TS ; M ) where S is the inductive closure of fM g w.r.t. forward transitions in T , and TS = T \ (S E S ). A key example is the type of Petri nets, Petri = (IN; IN IN; Petri). Here, the local states are natural numbers while the local events are pairs of natural numbers, acting partially on the former according to the transition rule:

( ) 0 0 0

p;q (n ?! n0) 2

( )

Petri

, n p ^ n0 = (n ? p) + q

INRIA

On the synthesis of general Petri nets

7

If we set now W (x; e) = (F (x; e); F (e; x)), the reader recognizes in (1) the classical rule for the sequential ring of Petri nets, namely: M e>M 0 i 8x 2 P M (x) F (x; e) ^ M 0(x) = M (x) ? F (x; e) + F (e; x) pure A variant example is the type of pure Petri nets, Petri = (IN; Z ; Petri). In this Z pure weaker type of nets, the local events are relative numbers, acting partially on local states according to the transition rule: z pure n ! n0 2 Petri , n0 = n + z So, the local action of z is de ned at n if and only if n + z 0. The types of pure Petri nets and general Petri nets are in fact connected pure pure by morphisms I : Petri ! Petri and J : Petri ! Petri such that J I is the pure Z identity on Petri : J = (1 ; j ) where j : IN IN ! Z : j (p; q) = q ? p and I = (1 ; i) where i : Z ! IN IN : i(z) = (?z; 0) if z < 0 else i(z) = (0; z). Z A synthesis algorithm for pure Petri nets was proposed in BBD95b], based on the principle of regions as places. The primary goal of the paper is to extend this algorithm to (general) Petri nets. In order to get an intuitive understanding of regions for Petri nets, let us look back to their sequential ring rule (1). This rule means that for every place x, the pair of maps ( x; x) de ned by x(M ) = M (x) and x(e) = W (x; e) is a morphism of transition systems from the marking graph of the net to Petri . Let us now forget the internal structure of states in the marking graph, thus identi ed with any other isomorphic transition system (S; E; T ). If in addition we identify places x with their extensions ( x; x), we can rediscover the places of the original net (and also discover new places) as morphisms ( ; ) : (S; E; T ) ! Petri. This motivates the following de nition of regions for arbitrary types of nets. De nition 2.3 (Regions) Given a transition system T = (S; E; T ) and a type of nets = (LS; LE; ), the set R (T ) of -type regions in T is the set of morphisms from T to . By abuse of notations, we extend the above de nition to automata by setting R (A) = R (UA). In the sequel, the subscript is left implicit when it is equal pure to Petri, or abbreviated to pure when it is equal to Petri. So, pure regions and Petri regions are connected by maps IA : Rpure (A) ! R(A) : IA( ; ) = I ( ; ) and JA : R(A) ! Rpure (A) : JA ( ; ) = J ( ; ) such that JA IA is the identity.

I N I N

RR n 3025

8

E. Badouel & Ph. Darondeau

We saw above that regions may serve to reverse the production of marking graphs. The reversing process may also be applied to arbitrary transition systems, leading to the following de nitions. De nition 2.4 (Dual of a transition system) Given a transition system T = (S; E; T ) and a type of nets , the dual of T is the net T = (R (T ); E; W ) with weights de ned by W (( ; ); e) = (e). For any subset R of R (T ), let TR denote the subnet of T with restricted set of places R. De nition 2.5 (Dual of an automaton) Given an automaton A with initial state s and a type of nets , the dual of A is the net system A composed of the underlying net (UA) and of the initial marking M de ned by M ( ; ) = (s ) for every ( ; ) 2 R (A). For any subset R of R (A), let AR denote the subnet system of A with restricted set of places R. We will show that the two () operators mapping the automaton A to the net system A and the net system N to its marking graph N form a Galois connection A N , N A . One expects in particular A Nx , Nx A for every region x = ( x; x) 2 R (A) where Nx is the atomic subnet system of A with the sole place x (i.e. Nx = Afxg) and Nx is its marking graph. This particular case will help us to nd out the appropriate order relation on automata. Since Nx is a subnet sytem of A , both Nx A and A Nx are expected; by de nition of regions, if E is the set of events of A then ( x; 1E) is an event preserving morphism from A to Nx . Moreover, if there exists an event preserving morphism ( ; 1E) : A ! A between two automata with set of events E , this morphism is necessarily unique, owing to the strong properties of determinism and accessibility we have assumed from all automata. Therefore, if there exists morphisms ( ; 1E ) : A ! A and ( ; 1E) : A ! A , then A and A are identical up to the identity of states (A =E A ), and if we let Aut(E ) be the set of (deterministic and accessible) automata with xed set of events E , quotiented by =E , then A A if 9 : ( ; 1E ) : A ! A de nes a partial order on Aut(E ). This partial order is a complete lattice, with greatest lower bounds computed as synchronized products. We remind

0 0 0 0 1 2 1 1 2 2 2 1 1 2 1 2 1 2 1 2

2.2 Galois connection

INRIA

On the synthesis of general Petri nets

9

the reader that the synchronized product Vi2I Ai of a family of automata Ai = (Si ; E; Ti; s ;i) indexed by i 2 I is the automaton (S; E; T; s ) with components as follows: s = (s ;i)i2I , S is the inductive closure of the set fs g w.r.t. the synchronized transition rule

0 0 0 0 0

e (si )i2I ! (s0i )i2I

i

e 8i 2 I (si ! s0i ) 2 Ti

and T is the set of occurrences of this rule at states (si)i2I 2 S. So every automaton in Aut(E ) is an idempotent of the binary synchronized product ^, and the order could as well have been de ned as

A

0

1

A if A =E A ^ A

2 1 1

2

By de nition of marking graphs, the automaton N dual to a net system N = (P; E; W; M ) is actually the synchronized product Vx2P Nx of the marking graphs of its atomic subnet systems. Our starting point for choosing the order relation on Aut(E ) was to set A Nx for every region x 2 R (A). In fact, any atomic net system N = (fxg; E; W; M ) such that A N is isomorphic to Nx for some corresponding region ( x; x) 2 R (A) (i.e. N and Nx are identical up to exchanging x and ( x; x)).

0

Lemma 2.6 The regions in R (A) are in bijective correspondence with the (isomorphism classes of) atomic net systems N such that A N .

Proof: Let A N , where N = (fxg; E; W; M0) is an atomic net system of type = (LS; LE; ). Let ls0 = M0(x), hence ls0 2 LS . By de nition of marking graphs, N = (S; E; T; ls0) is the automaton with the least sets of states and transitions, S ( LS ) and T ( S E S ), such that ls0 2 S and e (ls ?! ls0) 2 T whenever ls 2 S ^ (ls W (x;e) ls0) 2 . Let ( x; 1E ) : A ! N ?! be the unique morphism (of transition systems) from UA to U (N ) acting as the identity on events and mapping the initial state s0 of A to ls0. Now the maps : S ! LS : (ls) = ls and x : E ! LE : x(e) = W (x; e) de ne a morphism ( ; x) : U (N ) ! . By composing morphisms one obtains a region in R (A) : ( ; x) ( x; 1E ) = ( x; x) : UA ! . Let Nx be the marking graph of the atomic net system Nx derived from the region ( x; x). Since x(s0) =

RR n 3025

10

( ) 0

E. Badouel & Ph. Darondeau

e ls and seeing that ls W x;e ls0 in entails ls ! ls0 in Nx for ls 2 S and e 2 E , ?! Nx is isomorphic to N .

Concerning the order relation on net systems, the central assumption that Nx A for every region x of A leads to choose something akin to the substructure ordering: N sub N if N is N restricted on a subset of places. However replicated places may occur in a net system N = (P; E; W; M ), i.e. places which the initial marking M and the weight function W do not happen to distinguish from one another, and we don't care about their degree of multiplicity nor about their identities. Let morphisms of net systems with xed set of events be de ned as follows: a morphism from N = (P ; E; W ; M ; ) to N = (P ; E; W ; M ; ) is a map : P ! P such that M ; (x) = M ; (x) and W (x; e) = W (x; e) for all x 2 P and e 2 E . Two net systems connected by morphisms in both directions are henceforth declared equivalent. Let Nets(E ) denote the set of equivalence classes of net systems with xed set of events E (replication free nets are the canonical representatives). One can equip Nets(E ) with a partial order relation by setting: N N if 9 : N ! N This partial order is a complete lattice, with least upper bounds Wi2I Ni of families of net systems computed by amalgamation of sets of places. Told in another way, if we identify a place x in a net system N = (P;W W; M ) with the E; pair (M (x); x) such that x(e) = W (x; e) for e 2 E then i2I (Pi; E; Wi; M ;i) for = (Si2I Pi; E; W; M ) where W (x; e) = Wi(x; e) and M (x) = M ;i(x)W x 2 Pi. A net system N with set of places P is now the least upper bound x2P Nx of its atomic subnet systems Nx. In the particular case where N = A is dual to the automaton A, its set of places P is the set of regions R (A), where is the type of N , and we get the following. Observation 2.7 Let P R R (A) then AP = Wx2P Afxg and AP AR. We are ready to establish the expected Galois connection between automata and net systems. Proposition 2.8 The two () operators, mapping respectively the automaton A to the dual net system A and the net system N to its marking graph N ,

1 2 1 2 0 0 1 1 1 01 2 2 2 02 1 2 01 02 1 2 1 1 2 1 2 0 0 0 0 0 0

INRIA

On the synthesis of general Petri nets

11

constitute a Galois connection between the ordered sets Nets(E ) and Aut(E ): A N , N A for A 2 Aut(E ) and N 2 Nets(E ). Proof: By Lem. 2.6, A N , N A if N is an atomic net system. Now for a net system N = Wx2P Nx, where Nx is the atomic subnet system of N with the unique place x, N = Vx2P Nx by de nition of marking graphs. Thus A N if and only if A Nx for all x 2 P if and only if Nx A for all x 2 P (because Nx is atomic) if and only if N A .

The relations A A ) A A (for A ; A 2 Aut(E )) and N N ) N N (for N ; N 2 Nets(E )) follow immediately from the Galois connection. It is nevertheless instructive to show directly that the () operators are decreasing. Let A A then every region ( ; ) of A , composed on the left with ( ; 1E ) : A ! A , yields a corresponding region ( ; ) of A ; the regions ( ; ) and ( ; ), taken as places of the respective net systems A and A , are identical since their values are identical in the initial markings M ; and M ; ( maps the initial state of A to the initial state of A ); hence A A . Let N N then we can assume P P without loss of generality, where P and P are the respective sets of places of N and N ; every atomic subnet system Nx of N is therefore a subnet V system of NV letting Ax = Nx ; (the marking graph of Nx), one obtains N = x2P Ax x2P Ax = N . Another general property of Galois connections is to produce closure operators by conjugated composition of the dual operators. Recall that an operator on (X; ), mapping x to x, is a closure operator if it is increasing (x x ) x x ), extensive (x x), and idempotent (x = x). The double dual operators () acting respectively on the ordered sets (Aut(E ); ) and (Nets(E ); ) are therefore closure operators. An automaton A equal to its closure A is said to be separated with respect to the xed type of nets , while a net system N equal to its closure N is said to be saturated. Owing to the Galois connection, the complete lattices of separated automata and saturated net systems are isomorphic.

1 2 2 1 1 2 1 2 2 1 1 2 1 2 2 2 2 1 2 2 2 1 2 2 2 2 2 1 01 02 1 2 2 1 1 2 1 2 1 2 1 2 1 2 1

1 2

2

1

2

1

2

In the end of the section, we state a criterion for the recognition of separated automata, at the basis of the synthesis algorithm proposed afterwards.

RR n 3025

2.3 Representation result

12

E. Badouel & Ph. Darondeau

By de nition, an automaton separated with respect to type is isomorphic to the synchronized product of marking graphs Nx of atomic net systems Nx = Afxg derived from -regions x of A (in formulas: A = Vx2R A Nx ). Following DR96], we say that a subset of regions R R (A) is admissible if A = Vx2R Nx . So, A is separated if and only if R (A) is admissible, and of course every superset of an admissible set of regions is admissible. The marking graph N of a net system N is separated because N = N follows from the Galois connection. In fact, the extensions ( x; x) of places x of N form an admissible set of regions of N . The following criterion may be used to recognize admissible sets of regions, and consequently separated automata.

( )

Theorem 2.9 Given an automaton A = (S; E; T; sO) and a type of nets , a set of regions R R (A) is admissible if and only if the following separation properties are satis ed for all states s; s0 2 S and for every event e 2 E : (SSP) s = s0 ) 9( ; ) 2 R : (s) = (s0) 6 6

(read: ( ; ) solves the states separation problem at (s; s0)) (e) e (ESSP) s 6! ) 9( ; ) 2 R : (s) 6?! w.r.t. (read: ( ; ) solves the event/state separation problem at (s; e)) When both properties are satis ed, A = (AR) , where AR is the subnet system of A with restricted set of places R (also called the net synthesized from R). Proof: Let Nx = AfxV for x 2 R, and let NR = AR . Seeing that A Nx for g every region x, A x2R Nx = NR. Accordingly, there exists a morphism of automata ( ; 1) : A ! NR. Moreover this morphism is unique. On the other hand, every region x = ( x; x) factors into ( ; x) ( x; 1) where acts as the identity on the local states in its domain, and ( x; 1) lifts to the unique event preserving morphism from A to Nx . As NR is the synchronized product of (Nx )x2R, must be the map that sends each state s of A to the associated vector (s) = ( x(s))x=( x ; x)2R (the x-component is computed by evaluating region x at state s). Since ( ; 1) is the unique morphism of this form from A to NR, and seeing that all automata are accessible and deterministic, the e assertion A = NR is now equivalent to (i) is an injective map, and (ii) s ! e in A whenever (s) ! in NR. Now SSP is just another form of assertione (i). e By de nition of the synchronized product, (s) ! in NR entails x(s) ! in

INRIA

On the synthesis of general Petri nets

13

Nx for all x 2 R, hence ESSP is just another form of assertion (ii).

3 Synthesis of general Petri nets (sequential ring)

Assuming the sequential ring rule, the synthesis problem for Petri nets consists in (i) deciding whether a nite automaton A given as input is isomorphic to the marking graph N of some net system N = (UN; M ), where UN is a Petri net red sequentially from the initial marking M , and if so, (ii) producing as output a net system N such that A = N and noproper subnet system of N satis es this property. On the grounds of Theo. 2.9, this amounts to (i) deciding whether all instances of the separation problems in A are solved by corresponding regions in R(A), and if so, (ii) synthesizing the desired net system N = AR from a minimal admissible subset of regions R, extracted from the set of solutions. In an automaton A = (S; E; T; s ), there are at most jS j ? jS j possible inputs for the states separation problem: SSPA (s; s0) : \construct from A and s 6= s0 a region ( ; ) s.t. (s) 6= (s0)" and at most jS j jE j instances of the event/state separation problem: e e ESSPA (s; e) : \construct from A and (s 6!) a region ( ; ) s.t. ( (s) 6?!)". Part (i) of the problem will therefore be solved in time polynomial (in jS j and jE j ) as soon as SSPA (s; s0) and ESSPA (s; e) are solved in polynomial time. Part (ii) consists in extracting from a set of regions with size polynomial in jS j and jE j a minimal admissible subset and this certainly can be done in polynomial time. So, a polynomial algorithm for the synthesis of Petri nets will follow if we succeed to construct procedures that solve in polynomial time SSPA (s; s0) and ESSPA (s; e) with respect to the type Petri. This is the program of the section. The rst stage of the program is to study the algebraic properties of R(A), the set of Petri regions of A. The second stage of the program is to elaborate decision procedures based on these properties.

0 0 0 2 ( )

3.1 The synthesis problem

RR n 3025

14

E. Badouel & Ph. Darondeau

From now on, A = (S; E; T; se ) is a xed automaton, nite and reduced i.e. such that 8e 2 E 9s 2 S s !. Of major importance for algorithms are the algebraic properties of R(A), inherited from Rpure (A) through the embedding / projection pair (IA; JA ) de ned in section 2. Recall that IA : Rpure (A) ! R(A) maps a pure region ( ; ) 2 Rpure (A) to the region ( ; ( ? ; )) 2 R(A) such that for all e 2 E : (e) = (e) ? ?(e) and (e) 0 ) (e) = 0 and (e) 0 ) ? (e) = 0, while JA : R(A) ! Rpure (A) maps a region ( ; ( ? ; )) 2 R(A) to the pure region ( ; ) 2 Rpure (A) such that for all e 2 E : (e) = (e) ? ?(e) (where : S ! IN, : E ! Z , ? : E ! IN, and : E ! IN). Let Z us focus on the second projections of pure regions, henceforth called abstract regions. Let Rabs (A) denote the set of abstract regions of A, i.e. Rabs (A) = f : E ! Z j 9 : S ! IN ( ; ) 2 Rpure (A)g. We are primarily interested Z in the algebraic properties of Rabs (A), with elements 2 Rabs(A) seen as vectors in the Z -module (E ! Z ) and represented in the sequel as formal Z Z sums = i ei where i = (ei). Before investigating these properties, let us establish a few notations. In the xed transition system UA = (S; E; T ), let @ ; @ : T ! S and ` : T ! E denote the respective source, target, and labelling functions given by @ (t) = s, e @ (t) = s0, and `(t) = e for t = s ! s0 2 T . A 0-chain of UA is a vector in the Z -module C (UA) = (S ! Z ). A 1-chain of UA is a vector in the Z -module Z Z Z C (UA) = (T ! Z ). The boundaries of the 1-chains are the 0-chains computed Z by the operator @ : C (UA) ! C (UA) : @ ( cj tj ) = cj (@ (tj ) ? @ (tj )). A cycle is a 1-chain with the null boundary. The cycles of UA form a submodule of the Z -module (T ! Z ), let Z (UA)= fc 2 C (UA)j @ (c) = 0g. The Parikh Z Z images of cycles form in turn a submodule of the Z -module (E ! Z ), where Z Z the Parikh image of a 1-chain c = cj tj is the vector (c) = cj `(tj ). Given vectors = i xi and = i xi in a nite dimensional Z -module (X ! Z ), Z Z we let denote their scalar product i i.

0 + + + + + + 0 1 0 1 0 1 1 0 1 0 1

3.2 The structure of Petri regions

Lemma 3.1 ( ; ) 2 Rpure (A) i

@ (c) =

(c) for all c 2 C (UA).

1

Proof: By linearity, the condition 8c 2 C1(UA) @ (c) = (c) is equivalent to the condition 8t 2 T @ (t) = (t) where t is identi ed with the chain

INRIA

On the synthesis of general Petri nets

1 0

15

(1:t). Now the equation @ (t) = (t) is valid if and only if (@ (t)) - (@ (t)) `t pure = (`(t)), if and only if (@ (t)) ?! (@ (t)) w.r.t. the type Petri, if and only if ( ; ) 2 Rpure(A) by de nition of regions.

0 ( ( )) 1

rized by the condition: (s0) + ( (c)) 0 for every 1-chain c 2 C1(UA) such that @ (c) = (s ? s0) for some s 2 S . Proof: From Lem. 3.1, the condition on must hold and whenever it does, the scalar product ( (c)) takes an identical value for all 1-chains c with an identical boundary. From the de nition of regions, the condition on (s0) pure must hold because the local states speci ed for the type of nets Petri are the non negative integers. Now the two conditions taken together guarantee that one does always complete the data ( (s0); ) to a pure region by selecting for each state s 2 S a corresponding 1-chain cs such that @ (cs) = (s ? s0 ) and then setting (s) = (s0) + (cs).

Proposition 3.2 : E ! Z 2 Rabs(A) i Z (c) = 0 for every cycle c 2 Z (UA); the regions ( ; ) 2 Rpure(A) which project on are then characte-

Since A is a reduced automaton, determines for the pure regions ( ; ) 2 Rpure (A), thus determines ( ? ? ) for the Petri regions ( ; ( ? ; )) 2 R(A). Therefore, as observed in DS96], the latter are fully determined from maps and ?. Now in turn may be computed from (s ) and = ( ? ?), hence a Petri region is still fully determined from (s ) and the maps ? and ( ? ? ). The following corollary to Prop. 3.2 states the recipe for manufacturing regions presented in this form from abstract regions 2 Rabs(A).

+ + 0 + 0 +

Corollary 3.3 ( ; ( ?; )) 2 R(A) if and only if (i) = ( ? ? ) 2 Rabs(A) , and (ii) (s ) + (c) ? (e) for every chain c 2 C (UA) and e 2 E such

+ +

that 9s 2 S @ (c) = (s ? s0 ) ^

0

e s !.

1

In order to complete the machinery, it remains to produce a linear basis for the Z -module of abstract regions Rabs(A). We recall hereafter classical results Z from graph theory and linear algebra showing that a basis may be computed in time polynomial in jS j and jE j (since A is deterministic, jS j jE j is an upper bound for jT j). First, one produces a linear basis for the Z -module Z

RR n 3025

16

E. Badouel & Ph. Darondeau

of cycles Z (UA). According to Prop. 3.4, which specializes results found in e.g. Lef75] or GM85], this amounts to construct a spanning tree for A, i.e. a sub-automaton = (S; E; U; s ) such that: (i) U T (by de nition of a sub-automaton), (ii) u + + un 6= 0 for ui 2 U and n 6= 0 (n = 0 indicates the empty chain), and (iii) there exists for every state s 2 S a unique chain cs = u + + un such that ui 2 U and @ (cs) = s ? s . A spanning tree can be computed in polynomial time.

0 1 1 0

Proposition 3.4 Let = (S; E; U; s ) be a spanning tree for A, with set of arcs U = fui j i 2 I g, then each transition t 2 T n U determines a unique cycle ct = t + zi ui such that zi 2 f?1; 0; 1g for i 2 I . The set fct j t 2 T n U g is

0

a basis of the Z Z-module Z (UA).

1 1

The dimension (A) of the module Z (UA) is therefore equal to jT j ? jU j. Now let E = fe ; ; eng, T = ft ; ; tmg, and let fc ; ; c A g be an arbitrary basis for Z (UA). From Prop. 3.2, Rabs(A) is the kernel of the linear transformation MA : Z n ! Z A de ned by the (A) n matrix MA with integral coe cients Z Z

1 ( ) ( )

MA (i; j ) = fci(tk )j 1 k m ^ `(tk ) = ej g

Let k be the dimension of Ker(MA). The algorithm of von zur Gathen and Sieveking (see Sch86]), given MA as input, produces in time polynomial in (A) and n (or jS j and jE j) a basis f ; : : :; kg for Ker(MA) = Rabs(A). We have in hand all the elements needed for solving problems SSPA (s; s0) and ESSPA (s; e) relatively to the type of Petri nets. The data needed are the spanning tree , or more exactly the application c : that maps each state s 2 S to the unique path cs from s to s in , and the basis of abstract regions f ; : : :; kg.

1 () 0 1

3.3 Solving the states separation problem

+ +

Given s; s0 2 S such that s 6= s0, let us consider the separation problem SSPA (s; s0). Seeing that JA ( ; ( ?; )) = ( ; ? ?) according to the correspondence (IA; JA ) between Rpure (A) and R(A), SSPA (s; s0) has a solution in R(A) i it has a solution in Rpure (A). Now from Lem. 3.1 and Prop. 3.2, 6 SSPA (s; s0) has a solution in Rpure(A) i (cs ? cs0 ) = 0 for some abstract

INRIA

On the synthesis of general Petri nets

17

region 2 Rabs(A) i i (cs ? cs0 ) 6= 0 for some i 2 f1; ; kg, and the pure region ( i ; i) determined from i by setting i(s ) = ?minf i (cs) j s 2 S g is then a solution. The problem SSPA (s; s0) is thus solved in R(A) by the Petri region IA ( i ; i ). Therefore, deciding whether SSPA (s; s0) has a solution and producing it takes time polynomial in jS j and jE j.

0

3.4 Solving the event / state separation problem

Given s0 2 S and e0 2 E such that (s0 6!), let us consider now the separation problem ESSPA(s0; e0). From Cor. 3.3, ESSPA (s0; e0) has a solution in R(A) i there exists (s ) 2 IN, 2 Rabs (A), and ? : E ! IN such that: 1. 8e (e) + ? (e) 0 2. 8s (s ) + (cs) 0 e 3. 8s 8e s ! ) (s ) + (cs) ? (e) 4. (s ) + (cs0 ) < ?(e0) e It eis worth noting that (2) entails both s ! ) (s ) + (cs) + (e) 0 and s ! ) (s ) + (cs) maxf0; ? (e)g, hence (1) and (3) hold automatically for e 6= e0 if one sets ?(e) = maxf0; ? (e)g. What remains after simpli cation is a system of linear inequations in k + 2 variables x; y; zi (i = 1 k) where x = (s ) 2 IN, y = ? (e0) 2 IN, and = zi i (recall that f ; : : :; kg is a basis for Rabs(A)). In order to obtain a more compact presentation, let wis = i (cs) for i 2 f1; ; kg and s 2 S . The system ? to be solved is assembled from the following inequations: 1. y + zi i (e0) 0 2. x + zi wis 0 (one inequation for each s 2 S )

0 0 0 0 0 0 0 1

e0

e 3. x ? y + zi wis 0 (one inequation for each s 2 S such that s !) 4. x ? y + zi wis0 < 0

0

RR n 3025

18

E. Badouel & Ph. Darondeau

This system augmented by the constraints x 0 and y 0 is homogeneous, hence it has an integral solution i it has a rational solution. Deciding upon the feasability of ? in Q k and computing a rational solution when it exists l may be achieved in time polynomial in jS j and k (and thus in jS j and jE j) following the method of Khachiyan (see for instance Sch86] p.170). Thus ? is solved up to a multiplicative factor or shown unfeasible in polynomial time. The above reasoning applies to any homogeneous system of linear inequations and it does not take advantage of the particular form of ?. The speci c analysis presented hereafter allows to optimize the0 solution. Since A is a ree duced automaton, the set fs ; ; shg = fs 2 S j s !g is not empty. Therefore, the system assembled from the linear inequations zi (wis0 ? wis) < 0 derived from (3) and (4) is not trivial. Let wij = wis0 ? wis for i 2 f1; ; kg and j 2 f1; ; hg. Now may be rewritten as W T Z (?1)k , where Z 2 Z k is Z k = (?1; ; ?1). A system of the vector of the unknown zi = Z (i) and (?1) this form has an integral solution i it has a rational solution, hence it may be solved or shown unfeasible in time polynomial in h and k following the method of Khachiyan. We claim that any integral solution of , let Z , extends to a solution of ?, let (x; y; Z ) where x; y 2 IN. The adequate values for x and y may be e0 chosen as follows. Let = minf zi wis j s 2 S g, = minf zi wis j s !g, and = zi i(e0). Observe0 the relations 0 (as s = s ) wis = 0), , e s00 ) z (w + (e0)) = z w 00 ). Now let x = ? and + (as s ! i is i i is and y = ? . The satisfaction of the inequations (1), (2), and (4) follows e0 immediately. Regarding (3), observe that s ! ) zi (wis0 ? wis) < 0 since Z is a solution of , hence zi wis0 < as was to show. The problem ESSPA(s0; e0) is now solved in R(A) by the Petri region ( ; ( ; )) de ned by (s ) = x, ( (e); (e)) = i ( zi i(e)) for e 6= e0, and ( (e0); (e0)) = (y; y + zi i(e0)). Observe nally that ( ; ( ; )) = IA JA ( ; ( ; )) i + , in which case ESSPA (s0; e0) is also solved by a pure region. The following theorem summarizes the section. Theorem 3.5 The synthesis problem for Petri net systems with the sequential ring rule is polynomial in the numbers of states and events of the transition systems taken as inputs.

+2 1 j 0 1 2 0 1 2 1 2 1 2 1 2

INRIA

On the synthesis of general Petri nets

19

4 Galois connection between step automata and net systems

We leave now the classical frame of (sequential) transition systems for the more expressive frame of step transition systems, de ned by Mukund so as to account fully for the independence of events in general Petri nets. A co-re ection was established in Mu92] between a full subcategory of step transition systems and the category of Petri nets, according to which the co-re ective image of a net is the marking graph of that net equipped with the step ring rule. Recalling this rule is a prerequisite for motivating the de nition of step transition systems.

from (P E ) (E P ) to the positive integers, the concurrent marking graph of N is the transition system (IN P ; IN E ; T ) with set of transitions T (IN P IN E IN P ) de ned as follows: (M ! M 0 ) 2 T i 8x 2 P M (x) e2E (e) F (x; e) ^ M 0 (x) = M (x) + e2E (e) (F (e; x) ? F (x; e)). When these conditions are satis ed we say that the step has concession in state M (written also M >).

4.1 Step transition systems

De nition 4.1 Given a Petri net N = (P; E; F ), where F is a partial map

It follows from Def. 4.1 that whenever = + in E ! IN and M ! M 0 in T , there exists an intermediate marking M 00 such that M ! M 00 and M 00 ! M 0. Let us inspect the relationship between the sequential and concurrent marking graphs of a net. On the one hand, the sequential marking graph is the induced restriction of the concurrent marking graph on the subset of atomic steps, i.e. steps such that e2E (e) = 1. On the other hand, the concurrent marking graph cannot in general be reconstructed up to isomorphism from an arbitrary copy of the sequential marking graph, even though additional data are provided by a binary relation of independence on events, depending on markings, such that e kM e0 i M fe; e0g > . An example borrowed from HKT96] is shown in Fig. 4.1. This example motivates the following de nition.

A step transition system (S; M; T ) over an abelian monoid M consists of a set of states S and a deterministic transition relation T S M S , with

RR n 3025

De nition 4.2 (Step transition system over an abelian monoid)

20

c a

E. Badouel & Ph. Darondeau

a b c c a

a b c

a b

c

b b

Figure 1: Three nets with an identical sequential marking graph but with di erent concurrent marking graphs

0 distinguished empty steps: s ! s0 i s = s0. A step automaton A is an initialized step transition system (S; M; T; s0 ) with initial state s0 2 S , such that every state s 2 S is reachable from s0 in U A = (S; M; T ). The step automaton A is nite if the set of transitions T is nite. When M = <E >, the free abelian monoid freely generated from set E , the step automaton A is said to be reduced if its skeleton (S; E; T \ (S E S ); s0 ) is a reduced automaton. The de nition of step transition systems extends Mukund's original de nition, which was restricted to free abelian monoids M = <E > = (E ! IN ). The extension was not indispensable for the progress of this work, but it allows to accomodate the idea of regions as morphisms to step transition systems which + do not present the intermediate state property: s ! s0 6) 9s00 2 S s ! s00 ^ s00 ! s0. This aspect will be investigated in another study. The nal goal of the present paper is to adapt the synthesis algorithm for Petri nets de ned in section 3 so as to t now step transition systems taken as inputs. This goal will be achieved in section 5. In the meantime, we proceed to adapt regions to step transition systems and to establish a Galois connection between step automata and Petri net systems.

The de nition of regions in step transition systems is parametric on enriched types of nets de ned as follows. De nition 4.3 (Enriched type of nets) An enriched type of nets is a (deterministic) step transition system = (LS; LE; ), where LE is a commutative monoid (LE; +; (0; 0)).

INRIA

4.2 Regions in step transition systems

On the synthesis of general Petri nets

21

Each type of nets determines a speci c concurrent ring rule and hence a speci c construction of concurrent marking graphs for nets.

De nition 4.4 (Concurrent marking graph) Given a net N = (P; E; W )

with (enriched) type = (LS; LE; ), the concurrent marking graph of N is the step transition system ( LS P ; <E >; T ) with set of transitions T de ned by :

(x; (M ! M 0 ) 2 T i 8x 2 P (M (x) W?! ) M 0 (x)) 2 (2) where W (x; e1 + + en ) = W (x; e1) + + W (x; en). Given a net system N = (P; E; W; M0), the concurrent marking graph of N is the step automaton N = (S; <E >; TS ; M0) where S is the inductive closure of the singleton set fM0g w.r.t. forward transitions in T , and TS = T \ (S <E > S ).

Regions may now be introduced, based on the following de nition of morphisms of step transition systems.

De nition 4.5 A morphism of step transition systems from T=(S; M; T ) to

T'=(S 0 ; M 0 ; T 0) is a pair ( ; ), made of a map : S ! S 0 and a monoid mor( phism : M ! M 0, such that s ! s0 ) (s) !) (s0 ). The morphisms of step automata from A to A0 are the morphisms from U A to U A0 that preserve the initial state.

De nition 4.6 (Regions in step transition systems) Given a step transition system T = (S; M; T ) and an enriched type of nets = (LS; LE; ), the set R (T ) of -type (extended) regions in T is the set of morphisms of step transition systems from T to . The set of -type (extended) regions of a step automaton A is the set R (A) = R (U A).

For the sake of illustration, let us specialize the above de nitions to Petri nets, and thereby pave the way for solving their extended synthesis problem (in section 5). The enriched type of Petri nets is just the type Petri = (IN; IN IN; Petri) enriched with the operation of componentwise addition in IN IN : (i; j ) + (k; l) = (i + k; j + l). This is coherent with Def. 4.6 since (IN IN; +; (0; 0)) is the free abelian monoid generated from (0; 1) and (1; 0). i;j Now seeing that n ?! in Petri i n i, Def. 4.1 may be restored from

( )

RR n 3025

22

E. Badouel & Ph. Darondeau

Def. 4.4 by specializing to Petri . Mukund's de nition of regions may be restored similarly from Def. 4.6. Returning to arbitrary types of nets, observe from equation 2 that the extension ( x; x) of a place x in the concurrent marking graph of a net N is a region, de ned by x(M ) = M (x) and x( ) = W (x; ) = e2E (e) W (x; e). The technical development about basic transition systems conducted through sections 2.2 and 2.3 may be reproduced nearly intact in the enriched setting of step transition systems over a free abelian monoid. We state here the de nitions and results needed for next section, and avoid a remake of the proofs by just indicating the adaptation.

4.3 Galois connection and representation result

De nition 4.7 (Dual of a step transition system) Given a step transition system over a free abelian monoid T = (S; <E >; T ), and an enriched type of nets , the dual of T is the net T = (R (T ); E; W ) with weights de ned by W (( ; ); e) = (e). For any subset R of R (T ), TR is the subnet of T with restricted set of places R. De nition 4.8 (Dual of a step automaton) Given a step automaton A over a free abelian monoid, with initial state s0 , and a type of nets , the dual of A is the net system A composed of the underlying net (U A) and of the initial marking M0 de ned by M0 ( ; ) = (s0) for every ( ; ) 2 R (A). For any subset R of R (A), AR is the subnet system of A with restricted set of places R.

Let SAut(E ) denote the set of isomorphism classes of reduced step automata over <E >. Seeing that SAut(E ) is a subset of Aut(<E >), it inherits the induced restriction of the order relation A A if 9 : ( ; 1<E>) : A ! A . This order relation on SAut(E ) may be equivalently de ned as : A A if there exists an event preserving morphism of step transition systems ( ; 1<E >) : A ! A . Moreover the synchronized product of step automata computed in Aut(<E >) is a step automaton, and it is in fact their greatest lower bound in SAut(E ). This justi es the following transposition of Prop. 2.8.

1 2 1 2 1 2 1 2

INRIA

On the synthesis of general Petri nets

23

Proposition 4.9 The two () operators, mapping respectively a step automaton A over the free abelian monoid <E > to the dual net system A and a net

system N with set of events E to its concurrent marking graph N , constitute a Galois connection between the ordered sets Nets(E ) and SAut(E ): A N , N A for A 2 SAut(E ) and N 2 Nets(E ).

( )

A step automaton A over <E > is said to be separated w.r.t. an enriched type of nets if it is isomorphic to its closure A = Vx2R A Nx where Nx = Afxg is the atomic net system derived from the extended region x. A set of extended regions R R (A) is said to be admissible if A = Vx2R Nx . The concurrent marking graph of a net system is always separated, and the extensions of the places of N in N form always an admissible set of extended regions (in view of equation 2). Next section is based upon the following counterpart to Theo. 2.9.

(read: ( ; ) solves the states separation problem at (s; s0)) ( ) (ESSP) s 6! ) 9( ; ) 2 R : (s) 6?! w.r.t. (read: ( ; ) solves the event/state separation problem at (s; )) When both properties are satis ed, A = (AR) , where AR is the subnet system of A with restricted set of places R (also called the net synthesized from R).

Theorem 4.10 Given a step automaton over a free abelian monoid, let A = (S; <E >; T; sO ), and an enriched type of nets , a subset of extended regions R R (A) is admissible if and only if the following separation properties are satis ed for all states s; s0 2 S and for every multiset 2 <E >: (SSP) s = s0 ) 9( ; ) 2 R : (s) = (s0) 6 6

5 Synthesis of general Petri nets (concurrent ring)

5.1 The extended synthesis problem

0

Assuming the concurrent ring rule, the extended synthesis problem for Petri nets consists in : (i) deciding whether a nite step automaton A over <E >, given as input, is isomorphic to the concurrent marking graph N of some net system N = (UN; M ), and if so : (ii) producing as output a net system N

RR n 3025

24

E. Badouel & Ph. Darondeau

such that A = N and no proper subnet system of N satis es this property. Henceforth, A = (S; <E >; T; s ) is a nite and reduced step automaton. Moreover, seeing that the intermediate state property is always satis ed in the concurrent marking graph of a Petri net, we assume this property from A. Thus, s ! s0 2 T ) 9s00 2 S s ! s00 2 T ^ s00 ! s0 2 T . The import is that we may further assume a compact representation for A, given by its skeleton and the set of the maximal steps at each state s 2 S . This makes sense since the set of steps of A is bounded (from the assumption that A is nite). In the sequel, A denotes the skeleton of A, and for each state s 2 S , Max(s) denotes the set of the maximal steps with concession at s.

0 +

Let us inspect the relationship between R(A) and R(A), the respective sets of Petri regions of A and extended Petri regions of A. A monoid morphism : <E > ! IN IN is totally de ned from its restriction on generators, let E = ( E? ; E ). The map which sends ( ; ) to ( ; E ) is thus an injection from R(A) into R(A). A Petri region ( ; E ) is in the image of this map i (s) e2E (e) E ? (e) for every state s 2 S and for every multiset 2 Max(s). When these conditions are met, the region ( ; E ) may be identi ed with the extended region ( ; ) where is the extension of E to multisets in <E >. One may therefore state without further proof the following lemma, extending Cor. 3.3.

+

5.2 The structure of extended Petri regions

Lemma 5.1 Let be a map from S to IN and : <E > ! IN

be a morphism of monoids, restricting on generators to E = ( E? ; E+ ) and let 0 = E + ? E ? , then ( ; ) 2 R(A) if and only if (i) 0 2 Rabs (A), and (ii) (s0) + 0 (c) e2E (e) E ? (e) for every chain c 2 C1 (UA) and for every step 2 <E > such that 9s 2 S @ (c) = (s ? s0 ) ^ s !.

I N

5.3 Solving the states separation problem

1

0 Let us recall from section 3 that computing a basis f 0 ; : : :; kg for the Z Z module of abstract regions Rabs(A) takes time polynomial in jS j and jE j. Now

INRIA

On the synthesis of general Petri nets

25

the states separation problem SSPA (s; s0) may be solved in R(A) i the states separation problem SSPA (s; s0) is solved in R(A) by a pure region of the form ( j ; i j0 ), where 1 j k. Seeing that a pure region of A extends always to a region of A, the separation problem SSPA (s; s0) is then also solved by ( j ; i j0 ). Therefore, solving all the instances of the states separation problem in A takes time polynomial in jS j and jE j. According to Lem. 5.1, an instance ESSPA (s0; 0) of the event / state separation problem in A has a solution in R(A) if and only if there exist (s ) 2 IN, 0 2 Rabs (A), and E ? : E ! IN such that the following hold, letting cs be the unique path from s to s in the spanning tree for A de ned in section 3 : 1. 8e 0(e) + E?(e) 0 2. 8s 8 2 Max(s) (s ) + 0 (cs) e2E (e) E?(e) 3. (s ) + 0 (cs0 ) < ( e2E 0(e) E?(e)) The expected solution is then the extended region ( ; ) such that (s) = (s ) + 0 (cs) and : <E > ! IN IN restricts on E to ( E? ; 0 + E? ). In order to study the existence of solutions to the above constraints, let us introduce variables x = (s ), yi = E?(ei) with E = fe ; ; eng, and zj with 0 = z 0 + + zk 0 . Thus x 2 IN , yi 2 IN for 1 i n, and zj 2 Z for Z k 1 j k. Let us de ne also integer constants wjs = j0 (cs) for 1 j k and s 2 S . Assuming w.l.o.g. that e0 = e and letting Max denote the size of the largest set of maximal steps Max(s) for s 2 S , then the above constraints may be rewritten into a system of at most ( jE j + Max jS j + 1 ) linear inequations in the unknowns x, yi and zj , as follows : 1. yi + j zj j0 (ei) 0 (one inequation for each 1 i n) 2. x ? i (ei) yi + j zj wjs 0 (for each s 2 S and 2 Max(s)) 3. x ? i 0(ei) yi + j zj wjs0 < 0 4. yi 0 (for each 1 i n)

0 0 0 0 0 0 1 1 1 1

5.4 Solving the event / state separation problem

RR n 3025

26

E. Badouel & Ph. Darondeau

5. x 0 The system is homogeneous, hence it has an integral solution i it has a rational solution. The method of Khachiyan may again be used to decide whether the system is feasible and to compute a solution in polynomial time. A region that solves the problem ESSPA (s; ) solves also all instances of the form ESSPA (s; ) for < therefore it is su cient to solve the instances corresponding to minimal failures. Thus if we let Min(s) stand for the set of minimal steps having no concession at s and Min the largest size of such set, the following theorem summarizes the section. Theorem 5.2 The synthesis problem for Petri net systems with the step ring rule, taking as inputs nite step transition systems is polynomial in their numbers of states and events, in the size of the largest set of minimal failures in one state, and in the size of the largest set of maximal steps enabled in one state. Notice that minimal failures cannot be determined from the maximal enabled steps as illustrated by the third Petri net of Fig. (1) for which Max(s ) = fa + c; b + cg and Min(s ) = f2a; a + b; 2bg and therefore Min(s) 6 f + ej 2 Max(s)g. Let us conclude by a comparison with Bad96]. Every step automaton may be transformed into an ordinary automaton by splitting its alphabet of events. More precisely the states of the split automaton are ethe pairs <s; > where is a step with concession at s and each transition s ! s0 gives e e? rise to the pair of transitions <s; > ! <s; + e> and <s; + e> ! <s0; > for every step = + e with concession at s. In Bad96] it is shown that the synthesis problem for Petri nets may be reduced to the synthesis of pure Petri nets by splitting events, and that one can derive from the algorithm of BBD95a] an algorithm for the synthesis of Petri nets from step automata taking time polynomial in the size of sets of higher-dimensional states. Now e if 2 Min(s) is a minimal failure, then <s; > 6! for any step and event e such that = + e, and the problem ESSPA (s; ) is equivalent to the event/state separation problem ESSP A (<s; >; e ) induced by the event e and the higher-dimensional state <s; >. Of course there is more instances of ESSP to be solved in the split automaton since can be decomposed as = +e in several ways. Nevertheless Min and the number of instances of the

0 0

+ +

+

Split(

+

INRIA

On the synthesis of general Petri nets

27

event/state separation problem in the split automaton are both exponential in the number of events. Actually if A is the step automaton whose skeleton A = (S; E; T; s ) is the 2n-dimensional hypercube, i.e. E = fa ; : : : ; a ng, e S = 2E with initial state s = ; and ! i = feg, and such that the concession of steps at states is given by s ! i s s! and

0 1 2 0

n _ j < k ) (a ) = 0 ^ (a ) = 1 ^ j j k + 1] j k k Pn C k = 2n ? 1. then jMin(s )j = Pn C k

0

+

s 6! ,

0 0

=1

k=1

2

n?k

k=1

n

References

Bad96] Badouel, E., Splitting of Actions, Higher-Dimensional Automata, and Net Synthesis. Inria Research Report 3013 (1996). BBD95a] Badouel, E., Bernardinello, L., and Darondeau, Ph., The Synthesis Problem for Elementary Net Systems is NP-complete. Inria Research Report 2558 (1995) -to appear in Theoretical Computer Science. BBD95b] Badouel, E., Bernardinello, L., and Darondeau, Ph., Polynomial Algorithms for the Synthesis of Bounded Nets. Proceedings of CAAP'95, Lecture Notes in Computer Science vol. 915 (1995) 647-679. BD95a] Badouel, E., and Darondeau, Ph., Trace Nets and Process Automata. Acta Informatica vol. 32 (1995) 647-679. BD95b] Badouel, E., and Darondeau, Ph., Dualities between Nets and Automata Induced by Schizophrenic Objects. Proceedings of 6th International Conference on Category Theory and Computer Science, Lecture Notes in Computer Science vol. 953 (1995) 24-43. BDPV96] Bernardinello, L., De Michelis, G., Petruni, K., and Vigna, S., On the Synchronic Structure of Transition Systems. In \Structures in Concurrency Theory", J. Desel ed., Springer-Verlag (1996) 11-31. Ber93] Bernardinello, L., Synthesis of Net Systems. Proceedings of Application and Theory of Petri Nets, Lecture Notes in Computer Science vol. 691 (1993) 89-105. CKLY95] Cortadella, J., Kishinevsky, M., Lavagno, L., and Yakovlev, A., Synthesizing Petri Nets from State-Based Models. Proceedings of ICCAD'95 (1995) 164-171.

RR n 3025

28

E. Badouel & Ph. Darondeau

DR96] Desel, J., and Reisig, W., The Synthesis Problem of Petri Nets. Acta Informatica vol. 33 (1996) 297-315. DS93] Droste, M., and Shortt, R.M., Petri Nets and Automata with Concurrency Relations - an Adjunction. In \Semantics of Programming Languages and Model Theory", M. Droste and Y. Gurevich eds (1993) 69-87. DS96] Droste, M., and Shortt, R.M., From Petri Nets to Automata with Concurrency. Draft communicated to the authors. ER90a] Ehrenfeucht, A., and Rozenberg, G., Partial (Set) 2-Structures; Part I: Basic Notions and the Representation Problem. Acta Informatica, vol. 27 (1990) 315-342. ER90b] Ehrenfeucht, A., and Rozenberg, G., Partial (Set) 2-Structures; Part II: State Spaces of Concurrent Systems. Acta Informatica, vol. 27 (1990) 343-368. GM85] Gondran, M., and Minoux, M., Graphes et algorithmes. Eyrolles, Paris (1985). Hi94] Hiraishi, K., Some Complexity Results on Transition Systems and Elementary Net Systems. Theoretical Computer Science, vol. 135 (1994) 361-376. HKT92] Hoogers, P.W., Kleijn, H.C.M., and Thiagarajan, P.S., A Trace Semantics for Petri Nets. Proceedings of ICALP'92, Lecture Notes in Computer Science vol. 623 (1992) 595-604. HKT96] Hoogers, P.W., Kleijn, H.C.M., and Thiagarajan, P.S., An Event Structure Semantics for General Petri Nets. Theoretical Computer Science, vol. 153 (1996) 129-170. Lef75] Lefschetz, S., Applications of Algebraic Topology. Applied Mathematical Science 16, Spinger-Verlag (1975). Mu92] Mukund, M., Petri Nets and Step Transition Systems. International Journal of Foundations of Computer Science vol. 3 no. 4 (1992) 443-478. NRT92] Nielsen, M., Rozenberg, G., and Thiagarajan, P.S., Elementary Transition Systems. Theoretical Computer Science, vol. 96 (1992) 3-33. NW94] Nielsen, M., and Winskel, G., Models for Concurrency. Handbook of Logic for Computer Science, vol. 3, Oxford University Press (1994) 100-200. Sch86] Schrijver, A., Theory of Linear and Integer Programming. John Wiley (1986).

INRIA

Unit? de recherche INRIA Lorraine, Technop? le de Nancy-Brabois, Campus scienti?que, e o ` 615 rue du Jardin Botanique, BP 101, 54600 VILLERS LES NANCY Unit? de recherche INRIA Rennes, Irisa, Campus universitaire de Beaulieu, 35042 RENNES Cedex e Unit? de recherche INRIA Rh? ne-Alpes, 655, avenue de l’Europe, 38330 MONTBONNOT ST MARTIN e o Unit? de recherche INRIA Rocquencourt, Domaine de Voluceau, Rocquencourt, BP 105, 78153 LE CHESNAY Cedex e Unit? de recherche INRIA Sophia-Antipolis, 2004 route des Lucioles, BP 93, 06902 SOPHIA-ANTIPOLIS Cedex e

? Editeur INRIA, Domaine de Voluceau, Rocquencourt, BP 105, 78153 LE CHESNAY Cedex (France)

http://www.inria.fr

ISSN 0249-6399

相关文章:

- ...Tool for the Synthesis and Mining of Petri Nets.pdf
- (Tool paper)Genet_a Tool for
*the**Synthesis*and Mining*of**Petri**Nets*_IT/...In Genet,*the*notion*of**general*region is used, were*the*corresponding ...

- Synthesis of General Petri Nets with Localities.unkown
*Synthesis**of**General**Petri**Nets*with Localities Maciej Koutny and Marta Pietkiewicz-Koutny School*of*Computing Science Newcastle University Newcastle upon Tyne...

- Synthesis of General Petri Nets with Localities.unkown
*Synthesis**of**General**Petri**Nets*with Localities. Newcastle upon Tyne:School*of*Computing Science, University*of*Newcastle upon Tyne,2010. Further information...

- On the Synthesis of General Petri Nets.unkown
*On**the**Synthesis**of**General**Petri**Nets*Eric Badouel, Philippe Darondeau To cite this version: Eric Badouel, Philippe Darondeau.*On**the**Synthesis**of*...

- Synthesis of Supervisors Enforcing General Linear Constraints....unkown
- 48, NO. 11, NOVEMBER 2003
*Synthesis**of*Supervisors Enforcing*General*Linear...*Petri**net*(PN) satisfies constraints*of**the*form L b (1) 2 2...

- Towards Synthesis of Petri Nets from General Partial Languages.unkown
- In this paper we investigate
*synthesis**of*place/transition*Petri**nets*from three different finite representations*of*infinite partial languages,*general*- izing...

- A tool for the synthesis and mining of Petri nets.unkown
- Genet A tool for
*the**synthesis*and mining*of**Petri**nets*Josep Carmona jcarmonalsi.upc.edu Software Department Universitat Politcnica de Catalunya 2 ...

- Synthesis of Asynchronous Hardware from Petri Nets.unkown
- This paper focuses
*on*some*of*recent developments and new opportunities for*Petri**nets*in designing asynchronous circuits such as*synthesis**of*asynchronous ...

- On the Analysis and Synthesis of Coloured Petri Nets*.unkown
- 2004 IEEE International Conference
*on*Systems, Man and Cybernetics*On**the*Analysis and*Synthesis**of*Coloured*Petri**Nets** Jean-Yves Morel and Marc Bourcerie...

- The unfolding of general Petri nets.unkown
*The*unfolding*of**general**Petri**nets*Jonathan Hayman Glynn Winskel Computer Laboratory, University*of*Cambridge, England Abstract*The*unfolding*of*(1-)safe ...

- The synthesis of Petri nets from path-automatic specifications.unkown
- Information and Computation 193 (2004) 117135 www.elsevier.com/locate/ic
*The**synthesis**of**Petri**nets*from path-automatic specifications E. Badouel and ...

- A Method for the Synthesis of Deadlock Prevention Controllers....unkown
- A Method for
*the**Synthesis**of*Deadlock Prevention...Controllers in Systems Modeled by*Petri**Nets*...*general*Operating Systems, Distributed Operating...

- Synthesis of Embedded Software Using Free-Choice Petri Nets.unkown
*Synthesis**of*Embedded Software Using Free-Choice*Petri**Nets*Marco Sgroiy, Luciano Lavagnoz, Yosinori Watanabez and Alberto Sangiovanni-Vincentelliy y ...

- Controller Synthesis of Time Petri Nets Using Stopwatch.unkown
- //dx.doi.org/10.1155/2013/970487 Research Article Controller
*Synthesis**of*Time*Petri**Nets*Using Stopwatch Parisa Heidari and Hanifa Boucheneb Laboratoire ...

- Synthesis of Petri nets from scenarios (pomsets).unkown
*Synthesis**of**Petri**nets*from scenarios (pomsets) Jrg Desel Robert Lorenz, Robin Bergenthum, Gabriel Juhás, Sebastian Mauser Given: Model*of*behavior ...

- Protocol Synthesis from Time Petri Net Based Service Speci....unkown
- Protocol
*Synthesis*from Time*Petri**Net*Based Service Speci cations Hirozumi ...1 Introduction In*general*, for a distributed system, two di erent levels ...

- ...Algorithms for Process Mining and Synthesis of Petri nets.unkown
- 1 Region-based Algorithms for Process Mining and
*Synthesis**of**Petri**nets*Josep Carmona, Jordi Cortadella, Mike Kishinevsky Abstract*The*theory*of*regions ...

- Synthesis and Analysis of Product-form Petri Nets.unkown
*Synthesis*and Analysis*of*Product-form*Petri**Nets*Serge Haddad, Jean Mairesse, Hoang-Thach Nguyen To cite this version: Serge Haddad, Jean Mairesse, ...

- ...Based Synthesis with Modular Encoding of Petri Nets into ....unkown
- CONTROL ENGINEERING VOLUME: 12 | NUMBER: 5 | 2014 | DECEMBER Transition Based
*Synthesis*with Modular Encoding*of**Petri**Nets*into FPGAs Arkadiusz BUKOWIEC,...

- Feedback control logic synthesis for non safe Petri nets.unkown
- Feedback control logic
*synthesis*for non safe*Petri**nets*Dideban A*. Alla H.** * Semnan University, IRAN (Tel: (+98)231-3354123; e-mail: adi...

更多相关标签:

- On the Semantics of PlaceTransition Petri Nets
- Operational analysis of timed Petri nets and applications to the computation of performance
- Research on the Railway Safety Critical System with Petri nets
- A Survey on the Supervision of Petri Nets
- General morphisms of Petri nets
- Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools
- Fourth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools
- (Tool paper)Genet_a Tool for the Synthesis and Mining of Petri Nets
- Making Work Flow On the Application of Petri nets to Business Process Management
- On the ω-language Expressive Power of Extended Petri Nets