Decidability and Undecidability Results for Recursive Petri Nets

Overview & Synopsis

Recursive Petri nets (RPNs) have been introduced to model systems with dynamic structure. Whereas this model is a strict extension of Petri nets, reachability in RPNs remains decidable. Here we focus on three complementary theoretical aspects. At first, we develop decision procedures for new properties like boundedness and finiteness and we show that languages of RPNs are recursive. Then we study the expressiveness of RPNs proving that any recursively enumerable language may be obtained as the image by an homomorphism of the intersection of a regular language and a RPN language. Starting from this property, we deduce undecidability results including undecidablity for the kind of model checking which is decidable for Petri nets. At last, we compare RPNs with two other models combining Petri nets and context-free grammars features showing that these models can be simulated by RPNs.