Welcome to DiSC 2002
SIGMOD 2001
PODS 2001
SIGMOD RECORD 2001
CIKM 2001
CoopIS 2001
DASFAA 2001
DASFAA 2000
DBPL 2001
Data Engineering Bul
DEXA_EC-WEB 2001
DMKD 2001
DPDJ 2001
HYPERTEXT 2001
ICDE 2001
ICDM 2001
ICDT 2001
JCDL 2001
KDD 2001
KDD_EXPLORATIONS 20
KRDB 2001
MDM 2001
MIR 2001
MIS 2001
RIDE 2001
SBBD 2001
SIGIR 2001
SIGIR FORUM 2001
SSDBM 2001
SSTD 2001
TODS 2001
TIME 2001
= TIME'01 Website
<<< = TIME'01 papers>>>
VLDB 2001
VLDBJ 2001

Checking Linear Temporal Formulas on Sequential Recursive Petri Nets


Serge Haddad and Denis Poitrenaud

  View Paper (PDF)  

Return to Regular Papers 3


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 the model checking of the action-based linear time logic on SRPNs. We prove that it is decidable for all its variants : finite sequences, finite maximal sequences, infinite sequences and divergent sequences. At the end, we analyze language aspects proving that the SRPN languages still strictly include the union of Petri nets and context-free languages and that the family of languages of SRPNs is closed under intersection with regular languages (unlike the one of RPNs).


DiSC'02 © 2003 Association for Computing Machinery