Nested-unit Petri nets

Hubert Garavel 1, 2
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Petri nets can express concurrency and nondeterminism but neither locality nor hierarchy. This article presents an extension of Petri nets, in which places can be grouped into so-called "units" expressing sequential components. Units can be recursively nested to reflect both the concurrent and hierarchical nature of complex systems. This model called NUPN (Nested-Unit Petri Nets) was originally developed for translating process calculi to Petri nets, but later found also useful beyond this setting. It allows significant savings in the memory representation of markings for both explicit-state and symbolic verification. Thirteen software tools already implement the NUPN model, which has also been adopted for the benchmarks of the Model Checking Contest (MCC) and the parallel problems of the Rigorous Examination of Reactive Systems (RERS) challenges.
Complete list of metadatas

Cited literature [130 references]  Display  Hide  Download

https://hal.inria.fr/hal-02072190
Contributor : Hubert Garavel <>
Submitted on : Tuesday, March 19, 2019 - 8:13:07 AM
Last modification on : Tuesday, April 2, 2019 - 2:03:10 AM
Long-term archiving on : Thursday, June 20, 2019 - 12:54:26 PM

File

Garavel-19.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Hubert Garavel. Nested-unit Petri nets. Journal of Logical and Algebraic Methods in Programming, Elsevier, 2019, 104, pp.60-85. ⟨10.1016/j.jlamp.2018.11.005⟩. ⟨hal-02072190⟩

Share

Metrics

Record views

100

Files downloads

119