M. Sogbohossou ; D. Delfieu - Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf

arima:1950 - Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées, October 16, 2011, Volume 14 - 2011 - Special issue CARI'10 - https://doi.org/10.46298/arima.1950
Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf

Authors: M. Sogbohossou ; D. Delfieu

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.


Volume: Volume 14 - 2011 - Special issue CARI'10
Published on: October 16, 2011
Submitted on: March 24, 2011
Keywords: Time Petri nets, non safeness, timed unfolding, finite complete prefix, time processes, hard real-time systems.,Réseaux de Petri temporels,caractère non sauf,dépliage temporel,préfixe complet fini,processus temporisés,systèmes temps réel durs.,[MATH] Mathematics [math],[INFO] Computer Science [cs]


Share

Consultation statistics

This page has been seen 79 times.
This article's PDF has been downloaded 97 times.