LIP6 2000/024

• Reports
  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 - 09/12/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
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.
• Keywords : Recursive Petri net, Model checking and decidability
• Publisher : Denis.Poitrenaud (at) nulllip6.fr