Equivalence of Timed State Machines and safe TPN

Stefan Haar (1) , Laurent Kaiser (2) , Françoise Simonot-Lion (2) , Joël Toussaint (3)

1 SIGMA2 - Signal, models, algorithms
2 TRIO - Real time and interoperability
3 LIMOS - Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes

In this article, we show that an important subclass of Timed Automata, called Timed Input Output State Machines (TIOSM) is weackly time equivalent to bounded non-Zeno Time Petri Nets (TPNs) in the sense of Merlin and Farber. We present here an explicit construction for two-way translation between 1-safe TPNs and TIOSMs; in both directions, the power of clock timing is exploited to obtain concise and analyzable models. || Dans cet article, nous montrons qu'une importante sous-classe d'automates temporisés, appelés Timed Input Output State Machines (TIOSM) est faiblement équivalente aux Réseaux de Petri temporels "non-Zeno" (TPN) (Merlin et Farber). Nous présentons ici une

Mots clés: automatic model translation; automates temporisés; bisimulation; verification; timed automata; time petri nets; réseaux de petri temporels; traduction automatique

Domaines: Autre [cs.OH]

Stefan Haar, Laurent Kaiser, Françoise Simonot-Lion, Joël Toussaint. Equivalence of Timed State Machines and safe TPN. 6th International Workshop on Discrete Event Systems - WODES'02, 2002, Zaragoza/Spain, Spain. pp.119-126. ⟨inria-00100864⟩