APC semantics for Petri nets.

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 Petri nets. This is done by assigning special variables (called E-variables here) to every place of given Petri net, 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.

Keywords: Petri nets semantics, process algebra, algebra of process components

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.sub.1], than it is the case for f in [F.sub.2]. 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 composionality, 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 [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 [intersection] T = 0), pre: P x T [right arrow] {0, 1} is the preset function and post: P x T [right arrow] {0.1} is the postset function.

By the marking of PN N = (P, T. pre, post) we mean a totally defined function m: P [right arrow] IN, where IN is the set of natural numbers. We denote marked net with initial marking [m.sub.0] as [N.sub.0] = (N, [m.sub.0]) or [N.sub.o] = (P, T, pre, post, [m.sub.0]).

Some useful notations can be defined:

*t = {p|pre(p, t) [not equal to] 0} the set of preconditions of t

t* = {p|post(p, t) [not equal to] 0} the set of postconditions of t

p* = {t|pre(p, t) [not equal to] 0}, *p = {t|Post(p, t) [not equal to] 0}

We say that t is enabled in m (and denote it m [??]) if for every p [member of] *t, m (p) [greater than or equal to] pre(p, t). The effect of firing t in m is the creation of a new marking m' ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]) and m' is defined in the following way:

m'(p) = m(p) - pre(p. t) + post(p, t), p [member of] P. t [member of] T

Denotation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is alternatively used within the paper for expressing a step of computation ([MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]) within the Petri net N. The set of reachable markings for given Petri net [N.sub.0] = ( P, T, pre, post, [m.sub.0]) we define by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where [sigma] = [t.sub.1], [t.sub.2] ... [t.sub.r] stands for an admissible firing sequence in No. We also can define the language of Petri net [N.sub.0]:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

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 (x) and the alternative (+) composition respectively and corresponding axioms also hold in algebra APC (Table 1). ACP's communication function ([gamma]) and its extension communication merge operator (|), are not present in APC. A composition function ([pi]) and a special composition operator ([absolute value of |]) 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, [ZIGMA]), 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. [ZIGMA] (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 [delta] (deadlock) and operators: +; [parallel] (parallel composition), [??] (left merge) and [??] (process component composition). It also contains a (partial) commutative composition function [pi], denoting the merging of process components. Now we will define APC terms:

Definition 2. 1. variables are APC terms,

2. constants a [member of] A and a special constant [delta] are APC terms,

3. if u, v are APC terms, then u + v, u x v, u [parallel] v, u [??] v, u [??]] v are APC terms.

4. if u is APC term, then [u.sup.[c]], c [member of] IN is also APC term.

