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

  • 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.


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]

Consultation statistics

This page has been seen 281 times.
This article's PDF has been downloaded 391 times.