A logical approach of Petri net languages. (English) Zbl 0605.68049

Parigot, Michel; Pelz, Elisabeth

Theor. Comput. Sci. 39, 155-169 (1985).

The paper contributes with an important theorem to the development of Petri net language theory. This theorem characterizes Petri net languages in terms of second-order logical formulas giving three sentence forms from a monadic second-order logic \({\mathcal L}\) which are equivalent with a Petri net language. In addition, it is proved that Petri net languages and deadlock Petri net languages coincide. This characterization has two advantages: it proves that Petri nets are finite automata plus the ability of testing if a string of parenthesis is well formed, and it enables to easily prove that a given language is a Petri net language.

Reviewer: D.Cristea

MSC:

68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03D05	Automata and formal grammars in connection with logical questions
68Q45	Formal languages and automata
03B15	Higher-order logic; type theory (MSC2010)

Keywords:

Petri net language; monadic second-order logic; finite automata

References:

[1]	Brams, G.W., Réseaux de Petri, théorie et pratique, (1983), Masson Paris · Zbl 0501.68027
[2]	Büchi, J.R., Weak second-order arithmetic and finite automata, Z. math. logik und grundlagen der math., 6, 66-92, (1960) · Zbl 0103.24705
[3]	Kleene, M., Representation of events in nerve nets and finite automata, ()
[4]	Peterson, J.L., Petri net theory and the modeling of systems, (1981), Prentice-Hall Englewood Cliffs, NJ
[5]	Sifakis, J., Le contrôle des systèmes asynchrones: concepts, propriétés, analyse statique, (), Grenoble
[6]	Valk, R.; Vidal-Naquet, G., Petri nets and regular languages, J. comput. system sci., 23, 3, 299-325, (1981) · Zbl 0473.68057