Loading...
Please wait, while we are loading the content...
Similar Documents
On Equivalence between Timed State Machines and Time Petri Nets
| Content Provider | Hyper Articles en Ligne (HAL) |
|---|---|
| Author | Haar, Stefan Kaiser, Laurent Simonot-Lion, Françoise Toussaint, Joël |
| Abstract | 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. |
| Related Links | https://inria.hal.science/inria-00072589/file/RR-4049.pdf |
| Language | English |
| Publisher | HAL CCSD |
| Publisher Date | 2000-01-01 |
| Access Restriction | Open |
| Subject Keyword | TIME PETRI NETS REAL TIME SYSTEMS TEST GENERATION VERIFICATION TIMED AUTOMATA |
| Content Type | Text |
| Resource Type | Report |
| Subject | Computer Science |
