A logical formalism for the study of the finite behaviour of Petri nets

For languages recognized by finite automata we have two formalisms at our disposal: regular expressions (Kleene [3]) and logical formulas (Büchi [2]). In the case of Petri net languages there is no formalism like regular expressions. We give here a Büchi-like theorem which characterizes Petri net languages in terms of second order logical formulas.

This characterization 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 parentheses is well formed (in this paper "parentheses" always means the usual one sort of parentheses);

From a more practical point of view, the logical formalism has two advantages: 1. given a language, it enables us to easily prove that it is a Petri net language; 2. it gives an automatic procedure to construct a Petri net having a definite behaviour

The paper is organized as follows: in section 1 we present the Petri net formalism and the logical formalism. The proofs of the main results are sketched in section 2 (for details of them cf. [5]). Examples and applications are given in section 3.

Authors and Affiliations

1. CNRS U.A. 753, UER de Mathematiques et Informatique, Université Paris VII, 2, place Jussieu, 75251, Paris Cedex 05, France

   Michel Parigot

2. Laboratoire de Recherche en Informatique, CNRS U.A. 410, Université Paris-Sud, Bat. 490, 91405, Orsay Cedex, France

   Elisabeth Pelz

Reprints and permissions

© 1986 Springer-Verlag Berlin Heidelberg

Policies and ethics