A logical approach of Petri net languages (Q1083861)

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.