Comments on capabilities, limitations and “correctness” of Petri nets

In this paper we examine the capabilities and limitations of Petri nets and investigate techniques for proving their correctness. We define different classes of nets where each is basically a Petri net with slight modifications and study the relationship between the various classes. One particular class appears to be quite powerful, with respect to its capability for representing coordinations. In the second part of the paper we establish the feasibility of using the methods of computational induction and inductive assertions to prove restricted statements about Petri nets.