On Equivalence between Timed State Machines and Time Petri Nets - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2000

On Equivalence between Timed State Machines and Time Petri Nets

Stefan Haar
Laurent Kaiser
  • Fonction : Auteur
  • PersonId : 756519
  • IdRef : 083946241
Joël Toussaint
  • Fonction : Auteur
  • PersonId : 756520
  • IdRef : 076329461

Résumé

In this article, we identify a subclass of Timed Automata (Alur and Dill \citeAlurDill: [1], called Timed State Machines as weakly equivalent w.r.t. strongly timed behavior to a canonical class of Time Petri Nets (TPNs) in the sense of Merlin and Farber [17]; more precisely, the weak equivalence holds for bounded non-Zeno TPN with self-concurrency 1, denoted N1TPN. TSMs, and in particular message synchronized products, called TIOSMs, are mainly used for test generation; on the other hand, there is a rich literature on TPNs in verification. Hence our motivation to combine the strengths of both models. We present here an explicit construction for two - way translation between 1-TPNs and TSMs; in both directions, the power of clock timing is exploited to obtain concise and analyzable models. The TSM model obtained from the translation has a state set the size of the reachability graph; it thus improves on the class graph obtained by the enumerative method [3],[2]. The existence of the translation procedure, which has also been implemented in a tool prototype, XTIOSM, makes the model equivalence effective.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-4049.pdf (318.45 Ko) Télécharger le fichier

Dates et versions

inria-00072589 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00072589 , version 1

Citer

Stefan Haar, Laurent Kaiser, Françoise Simonot-Lion, Joël Toussaint. On Equivalence between Timed State Machines and Time Petri Nets. [Research Report] RR-4049, INRIA. 2000. ⟨inria-00072589⟩
100 Consultations
219 Téléchargements

Partager

Gmail Facebook X LinkedIn More