Informática 32 (2008) 253-260 2 53 APC Semantics for Petri Nets Slavomír Simoñák, Stefan Hudák and Stefan Korecko Department of Computers and Informatics, Technical University of Kosice, Letná 9, 042 00 Kosice, Slovak Republic E-mail: slavomir.simonak@tuke.sk, stefan.hudak@tuke.sk, stefan.korecko@tuke.sk Keywords: Petri nets semantics, process algebra, algebra of process components Received: July 13, 2007 The paper deals with an algebraic semantics for Petri nets, based on a process algebra APC (Algebra of Process Components) by the authors. APC is tailored especially for describing processes in Petrinets. This is done by assigning special variables (called E-variables here) to everyplace of given Petrinet, expressing processes initiated in those places. Algebraic semantics is then given as a parallel composition of all the variables, whose corresponding places hold token(s) within the initial marking. Resulting algebraic specification preserves operational behavior of the original net-based specification. Povzetek: Clanek opisuje algebro semantike za Petri mreze. 1 Introduction An assertion widely accepted in formal methods community states, that there will never be invented a single formal method, that will cover all aspects of the system in acceptable way [12]. The latter is mainly because of the complexity of the system and vast variety of its features (aspects) to be covered for the system to be modeled and designed. As a consequence of that situation, many formal description techniques (FDTs) exist and are used nowadays. That reflects the fact that one feature f of the system is more readily expressed in FDT (say) F\, than it is the case for f in F2. To cope with that situation there have been attempts to integrate two or more formal methods. Main motivation for using FDT in design and analysis of computer-based systems lies in everyday growing dependence of human society on such the systems, particulary those applied in safety-critical domains (such as military weaponry, aircraft transport, medicine, etc.). The situation just described put strong requirements on new methods of the design, analysing and maintaining of such the systems. Time-critical issue of to be able to cope with malicious behaviour of the systems in limited time period, dictates strongly to deal with the problem in an automated way. The latter is impossible without using FDTs in proper combination and integration in the frame of computer-based design and analysis environments. Yet a formal way how to incorporate conditions to guarantee the safety of system designed is an example of another problem which underlines the importance of expolitation of FDTs. Guided by the considerations mentioned an approach has been applied at the home institution of the authors to create an environment for the design and analysis of discrete systems based on integration of three FDTs: Petri Nets (PN), process algebras and B-Method. That is why we have chosen the acronym mFDTE for it (multi FDT Environment). The choice of the FDTs has been motivated by their abilities to cover in some mutually complementary ways a chosen set of system's features. In this work we pay attention to two of the FDTs chosen: PN and process algebras. While on one side PN posses nice properties suited for system modelling (formal and graphical language) and analysis (invariants, reachability), on the other side they suffer from a lack of formally sound and effective methods of their de/composition. The latter can be considered as an essential drawback as far as the modular system design is concerned. Process algebras (CCS, CSP, ACP)[1] on the other hand support composion-ality, by their definition, so PN and process algebras can be considered to meet the complementarity property in the above sense. The paper is organized in the following way: Section 1 is introductory one, whole related works are briefly summarized in Section 2. In Section 3, basic notions and definitions for the class of Petri nets used are given. Algebra of Process Components is defined in Section 4. Notion of term is presented as a mean for describing processes, axioms are given and operational semantics is assigned to process expressions (terms). Section 5 concentrates on the algebraic semantics construction for a Petri net given. A special variable is assigned to every place of the Petri net. Construction rules are defined for assigning a term to the variable which represents all the computations which can be initiated at the corresponding place. An example provided in Section 6 demonstrates the approach introduced above. Section 7 concludes the paper and contains a summary of the results and concepts presented. 2 Related work An active research has been performed in the area of combining Petri nets and process algebras during last years 254 Informática 32 (2008) 253-260 S. Simonák et al. [4, 5, 2, 6, 10, 11]. It will be mentioned further [3], where authors propose an approach to algebraic semantics for Hierarchical P/T nets. PTNA (Place/Transition Net Algebra) is defined there, based on process algebra ACP and an algebraic semantics for P/T nets is given such that a P/T net and its term representation have the same operational behavior. The actions of the algebra presented correspond to the consumption and production of tokens by transitions. Results achieved are further extended to hierarchical P/T nets. In [11] relations among nets, terms and formulas are treated. Particularly relations are defined via properly defined semantics: net semantics of terms and process semantics of nets. The most influential works in the line we follow here are [5, 2]. In [5] relations between the process algebra, called there PBC (Petri Box Calculus) and a class of Place Transition Nets (safe P/T nets) are studied. Syntax and semantics of PBC terms are carefully selected to allow to define a transformation yielding P/T nets preserving structural operational semantics of the source terms. The transformation allows composition of P/T nets. In work [2] authors treat the issue of partial-order algebras and their relations to P/T nets based on the theory of BPA and ACP. Within our work we propose the general approach to characterising PN in form of E-(B-) terms. General (not only interleaving) semantics is given, and the results obtained in this respect are published in [9]. mFDT Environment is under construction, based on FDT interfaces by the authors, which aims to integrate the three formal methods mentioned above. 3 Petri Nets We assume the class of ordinary Petri nets [18] within this paper, and brief description of the basic notions follows [7]. Definition 1. The Petri net is a 4-tuple N = (P, T, pre, post), where P is a finite set of places, T is a finite set of transitions (P n T = 0), pre: P x T — {0,1} is the preset function and post: P x T — {0,1} is the postset function. By the marking of PN N = (P, T, pre, post) we mean a totally defined function m: P — IN, where IN is the set of natural numbers. We denote marked net with initial marking m0 as N0 = (N, m0) or N0 = (P, T,pre, post, m0). Some useful notations can be defined: *t = {p\pre(p, t) = 0}the set of preconditions of t t = {p\post(p, t) = 0}the set of postconditions of t p* = {t\pre(p,t) = 0}, • p = {t\post(p,t) = 0} We say that t is enabled in m (and denote it m ) if for every p e *t, m(p) > pre(p, t). The effect of firing t in m is the creation of a new marking m' (m -— m') and m' is defined in the following way: m'(p) = m(p) — pre(p,t) + post(p,t),p e P,t e T Denotation (N,m) (N,m') is alternatively used within the paper for expressing a step of computation (m -— m') within the Petri net N. The set of reachable markings for given Petri net N0 = (P, T, pre, post, m0) we define by R(Nq) = {m\mo — m} where a = t1,t2...tr stands for an admissible firing sequence in N0. We also can define the language of Petri net No: L(No) = {a e T*\mo — m} 4 APC - Algebra of Process Components Process algebra APC [8, 16] is inspired by the process algebra ACP [1]. ACP is modified in a way, that allows for comfortable description of PN processes in the algebraic way. We use the same operators for the sequential ( ) and the alternative (+) composition respectively and corresponding axioms also hold in algebra APC (Table 1). ACP's communication function (y) and its extension -communication merge operator (\), are not present in APC. A composition function (n) and a special composition operator (\\\) are introduced into the algebra APC instead. The impact of an introduction of the two operators will be treated later. APC is defined as a couple (P, £), where P (the domain) is represented by the set of constants, set of variables and set of all processes (terms) we are able to express. £ (the signature) contains function (operator) symbols. It is supposed that, the set of variables contain arbitrary many of them (x,y,...). Terms containing variable(s) are called open terms, otherwise terms are closed. 4.1 Syntactical issues From the syntactical point of view APC contains a number of constants a,b,c,... (we use the set A = {a,b,c,...} for referring to them) a special constant S (deadlock) and operators: +, •, || (parallel composition), [ (left merge) and ||| (process component composition). It also contains a (partial) commutative composition function n, denoting the merging of process components. Now we will define APC terms: Definition 2. 1. variables are APC terms, 2. constants a e A and a special constant S are APC terms, 3. if u, v are APC terms, then u + v,u • v, u || v,u [[v^W are APC terms, 4. if u is APC term, then u[c\ c e IN is also APC term. APC SEMANTICS FOR PETRI NETS Informatica 32 (2008) 253-260 2 55 All these terms are part of P - the domain of APC. P can further be subdivided into two parts PA and PC (P = PA U PC). Terms belonging to the set PA defined by items 1, 2 and 3 of Definition 2 (i.e. those without the superscript notation) represent the set of true processes. Terms from the set PC (superscripted) represent the set of process components. Only difference between the (true) process and process component is, that while the process is able to execute actions, process component is introduced for synchronization purpose only. The latter is only able to join with its counterparts) (other process component(s) fitting for being synchronized to) in order to form a true process. The composition function n is defined as follows: : Pcx ... x Pc n : Pc Pa (1) A connection between the composition function n and the process component composition operator (|||) can be expressed as: xi|||...|||xn = n(x1,...,xn) when n(x1, ..,xn) is defined. Axioms of algebra APC can be found in Table 1. Within the table u, v, z, xi,..., xn stand for processes, a e A and S are constants. u + v = v + u A1 u + u = u A2 (u + v) + z = u + (v + z) A3 (u + v) • z = uz + vz A4 (u • v) • z = u • (v • z) A5 u\\v = u |[v + v |[u + uH\v A6 (u + v)|||z = uHz + vmz A7 u|||(v + z) = uH\v + uHz A8 au |[v = a(u\\v) A9 (u + v) \[z = u\[z + v \[z A10 xi|||...|||xn = n(xi, ...,xn) if A11 n(x1;..., xn) is defined ^^ 11||... ||| ^^^^ = S otherwise u + S = u A12 S • u = S A13 Table 1: Axioms of APC Theorem 1. In the case of the parallel composition of more than two processes the following equality (expansion theorem) can be proven: 1 u ^ i a , u + v —> u i a , v + u —> u a / u • v —> u • v u\\v u'\\v v\\v, —— v\\v,' u |[v —— u'\\v a / u —> u , n(u[1\..,u[n]) = u ^ u[1]|||...|||u["] u' a e A, u e PA, ul1],...,ul"] G Pc, u',v G P Table 2: Transition relations for APC terms 5 APC semantics for Petri Nets In this section the transformation description is given in detail [16]. We start with creating a special variable for every place in the PN N to be transformed. We call these variables E-variables here, and they will be bound to terms, representing possible computations started from given place in PN, later. So the value (term) assigned to a particular variable depends on the structure of the net in the vicinity of a place associated. So considering the place p, variable E(p) will be bound to a term representing all the computations within the net N, which are initiated in p. a) b) c) Figure 1: Petri net fragments Basic situations are captured in Fig. 1. In the case a) a situation is depicted, where no arcs are connected to the place investigated. This results to the assignment of a term representing no computations to the variable corresponding to such place, i.e. S (deadlock). Case b) stands for an alternative composition (choice). If a token is situated in place p, a choice is to be made, and only one of transitions t1, ...,tn can fire. Case c) represents general composition, where tokens must be present in all pre-places of transition t. If some of these places does not contain a token, firing of t is not possible. After firing of t, however post-places of it are marked and thus processes initiated in those places are enabled. General composition (case c) can be understood as a generalization of the three basic compositions - sequential, parallel and synchronization (Fig. 2) - three of four basic composition mechanisms (with alternative composition) used within the APC. If n is the number of pre-places and m, the number of post-places of a transition t: - n =1 A m =1 we obtain sequential composition (case a) of Fig. 2), - n =1 A m > 1 we obtain parallel composition (case b) of Fig. 2), - n > 1 A m =1 we obtain synchronization (case c) of Fig. 2). Now we can proceed by constructing terms representing possible computations for given places of PN N. These will be bound to a corresponding E-variables in a way given by the definition: Definition 3. According to the structure of Petri net in the vicinity of a given place, terms are bound to corresponding variables for elementary situations depicted in figures Fig. 1 and Fig. 2 as follows: APC SEMANTICS FOR PETRI NETS Informatica 32 (2008) 253-260 2 57 Figure 2: Basic compositions as a special cases of the general composition - deadlock (Fig. 1a): E(p) = S - alternative composition (Fig. 1b): E(p) = h • E(qi) +t2 • E(q2) + ... + tn • E(qn) - sequential composition (Fig. 2a): E(p) = t • E(q) - parallel composition (Fig. 2b): E(p) = t • (E(qi) y... y E(qn)) - synchronization (Fig. 2c): E(pi) = (t • E(q))[i ,Ep) = (t • E(q))V\..,E (pn ) = (t • E (q))[n], and the composition function is defined: n((t • E(q))[i],.., (t • E(q))n) = t • E (q) or n(E(pi ),..., E(pn))= t • E (q) - general composition (Fig. 1c): E(pi) = (t • (E(qi) y... y E(qm)))[i], E(p2) = (t • (E(qi) y... y E(qm)))[2],..., E(pn) = (t • (E(qi) y... y E(qm)))[n, and the composition function is defined in the following way: n(E(pi ),..., E(pn))= t • (E (qi) y ... y E(qm )) - transition without post-place(s) (Fig. 3a): E(p) = t - transition without pre-place(s) (Fig. 3b): a new place is added, such that firing properties of a transition given are preserved (Fig. 3c): E(p) = t • E(q). In the case of the synchronization we can observe that, all variables composed are assigned to terms representing process components instead of true processes. These components, if all are present within the term representing the net computation, can merge together by means of composition function n, and form the true process (able to execute action t and then to behave like E(q)). Taking into account the case, when a transition without pre-places occurs within the net structure (Fig. 3b), the following solution is proposed: for every such transition t, a new pre-place is added, such that the firing properties of transition t are preserved (Fig. 3c). This is achieved by setting the initial marking of given place to w, where Figure 3: Transitions without input/output G IN : w ± n = w. In fact, this causes the transition t can be fired infinitely many times. Combining these basic principles, we are able to construct terms for more complicated net structures. Definition 4. Let the PN N is given by N = (P,T, pre, post), m G lNfc stands for its initial marking, and k = \P\. Then the APC semantics for N with marking m is given by the formula: A(N,m) = E(p1)(il)\\...\\E(pk )(ik > (4) Within the Definition 4, E(pi) stands for an APC-term defined according to PN structure in the vicinity of the place pi (Definition 3). The value ij is given by ij = m(pj), so it represents the marking with respect to place pj, 1 < j < k. E(pj)(i) is defined as a term E(pj )\\...\\E (pj), and represents a multiple (i-times) parallel composition of a process E(pj). Note that E(pj )(0) = S. When ij = w for place pj, it means that E(pj) can occur infinitely many times in resulting composition. Theorem 2. For given PN N = (P, T, pre, post), APC-term p, representing an algebraic (APC) semantics for the net N, transition t G T and m, m' markings of N, following implication holds: (N, m)-^(N, m') ^ A(N, m)-^A(N, m') Proof 2. The proof is given by the induction on a structure of the net. Let us suppose, that a step in computation of N exists: (N, m)-— (N, m'), then Vpi G (*t) : m(pi) > pre(pi,t) Vpi G P : m'(pi) = m(pi) - pre(pi,t) + post(pi,t) Algebraic semantics for Petri net N with marking m is given by: A(N,m)= E(pi)(il)\\...\\E(pk)(ik), k = \P\ (5) Transition t fired in N within a step can be of two kinds: 1. \'t\ = 1 2. \*t\ > 2 258 Informática 32 (2008) 253-260 S. Simonák et al. According to the transition relations of APC (Table 2), a step can be made by executing the action of the true process or by merging the process components together with execution of an action associated. Let us explore the two cases: 1. If |*t| = 1 is the case, the situation is captured in the Fig. 4, case a). Then within the Petri net N holds: m(pa) > pre(pa,t) (so the place pa contains a to-ken(s)) and also m'(pi) = m(pi) + post(pi,t) — pre(pi,t),pi e P is a new marking after firing of the transition t. If E(pa) = t ■ (E(pc)\\...\\E(pd)) is corresponding APC semantics for process initiated in the place pa, then a step (action t) is enabled E(pa)—E(pc)\\...\\E(pd), since Ep) is present in specification A(N, m). Let values jl, l e {1,..., k} are given by: jl = il — pre(pl,t) + post(pl,t). When a step A(N, m )—A(N, m') occurs, corresponding APC semantics of the net (N,m') is given by: A(N, m') = E(p1)(jl)\\...\\E(pk )j >, (6) k = \P \ a) b) Figure 4: Two cases considered for a step in computation of N 2. Here transition t firing in Petri net N occurs, for which |*t| > 2 holds. Situation is depicted in Fig. 4, case b). Within the Petri net N there holds: m(pa) > pre(pa,t),... ,m(pb) > pre(pb,t) (so the places pa,.. .,pb contain enough tokens) and thus transition t can fire. From the definition of APC semantics for Petri net N (5) and Definition 3, we have that a step from (N, m) is represented by: E(Pa )(ia ] \\ E (Pc )(jc) E (pb \\ E(pd)j (7) The step is enabled in A(N, m) since values ia,... ,ib are given by number of tokens in corresponding places. According to the definition, variables E(pa),...,E(pb) are bound to process components and composition function is defined: n(E(pa),..., E(pb)) = t ■ (E(pc) \\ ... \\ E(pd)). The step (7) thus is enabled, and (6) holds, where: j = il +post(pi,t) —pre(pi,t),...,jk = ik +post(pk ,t) — pre(pk ,t). We can conclude, that if a step in Petri net N with marking m is enabled, so it is enabled also in corresponding algebraic representation A(N, m). □ We give a small example here, representing the configuration of Petri net N sometimes called confusion (Fig. 5) for the sake of clarity. Pi Figure 5: Confusion First, APC-terms are assigned to variables created for every place of Petri net N. Ep)= h • E(qi) + (t2 • E(q2))[1], E(p2) = (t2 • E(q2))[2] Next, the composition function n is defined: n((t2 ■ E(q2))[1], (t2 ■ E(q2)) ) = t2 ■ E(q2) (8) Within the initial marking m0 of Petri net N, the only place holding a token is p1, so only the variable corresponding to this place will be included within the equation describing the algebraic semantics of N. A(N, mo) = E(pi) = ti ■ E (qi) + (t2 ■ E (q2))[1] = ti ■ E(qi) + S = ti ■ E(qi) In the configuration depicted, the only transition enabled is ti and it can fire. This is not the case of the transition t2, because the place p2, the pre-place of t2 is not marked. The same could be observed within the APC representation - only one process component ((t2 ■ E(q2 ))[i]) is present within the equation (so the mapping n cannot be used to produce a true process) and it thus cannot perform any action and is replaced by the S. 6 An example An example has been chosen to demonstrate a way how the transformation rules proposed can be used. The Petri net N APC SEMANTICS FOR PETRI NETS Informatica 32 (2008) 253-260 2 59 (depicted in Fig. 6) represents a synchronization problem for sharing one resource by two processes. System modeled consists of two processes (let the first process represented by the places pi,p2 and transitions ti; t3, be named A, and the second one (p3,p4, t2, t4) be named B). The resource shared is represented by the place po. The token at this place indicates the resource is free to be shared either by process A or process B. The place p2 stands for the condition 'process A is using the resource', firing transition ti starts the resource usage and firing t3 ends it. Similarly, for process B, firing t2 starts and firing t4 ends the usage respectively. A token occurrence in the place p3 indicates the resource is used by the process B. A(N,mo) = E(po) y E(pi) y E(p4) (11) Since the term on the RHS of equation (11) represents parallel composition of three processes, we expand it according to (2): = E(po) l(E(pi) y E(p4)) + E(pi) l(E(po) y E(p4)) + E(p4) l(E(po) y E(pi))+ (E (po)|||E(p1)) lE(pi) + (E(po)|||E(p4)) IE (pi) + (E (Pi)|||E(p4)) |LE(po)+(E(po)|||E (pi)|||E(p4)) After substituting terms assigned (bound) to variables E(p0), E(p1) and E(p4), we can write: = [(ti • E(p2))[2] + (t2 ■ E(p3))[2] ] l((ti ■ E(p2))[1] || (t2 ■ E(p3))[i]) + (ti ■ E(p2))[il |[((ti ■ E(p2))[2] + (t2 ■ E(p3))I2l ] y (t2 ■ E(p3))W) + E(p3))[il[((ti ■ E(p2))[2+(t2 ■ E(p3))[21 ] (t (t2 Figure 6: Petri net for resource sharing We start with assigning APC-terms to variables created for every place of PN N, according to the structure of the net in the vicinity of the corresponding place. E(pi) = (ti • E(p2))[il , E(p2) = ts(E(po) y E(pi)), E(ps) = t4(E(po) y E(p4)), E(p4) = (t2 • E(p3))W , E(po) = (ti • E(p2))I2l+(t2 • E(p3))[2l Composition function n is defined in two cases: n((ti ■ E(p2))[i], (ti ■ E(p2))[2] ) = ti ■ E(p2) (9) n((t2 ■ E(p3))[i], (t2 ■ E(p3))[2]) = t2 ■ E(p3) (10) Since the initial marking of Petri net N is given as m0 = (1,1,0,0,1), only three places (p0, pi andp4) hold tokens, and only variables corresponding to these places will take place in equation describing the algebraic semantics of PN N. • E(p2))[i])+ ([(ti • E(p2))[2] + (t2 • Efe))[2] ]|||(ti • E(p2))[i] ) l(t2 • E(p3))[il + ([(ti • E(p2))[2 + (t2 • E(p3))[2]]|||(t2 • E(p3))[il ) l(ti • E(p2))[i] + ((ti • E(p2))[i] |||(t2 • E(p3))[il) l[(ti • E(p2))[2 + (t2 • E(p3))[2] ]+ ([(ti • E(p2))[2] + (t2 • E(p3))[2]]|||(ti • E(p2))[i] |||(t2 • E(p3))[il ) Using the composition (n) definition (9, 10) and axioms associated (A11, A13), we have: (ti ■ E(p2)) |(t2 ■ E(p3))[il + (t2 ■ E(p3)) |(ti ■ E(p2))[il Using the left merge operator axiom (A9) and substituting for E(p2) and E(p3) we obtain: = ti(E(p2) y (t2 ■ E(p3))[i])+ t2(E(p3) y (ti ■ E(p2))W) = ti(t3(E(po) y E(pi)) y (t2 ■ E(p3))[il) + t2(t4(E(po) y E(p4)) y (ti ■ E(p2))W) Considering all the cases for two processes composed by the parallel composition operator (y ) and using the axiom A6: = ti(t3(E(po) y E(pi)) |(t2 ■ E(p3))w + (t2 ■ E(p3))[il|t3(E(po) y E(pi))+ t3 (E (po) y E(pi))|||(t2 ■ E (p3))[i] ) + t2(t4(E(po) y E(p4)) |(ti ■ E(p2))[il + (ti ■ E(p2))[il[t4(E(po) y E(p4))+ t4(E(po) y E(p4))|||(ti ■ E(p2))[il) = ti(t3(E(po) y E(pi))|(t2 ■ E(p3))[il + S + 5)+ t2(t4(E(po) y E(p4))|(ti ■ E(p2))W + S + S) = tit3((E(po) y E(pi)) y (t2 ■ E(p3))[ii)+ t2t4((E(po) y E(p4)) y (ti ■ E(p2))[il ) Since E(p4) = (t2 E(p2))[i], we can write: = tit3((E (po) t2t4((E(po) = tit3(E (po) t2t4(E(po) E(p3))[i] and E(pi) = (ti E(pi)) y E(p4))+ E(p4)) y E(pi)) E(pi) y E(p4))+ E(pi) y E(p4)) Using axiom A4, the term becomes even simpler: = (tit3 + t2t4)(e(po) y E(pi) y e(p4)) 260 Informática 32 (2008) 253-260 S. Simonák et al. Here we can observe a parallel composition of the three variables, from which we started our derivation (E(p0) || E(pi) || E(p4)). In terms of Petri nets, the initial marking was reached again. Prefix (tits +t2t4) represents the traces of processes. The sequential composition operator is often omitted, so we can state that the APC semantics is finally given by the following equation: A(N,mo) = (tits + t2hT 7 Conclusion In this paper a general method was presented for constructing an algebraic semantics of Petri nets, based on Algebra of Process Components (APC) by the authors. The notion of process component is introduced in order to model synchronization, which, in case of Petri nets, is modeled in a natural way. A variable is created for every place of given net and a term is bound to this variable, which express the process initiated in the corresponding place. The description of process representing computations of Petri net is given by the parallel composition of all the variables associated with places holding token(s) within the initial marking. Traces of processes can be observed in addition to changes on the PN marking along the computation. Resulting algebraic specification can further be analyzed using process algebra tools like CWB-NC, etc. A proof of identical operational behavior has also been provided. The PETRI2APC tool, a practical implementation of method presented, is intended to be a part of multi FDT (mFDT) environment - an environment for designing and analysing of discrete systems based on three formal methods with useful complementary properties. The methods considered are Petri nets, Process algebra and B-Method. The mFDT environment is under development at DCI FEEI TU of Kosice. Acknowledgement This work is supported in part by the VEGA 1/3140/06 and in part by the VEGA 1/4073/07 grant projects of Slovak Grant Agency. References [1] Baeten, J.C.M., Weijland, W.P.: Process Algebra, Cambridge University Press, ISBN 0 521 40043 0, pp.248, 1990. [2] Baeten, J.C.M., Basten, T.: Partial-Order Process Algebra, in Handbook of Process Algebra, Elsevier Science, Amsterdam, The Netherlands, 2000, 78pp. [3] Basten, T., Voorhoeve, M.: An Algebraic Semantics for Hierarchical P/T Nets, Computing Science Report, Eindhoven University of Technology, pp.32, 1995. [4] Best, E.: Semantics of Sequential and Parallel Programs, Prentice Hall Europe, ISBN 0-13-460643-4, pp.352, 1996. [5] Best, E., Devillers,R., Koutny,M.: Petri Nets, Process Algebras and Concurrent Programming Languages , Lecture on Petri Nets II:Applications, LNCS , Advances in Petri Nets (W.Reisig,G.Rozenberg Eds.), Springer , Berlin 1998, ISBN 3-540-65306-6,pp.1-84. [6] Desel, J., JuMs, G., Lorenz, R.: Process Semantics of Petri Nets over Partial Algebra, Proceedings of ICATPN 2000, 21-st International Conference on Application and Theory of Petri Nets, vol.1825 of LNCS, pp.146-165, Springer-Verlag, 2000. [7] Hudik, S.: Reachability Analysis of Systems Based on Petri Nets, Elfa s.r.o. Kosice, ISBN 80-88964-075, pp.272, 1999. [8] Hudik, S., SimoMk, S.: APC - Algebra of Process Components, Proceedings of EMES'03, Oradea, Felix Spa, Romania, May 2003, pp. 57-63, ISSN 1223 - 2106. [9] Hudik S., Simonik S., Korecko S., N.Kovacs A.: Formal Specifications and de/compositional approach to design and analysis of discrete systems, Computer Science and Technology Research Survey, Kosice, Elfa, pp. 8-46, 2007. [10] Mayr, R.: Combining Petri nets and PA-processes, in Theoretical Aspects of Computer Software (TACS'97), volume 1281 of Lecture Notes in Computer Science, pages 547-561, Sendai, Japan, 1997. Springer Verlag. [11] Olderog, E.R.: Nets, Terms and Formulas, ISBN 0 521 40044 9, Cambridge University Press, 1991. [12] Paige, R.F.: Formal Method Integration via Heterogeneous Notations, PhD Dissertation, November 1997. [13] PNML-Petri Net Markup Language, URL: http://www.informatik.hu-berlin.de/ top/pnml/ [14] PNML Framework, URL: http://www-src.lip6.fr/logiciels/mars/PNML/ [15] SimoMk, S., Hudik, S., Korecko, S.: ACP2PETRI: a tool for FDT integration support, Proceedings of 8th International Conference EMES'05, Oradea, Felix Spa, Romania, 2005, pp. 122-127, ISSN 12232106. [16] SimoMk, S.: Formal methods integration based on Petri nets and process algebra transformations, PhD Dissertation, DCI FEEI TU Kosice, 2003. (In Slovak) [17] Starke, P.H.: Processes in Petri Nets, LNCS 117, Fundamentals of Computation Theory, ISBN 3-54010854-8, Springer-Verlag, 1981. [18] Petri Nets World (A Classification ofPN), URL: http://www.informatik.uni- hamburg.de/TGI/PetriNets/classification/