HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Petri Nets with May/Must Semantics

Olga Kouchnarenko 1 Natalia Sidorova Nikola Trcka
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Many systems used in process managements, like workflow systems, are developed in a top-down fashion, when the original design is refined at each step bringing it closer to the underlying reality. Underdefined specifications cannot however be used for verification, since both false positives and false negatives can be reported. In this paper we introduce colored Petri nets where guards can be evaluated to true, false and indefinite values, the last ones reflecting underspecification. This results in the semantics of Petri nets with may- and must-enableness and firings. In this framework we introduce property-preserving refinements that allow for verification in an early design phase. We present results on property preservation through refinements. We also apply our framework to workflow nets, introduce notions of may- and must-soundness and show that they are preserved through refinements. We shortly describe a prototype under implementation.
Document type :
Conference papers
Complete list of metadata

Contributor : Olga Kouchnarenko Connect in order to contact the contributor
Submitted on : Wednesday, October 28, 2009 - 10:23:13 AM
Last modification on : Friday, January 21, 2022 - 3:09:01 AM


  • HAL Id : inria-00426835, version 1


Olga Kouchnarenko, Natalia Sidorova, Nikola Trcka. Petri Nets with May/Must Semantics. Workshop on Concurrency, Specification, and Programming - CS&P 2009, Humboldt University, Sep 2009, Kraków-Przegorzały, Poland. ⟨inria-00426835⟩



Record views