Processes in Petri nets

Grzegorz Bancerek

Bialystok Technical University

Mitsuru Aoki

Shinshu University, Nagano

Akio Matsumoto

Shinshu University, Nagano

Yasunari Shidama

Shinshu University, Nagano

Summary.

Sequential and concurrent compositions of processes in Petri nets are introduced. A process is formalized as a set of (possible), so called, firing sequences. In the definition of the sequential composition the standard concatenation is used $$ R_1 \mathop{\rm before} R_2 = \{p_1\mathop{^\frown}p_2: p_1\in R_1\ \land\ p_2\in R_2\} $$ The definition of the concurrent composition is more complicated $$ R_1 \mathop{\rm concur} R_2 = \{ q_1\cup q_2: q_1\ {\rm misses}\ q_2\ \land\ \mathop{\rm Seq} q_1\in R_1\ \land\ \mathop{\rm Seq} q_2\in R_2\} $$ For example, $$ \{\langle t_0\rangle\} \mathop{\rm concur} \{\langle t_1,t_2\rangle\} = \{\langle t_0,t_1,t_2\rangle , \langle t_1,t_0,t_2\rangle , \langle t_1,t_2,t_0\rangle\} $$ The basic properties of the compositions are shown.

MML Identifier: PNPROC_1

Contents (PDF format)

1. Preliminaries
2. Markings on Petri Nets
3. Transitions and Firing
4. Firing Sequences of Transitions
5. Sequential Composition
6. Concurrent Composition
7. Neutral Process

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[4] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[7] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.

[8] Patricia L. Carlson and Grzegorz Bancerek. Context-free grammar --- part I. Journal of Formalized Mathematics, 4, 1992.

[9] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[10] Beata Madras. Product of family of universal algebras. Journal of Formalized Mathematics, 5, 1993.

[11] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.

[12] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[13] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[14] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[15] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[16] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.

[17] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[18] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.