Skip to Main content Skip to Navigation
Reports

Proposal for Adding Useful Features to Petri-Net Model Checkers

Hubert Garavel 1
1 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Solutions proposed for the longstanding problem of automatic decomposition of Petri nets into concurrent processes, as well as methods developed in Grenoble for the automatic conversion of safe Petri nets to NUPNs (Nested-Unit Petri Nets), require certain properties to be computed on Petri nets. We notice that, although these properties are theoretically interesting and practically useful, they are not currently implemented in mainstream Petri net tools. Taking into account such properties would open fruitful research directions for tool developers, and new perspectives for the Model Checking Contest as well.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/hal-03087421
Contributor : Hubert Garavel <>
Submitted on : Wednesday, December 23, 2020 - 7:13:39 PM
Last modification on : Thursday, January 14, 2021 - 3:17:36 AM

Identifiers

  • HAL Id : hal-03087421, version 1
  • ARXIV : 2101.05024

Collections

Citation

Hubert Garavel. Proposal for Adding Useful Features to Petri-Net Model Checkers. [Research Report] Inria Grenoble - Rhône-Alpes. 2020. ⟨hal-03087421⟩

Share

Metrics

Record views

40

Files downloads

127