All these terms are part of P--the domain of APC. P can further be subdivided into two parts [P.sub.A] and [P.sub.C] (P = [P.sub.A] [union] [P.sub.C]). Terms belonging to the set [P.sub.A] 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 [P.sub.C] (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 counterpart(s) (other process component(s) fitting for being synchronized to) in order to form a true process. The composition function [pi] is defined as follows:

[pi]: [P.sub.C] x ... x [P.sub.C] [right arrow] [P.sub. A] (1)

A connection between the composition function [pi] and the process component composition operator ([absolute value of |]) can be expressed as: [x.sub.1] [??] ... [??] [x.sub.n] = [pi] ([x.sub.1], ..., [x.sub.n]) when [pi]([x.sub.1], ..., [x.sub.n]) is defined. Axioms of algebra APC can be found in Table 1. Within the table u, v, z, [x.sub.1], ..., [x.sub.n] stand for processes, a [member of] A and [delta] are constants.

Theorem 1. In the case of the parallel composition of more than two processes the following equality (expansion theorem) can be proven:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (2)

Proof 1. By induction on n, the number of processes. The case for n = 2 is treated by the axiom A6, Table 1. The induction step is as follows:

([x.sub.1] [parallel] ... [parallel] [x.sub.n+1]) = ([x.sub.1] [parallel] ... [parallel] [x.sub.n]) [parallel] [x.sub.n+1]

Denoting the RHS of original theorem as E, we can write:

([x.sub.1] [parallel] ... [x.sub.n]) [parallel] [x.sub.n+1] = E = [parallel] [x.sub.n+1] + [x.sub.n+1] [paralllel] [E + E] [parallel] [x.sub.n+1] (3)

Now we have three summands, each of them will be treated separately. Let's start dealing with the first of them.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The second summand of(3) can be expressed as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

The third one represents the process components composition:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Summing up the three summands we have:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

4.2 Semantics issues

Constants a, b, c [member of] A are called atomic actions, and are considered indivisible actions (events). The sequential composition operator (x) function can be explained as follows: x x y is the process that first executes x and after finishing it, starts y. The alternative composition (+): x + y is the process that either executes z or y (choice). The meaning of parallel composition ([parallel]) follows: considering the merge of two processes x [parallel] y, we recognize three possibilities to proceed. Either we start with a first step of x (given by x [??] y), or a first step from y (y [??] x) or we check a possibility to compose processes by means of process components composition operator - x [??] y. The result of this composition of course is different from [delta] only in a case, when the composition function [pi] is defined.

To assign an operational semantics to process expressions, we determine, which actions a process can perform. The fact, that process represented by the term t can execute action a and turn to the term s is denoted by: [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (or alternatively a is enabled in t). The symbol [square root] stands for successful termination and thus [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] denotes a fact that can terminate by executing a. An inductive definition of action relations is given in the Table 2.

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.

[FIGURE 1 OMITTED]

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. [delta] (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 [t.sub.1], ..., [t.sub.n], 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 [conjunction] m = 1 we obtain sequential composition (case a) of Fig. 2),

- n - 1 [conjunction] m > 1 we obtain parallel composition (case b) of Fig. 2),

- n > 1 [conjunction] 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:

[FIGURE 2 OMITTED]

--deadlock (Fig. 1a): E(p) = [delta]

--alternative composition (Fig. 1b): E(p) = [t.sub.1] x E([q.sub.1]) + [t.sub.2] x E([q.sub.2]) + ... + [t.sub.n] x E([q.sub.n])

--sequential composition (Fig. 2a): E(p) = t x E(q)

--parallel composition (Fig. 2b): E(p) = t x (E([q.sub.1]) [parallel] ... [parallel] E([q.sub.n]))

--synchronization (Fig. 2c): E([p.sub.1]) [(t x E(q)).sup.[1]), E([p.sub.2]) = [(t x E(q)).sup.[2]]), ..., E([p.sub.n]) = (t x E(q).sup.[n],

and the composition function is defined: [pi][((t x E(q)).sup.[1]], ..., [(t x E(q)).sup.[n]]) = t x E(q) or [pi](E([p.sub.1]), ... E([p.sub.n])) = t x E(q)

--general composition (Fig. 1c): E([p.sub.1]) = (t x (E([q.sub.1]) [parallel] ... [parallel] E(q.sub.m]))).sup.[1]], E([p.sub.2]) = (t x (E([q.sub.1]) [parallel] ... [parallel] E[([q.sub.m]))).sup.[2]] , ..., E([p.sub.n]) = (t x (E([q.sub.1]) [parallel] ... [parallel] E([[q.sub.m]))).sup.[n]], and the composition function is defined in the following way:

[pi](E([p.sub.1]), ..., E([p.sub.n])) = t x (E([q.sub.1]) [parallel] ... [parallel] E([q.sub.m]))

--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 x 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 [pi], 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 OMITTED]

[for all]n [member of] IN: w [+ or -] 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 [member of] [IN.sub.k] stands for its initial marking, and k = [absolute value of P]. Then the APC semantics for N with marking m is given by the formula:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (4)

Within the Definition 4, E([p.sub.i]) stands for an APC-term defined according to PN structure in the vicinity of the place [p.sub.i] (Definition 3). The value [i.sub.j] is given by [i.sub.j] = m([p.sub.j]), so it represents the marking with respect to place [p.sub.j], 1 [less than or equal to] k. E[([p.sub.j]).sup.(i)] is defined as a term E([p.sub.j])[parallel] ... [parallel] E ([p.sub.j]), and represents a multiple (i-times) parallel composition of a process E([p.sub.j]). Note that E([p.sub.j])(o) = [delta]. When [i.sub.j] = w for place [p.sub.j], it means that E([p.sub.j]) 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 [member of] T and m, m' markings of N, following implication holds:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

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: [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] then

[for all][p.sub.i] [member of] (*t): m([p.sub.i]) [greater than or equal to] pre([p.sub.i], t)

[for all][p.sub.i] [member of] P: m' ([p.sub.i]) = m([p.sub.i]) = m([p.sub.i]) - pre([p.sub.i], t) + post([p.sub.i], t)

Algebraic semantics for Petri net N with marking m is given by:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (5)

Transition tilted in N within a step can be of two kinds:

1. [absolute value of *t] = 1

