Skip to Main content Skip to Navigation
Documents associated with scientific events

Vérification de réseaux de Petri avec états sous une sémantique d'ordres partiels

Abstract : In order to study MSC specifications with counters, timers and other features, we introduce the model of Petri nets with states together with a non-branching non-sequential process semantics.We obtain a framework that is more expressive and more concise than MSGs.We consider then three classical verification problems for the set of markings reached by prefixes of processes: boundedness, covering and reachability. We show that each of these problems boils down to the equivalent problem for Petri nets. We consider also the notion of semi-structural property in order to study parametrized systems. In this way, only part of the places are provided with an initial marking. Unfolding such a system leads to a simpler problem in the form of a linear programme.
Document type :
Documents associated with scientific events
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Hervé Marchand Connect in order to contact the contributor
Submitted on : Friday, October 25, 2013 - 11:42:17 AM
Last modification on : Friday, October 22, 2021 - 3:33:26 AM
Long-term archiving on: : Friday, April 7, 2017 - 5:40:30 PM


Files produced by the author(s)


  • HAL Id : hal-00876642, version 1



Florent Avellaneda, Rémi Morin. Vérification de réseaux de Petri avec états sous une sémantique d'ordres partiels. MSR 2013 - Modélisation des Systèmes Réactifs, 2013, Rennes, France. ⟨hal-00876642⟩



Record views


Files downloads