M. Sogbohossou ; D. Delfieu
-
Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf
arima:1950 -
Revue Africaine de 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 saufArticle
Authors: M. Sogbohossou 1; D. Delfieu 2
NULL##NULL
M. Sogbohossou;D. Delfieu
1 Laboratoire d'Electrotechnique, de Télécommunication et d'Informatique Appliquée
2 Institut de Recherche en Communications et en Cybernétique de Nantes
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.
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]