• Accueil LIP6
  • Page : 'rapport_recherche' inconnue (menus.php)

LIP6 2000/024

  • Rapports de recherche
    Une procédure de décision du "model checking" pour les réseaux de Petri récursifs séquentiels
  • S. Haddad, D. Poitrenaud
  • 21 pages - 12/09/2000- document en - http://www.lip6.fr/lip6/reports/2000/lip6.2000.024.ps.gz - 113 Ko
  • Contact : Denis.Poitrenaud (at) nulllip6.fr
  • Ancien Thème : SRC
  • Les réseaux de Petri récursifs (RdPR) ont été introduits pour la modélisation de systèmes à structure dynamique. Bien que ce formalisme soit une stricte extension des réseaux de Petri et des grammaires "context-free" (par rapport aux langages engendrés), le problème de l'accessibilité reste décidable pour les RdPR. Toutefois, le type de logique temporelle qui est décidable pour les réseaux de Petri devient indécidable pour les RdPR. Dans ce travail, nous introduisons un sous- formalisme des RdPR appelé réseaux de Petri récursifs séquentiels (RdPRS) et nous étudions ses aspects théoriques. Nous commençons par montrer qu'il est possible de décider si un RdPR est un RdPRS. Ensuite, nous étudions les langages engendrés par les RdPRS en prouvant qu'ils inclues strictement l'union des langages réseaux de Petri et "context-free". De plus, la famille des languages des RdPRS est close par intersection avec les langages réguliers (à la différence de celle des RdPR). Cette propriété est le point de départ du "model checking" de la logique temporelle à temps linéaire basée sur les actions qui est aussi montré décidable. A notre connaissance, c'est la première fois qu'un tel résultat est obtenu pour un formalisme incluant stictement les réseaux de Petri et les grammaires "context-free".
  • Mots clés : Réseaux de Petri récursif, vérification de modèle et décidabilité
  • Directeur de la publication : Denis.Poitrenaud (at) nulllip6.fr
Mentions légales
Carte du site