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

https://hal.inria.fr/hal-00876642
Contributor : Hervé Marchand <>
Submitted on : Friday, October 25, 2013 - 11:42:17 AM
Last modification on : Thursday, January 23, 2020 - 6:22:10 PM
Long-term archiving on: : Friday, April 7, 2017 - 5:40:30 PM

File

Avellaneda.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00876642, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

166

Files downloads

1640