2. [absolute value of *t] [greater than or equal to] 2

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 [absolute value of *t] = 1 is the case, the situation is captured in the Fig. 4, case a). Then within the Petri net N holds: m([p.sub.a]) [greater than or equal to] pre([p.sub.a], t) (so the place [p.sub.a] contains a token(s)) and also m'([p.sub.i]) = m([p.sub.i]) + post([p.sub.i], t) - pre([p.sub.i], t), [p.sub.i] [member of] P is a new marking after firing of the transition t. If E([p.sub.a]) = t x (E([p.sub.c]) [parallel] ... [parallel] E([p.sub.d])) is corresponding APC semantics for process initiated in the place [p.sub.a], then a step (action t) is enabled E([p.sub.a]) [??] E([p.sub.c]) [parallel] ... [parallel] E([p.sub.d]), since E ([p.sub.a]) is present in specification A(N, m). Let values [j.sub.l], l [member of] {1,.... k} are given by: [j.sub.l] = [i.sub.l] - pre([p.sub.l], t) + post([p.sub.l], t). When a step [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] occurs, corresponding APC semantics of the net (N, m') is given by:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. (6)

[FIGURE 4 OMITTED]

2. Here transition t firing in Petri net N occurs, for which [absolute value of *t] [greater than or equal to] 2 holds. Situation is depicted in Fig. 4, case b). Within the Petri net N there holds: m([p.sub.a]) [greater than or equal to] pre([p.sub.a], t), ..., m([p.sub.b]) [greater than or equal to] pre([p.sub.b], t) (so the places [p.sub.a], ..., [p.sub.b] 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:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (7)

The step is enabled in A(N, m) since values [i.sub.a], ..., [i.sub.b] are given by number of tokens in corresponding places. According to the definition, variables E([p.sub.a]), ..., E([p.sub.b]) are bound to process components and composition function is defined:

[pi](E([p.sub.a]), ..., E([p.sub.b])) = t x (E([p.sub.c]) [parallel] ... [parallel] E([p.sub.d])). The step (7) thus is enabled, and (6) holds, where: [j.sub.1] = [i.sub.l] @post([p.sub.1], t) - pre([p.sub.1], t), ..., [j.sub.k] = [i.sub.k] + post([p.sub.k], t) - pre([p.sub.k], 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.

[FIGURE 5 OMITTED]

First, APC-terms are assigned to variables created for every place of Petri net N.

E([p.sub.1]) = [t.sub.1] x E([q.sub.1]) + [([t.sub.2] x E(q2)).sup.[1], E([p.sub.2]) = [([t.sub.2] x E([q.sub.2])).sup.[2])

Next, the composition function [pi] is defined:

[pi][(([t.sub.2] x E([q.sub.2])).sup.[2]]. [([t.sub.2] x E([q.sub.2])).sup.[2]] = [t.sub.2] x E([q.sub.2]) (8)

Within the initial marking [m.sub.0] of Petri net N, the only place holding a token is [p.sub.1], so only the variable corresponding to this place will be included within the equation describing the algebraic semantics of N.

A(N, [m.sub.0]) = E([p.sub.1]) = [t.sub.1] x E([q.sub.1]) + [([t.sub.2] x E([q.sub.2]).sup.[1]] = [t.sub.1] x E([q.sub.1]) + [delta] = [t.sub.1] x E([q.sub.1])

In the configuration depicted, the only transition enabled is [t.sub.1] and it can fire. This is not the case of the transition [t.sub.2], because the place [p.sub.2], the pre-place of t2 is not marked. The same could be observed within the APC representation --only one process component [(([t.sub.2] x E([q.sub.2])).sup.[1]]) is present within the equation (so the mapping [pi] cannot be used to produce a true process) and it thus cannot perform any action and is replaced by the [delta].

6 An example

An example has been chosen to demonstrate a way how the transformation rules proposed can be used. The Petri net N (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 [p.sub.1], [p.sub.2] and transitions [t.sub.1], [t.sub.3], be named A, and the second one ([p.sub.3], [p.sub.4], [t.sub.2], [t.sub.4]) be named B). The resource shared is represented by the place [p.sub.0]. The token at this place indicates the resource is free to be shared either by process A or process B. The place [p.sub.2] stands for the condition 'process A is using the resource', firing transition [t.sub.1] starts the resource usage and firing [t.sub.3] ends it. Similarly, for process B, firing [t.sub.2] starts and firing [t.sub.4] ends the usage respectively. A token occurrence in the place [p.sub.3] indicates the resource is used by the process B.

[FIGURE 6 OMITTED]

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.

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Composition function [pi] is defined in two cases:

[pi][(([t.sub.1] x E([p.sub.2])).sup.[1]], [([t.sub.1] x E([p.sub.2]).sup.[2]]) = [t.sub.1] x E([p.sub.2]) (9)

[pi][(([t.sub.2] x E([p.sub.2])).sup.[1]], [([t.sub.2] x E([p.sub.3]).sup.[2]]) = [t.sub.2] x E([p.sub.3]) (10)

Since the initial marking of Petri net N is given as [m.sub.0] = (1, 1, 0, 0, 1), only three places ([p.sub.0], [p.sub.1] and [p.sub.4]) hold tokens, and only variables corresponding to these places will take place in equation describing the algebraic semantics of PN N.

A(N, [m.sub.0]) = E([p.sub.0]) [parallel] E([p.sub.1]) [parallel] E([p.sub.4]) (11)

Since the term on the RHS of equation (11) represents parallel composition of three processes, we expand it according to (2):

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

After substituting terms assigned (bound) to variables E([p.sub.0]), E([p.sub.1]) and E([p.sub.4]), we can write:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Using the composition ([pi]) definition (9, 10) and axioms associated (A11, A13), we have:

([t.sub.1] x E([p.sub.2]) [parallel] [([t.sub.2] x E([p.sub.3])).sup.[2]] + [([t.sub.2] x E([p.sub.3])) [parallel] ([t.sub.1] x E([p.sub.2])).sup.[1]]

Using the left merge operator axiom (A9) and substituting for E([p.sub.2]) and E([p.sub.3]) we obtain:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Considering all the cases for two processes composed by the parallel composition operator ([parallel]) and using the axiom A6:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Since E([p.sub.4]) = [([t.sub.2] x E([p.sub.3])).sup.[1]] and E([p.sub.1]) = ([t.sub.1] x E[([p.sub.2])).sup.[1]], we can write:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Using axiom A4, the term becomes even simpler:

= ([t.sub.1][t.sub.3] + [t.sub.2][t.sub.4])(E([p.sub.0]) [parallel] E([p.sub.1]) [parallel] E([p.sub.4]))

Here we can observe a parallel composition of the three variables, from which we started our derivation (E([p.sub.0]) [parallel] E([p.sub.1]) [parallel] E([p.sub.4])). In terms of Petri nets, the initial marking was reached again. Prefix ([t.sub.1][t.sub.3] + [t.sub.2][t.sub.4]) 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, [m.sub.0]) = [([t.sub.1][t.sub.3] + [t.sub.2][t.sub.4]).sup.[omega]]

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.

Received: July 13, 2007

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., Juhas, 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] Hudak, S.: Reachability Analysis of Systems Based on Petri Nets, Elfa s.r.o. Kogice, ISBN 80-88964-075, pp.272, 1999.

[8] Hudak, S., Simonak, S.: APC--Algebra of Process Components, Proceedings of EMES'03, Oradea, Felix Spa, Romania, May 2003, pp. 57-63, ISSN 1223 - 2106.

[9] Hudak S., Simonak 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, Kogice, 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://wwwsrc.lip6.fr/logiciels/mars/PNML/

[15] Simon, S., Hudak, 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 1223-2106.

[16] Simonak, 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-540-10854-8, Springer-Verlag, 1981.

[18] Petri Nets World (A Classification of PN), URL: http://www.informatik.unihamburg.de/TGI/PetriNets/classification/

Slavomir Simonak, Stefan Hudak and Stefan Korecko

Department of Computers and Informatics, Technical University of Kosice, Letna 9, 042 00 Kosice, Slovak Republic E-mail: [e-mail], [e-mail], [e-mail]

Table 1: Axioms of APC

u + v = v + u                                             A1
u + u = u                                                 A2
(u + v) + z = u + (v + z)                                 A3
(u + v) x z = uz + vz                                     A4
(u x v) x z = u x (v x z)                                 AS
u [parallel] v = u [parallel] v +
  v [parallel] u + u [parallel] | v                       A6
(u + v) [parallel] [absolute value of z = u]
  [parallel] z + v | [parallel] z                         A7
u [absolute value of [parallel] (v + z) =
  u [parallel]] v + u [parallel] | z                      A8
au [parallel] v = a(u [parallel] v)                       A9
(u + v) [parallel] z = u [parallel] z + v [parallel] z    A10
[x.sub.1] [absolute value of [parallel] ... [parallel]]
  [x.sub.n] = [pi] ([x.sub.1], ..., [x.sub.n]) if         A11
[pi]([x.sub.1], ..., [x.sub.n]) is defined
[x.sub.1] [absolute value of [parallel] ... [parallel]]
  [x.sub.n] = [delta] otherwise
u + [delta] = u                                           A12
[delta] x u = [delta]                                     A13

Table 2: Transition relations for APC terms

a [??] [square root]

                          u + v [??] u'
                          v + u [??] u'
u [??] u' [right arrow]   u x v [??] u' x v
                          v [parallel] v [??] u' [parallel] u'
                          u [parallel] v [??] u' [parallel] v

u [??] u',
[pi] ([u.sup.[1]], ..., u.sup.[n]] = u [right arrow] [u.sup.[1]]
[absolute value of [parallel] ... [parallel]] [u.sup.[n] [??] u'

a [member of] A, u [member of] [P.sub.A], [u.sup.[1]], ...,
[u.sup.[n]] [member of] [P.sub.c], u', v [member of P]