LIP6 1999/019

• Rapports de recherche
  Résultats de décidabilité et d'indécidabilité pour les réseaux de Petri récursifs
• S. Haddad, D. Poitrenaud
• 26 pages - 25/09/1999- document en - http://www.lip6.fr/lip6/reports/1999/lip6.1999.019.ps.gz - 154 Ko
• Contact : Denis.Poitrenaud (at) nulllip6.fr, haddad (at) nulllamsade.dauphine.fr
• Ancien Thème : SRC
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.
• Mots clés : Réseaux de Petri, Théorie des langages, Semantique, Récursivité
• Directeur de la publication : Denis.Poitrenaud (at) nulllip6.fr