Petri nets with may/must semantics: Preserving properties through data refinements

O. Kouchnarenko, N. Sidorova, N. Trcka

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

77 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings 18th Workshop on Concurrency and Specification (CS&P'09, Kraków-Przegorzaly, Poland, September 28-30, 2009)
EditorsL. Czaja
Place of PublicationWarsaw
PublisherInstitute of Informatics, Warsaw University
Publication statusPublished - 2009


Dive into the research topics of 'Petri nets with may/must semantics: Preserving properties through data refinements'. Together they form a unique fingerprint.

Cite this