Decidability and Undecidability Results for Recursive Petri Nets

S. Haddad, D. Poitrenaud

LIP6 1999/019: Rapport de Recherche LIP6 / LIP6 research reports
26 pages - Septembre/September 1999 - Document en anglais.

PostScript : 151 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Systèmes Répartis et Coopératifs

Titre français : Résultats de décidabilité et d'indécidabilité pour les réseaux de Petri récursifs
Titre anglais : Decidability and Undecidability Results for Recursive Petri Nets

Résumé : Les réseaux de Petri récursifs (RdPR) ont été introduits pour modéliser des systèmes ayant une structure dynamique. Alors que ce modèle est une extension stricte des réseaux de Petri, le problème de l'accessibilité reste décidable. Dans ce papier, nous nous focalisons sur trois aspects théoriques complémentaires. Initialement, nous développons des procédures de décisions pour de nouvelles propriétés telles que le caractère borné et fini et nous montrons que les langages des RdPR sont récursifs. Dans un deuxième temps, nous étudions la puissance d'expression des RdPR en démontrant que tout langage récursivement énumérable peut être obtenu comme étant l'image, par un homorphisme, de l'intersection d'un langage régulier et d'un langage d'un RdPR. Nous déduisons de cette propriété des résultats d'indécidabilité incluant le type de "Model Checking" qui est décidable dans le cas des réseaux de Petri. Enfin, nous comparons les RdPR avec deux autres modèles combinant les caractéristiques des réseaux de Petri et les grammaires "Context-Free" en montrant que ces modèles peuvent être simulés par les RdPR.

Abstract : 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.

Mots-clés : Réseaux de Petri, Théorie des langages, Semantique, Récursivité

Key-words : Petri Nets, Language Theory, Semantic, Recursivity

Publications internes LIP6 1999 / LIP6 research reports 1999

Responsable Éditorial / Editor :Denis.Poitrenaud@lip6.fr