A logical approach of Petri net languages

AbstractFor languages recognized by finite automata we dispose of two formalisms: regular expressions (Kleene, 1956) and logical formulas (Büchi, 1960). In the case of Petri net languages there is no formalism like regular expressions. In this paper we give a Büchi-like theorem which characterizes Petri net languages in terms of second-order logical formulas. This characterization has two advantages: (1) It situates exactly the power of Petri nets with respect to finite automata; roughly speaking, Petri nets are finite automata plus the ability of testing if a string of parenthesis is well formed (in this paper ‘parenthesis’ always means the usual one sort of parentheses). (2) Given a language, it enables us to easily prove that it is a Petri net language.In addition we prove that Petri net languages and deadlock languages coincide