Checking Linear Temporal Formulas on Sequential Recursive Petri Nets
Haddad, Serge; Poitrenaud, Denis (2001), Checking Linear Temporal Formulas on Sequential Recursive Petri Nets, Eighth International Symposium on Temporal Representation and Reasoning, 2001. TIME 2001. Proceedings., IEEE Computer Society, p. 198-205. http://dx.doi.org/10.1109/TIME.2001.930718
TypeCommunication / Conférence
Conference title8th International Symposium on Temporal Representation and Reasoning, TIME 2001
Conference cityCividale del Friuli
Book titleEighth International Symposium on Temporal Representation and Reasoning, 2001. TIME 2001. Proceedings.
MetadataShow full item record
Abstract (EN)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 paper, 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).
Subjects / KeywordsRecursive Petri nets
Showing items related by title and author.
Exploiting Partial Symmetries in Well-formed nets for the Reachability and the Linear Time Model Checking Problems Baarir, Souheib; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence