×

zbMATH — the first resource for mathematics

A logical approach of Petri net languages. (English) Zbl 0605.68049
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)
PDF BibTeX XML Cite
Full Text: DOI
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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.