A model checking decision procedure for sequential recursive Petri nets

S. Haddad, D. Poitrenaud

LIP6 2000/024: Rapport de Recherche LIP6 / LIP6 research reports
21 pages - Septembre/September 2000 - Document en anglais.

Get it : 110 Ko /Kb

Contact : par mail / e-mail

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

Titre français : Une procédure de décision du "model checking" pour les réseaux de Petri récursifs séquentiels
Titre anglais : A model checking decision procedure for sequential recursive Petri nets

Résumé : 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".

Abstract : Recursive Petri nets (RPNs) have been introduced to model systems with dynamic structure. Whereas this model is a strict extension of Petri nets and context-free grammars (w.r.t. the language criterion), reachability in RPNs remains decidable. However the kind of model checking which is decidable for Petri nets becomes undecidable for RPNs. In this work, we introduce a submodel of RPNs called sequential recursive Petri nets (SRPNs) and we study its theoretical features. First we show that we can decide whether a RPN is a sequential one. Then, we analyze the language aspects proving that the SRPN languages still strictly include the union of Petri nets and context-free languages. Moreover the family of languages of SRPNs is closed under intersection with regular languages (unlike the one of RPNs). This property is the starting point for the model checking of the action-based linear time logic which is also shown to be decidable. To the best of our knowledge, this is the first time such a result is obtained for a model strictly including Petri nets and context-free grammars.

Mots-clés : Réseaux de Petri récursif, vérification de modèle et décidabilité

Key-words : Recursive Petri net, Model checking and decidability

Publications internes LIP6 2000 / LIP6 research reports 2000

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