Skip to Main content Skip to Navigation
Journal articles

Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf

Abstract : For the formal verification of the concurrent or communicating dynamic systems modeled with Petri nets, the method of the unfolding is used to cope with the well-known problem of the state explosion. An extension of the method to the non safe time Petri nets is presented. The obtained unfolding is simply a prefix of that from the underlying ordinary Petri net to the time Petri net. For a certain class of time Petri nets, a finite prefix capturing the state space and the timed language ensues from the calculation of a finite set of finite processes with valid timings. The quantitative temporal constraints associated with these processes can serve to validate more effectively the temporal specifications of a hard real-time system.
Document type :
Journal articles
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01299417
Contributor : Coordination Episciences Iam <>
Submitted on : Thursday, April 7, 2016 - 4:12:14 PM
Last modification on : Tuesday, June 23, 2020 - 2:42:01 PM
Long-term archiving on: : Monday, November 14, 2016 - 9:13:28 PM

File

Vol.14.pp.185-203.pdf
Publisher files allowed on an open archive

Identifiers

  • HAL Id : hal-01299417, version 1

Collections

Citation

M. Sogbohossou, D. Delfieu. Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf. Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées, INRIA, 2011, 14, pp.185-203. ⟨hal-01299417⟩

Share

Metrics

Record views

192

Files downloads

992