Comparison of the Expressiveness of Timed Automata and Time Petri Nets

Béatrice Berard 1, 2 Franck Cassez 3, 4 Serge Haddad 2, 5 Didier Lime 3 Olivier Henri Roux 3
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
2 LAMSADE - Laboratoire d'analyse et modélisation de systèmes pour l'aide à la décision
3 IRCCyN - Institut de Recherche en Communications et en Cybernétique de Nantes
4 NICTA - National ICT Australia [Sydney]
5 LSV - Laboratoire Spécification et Vérification [Cachan]
Abstract : In this paper we consider the model of Time Petri Nets (TPN) where time is associated with transitions. We also consider Timed Automata (TA) as defined by Alur \& Dill, and compare the expressive- ness of the two models w.r.t. timed language acceptance and (weak) timed bisimilarity. We first prove that there exists a TA A s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to A. We then propose a structural translation from TA to (1-safe) TPNs preserv- ing timed language acceptance. Further on, we prove that the previous (slightly extended) translation also preserves weak timed bisimilarity for a syntactical subclass $T_{Asyn}(\leq,\geq)$ of TA. For the theory of TPNs, the consequences are: 1) TA, bounded TPNs and 1-safe TPNs are equally expressive w.r.t. timed language acceptance; 2) TA are strictly more expressive than bounded TPNs w.r.t. timed bisimilarity; 3) The subclass $T_{Asyn}(\leq,\geq)$, bounded and 1-safe TPNs ''`a la Merlin'' are equally ex- pressive w.r.t. timed bisimilarity.
Type de document :
Communication dans un congrès
FORMATS 2005 - 3rd International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2005, Uppsala, Sweden. Springer-Verlag, 3829, pp.211-225, 2005, Lecture Notes in Computer Science. 〈10.1007/11603009_17〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00368577
Contributeur : Franck Cassez <>
Soumis le : mardi 17 mars 2009 - 04:53:30
Dernière modification le : vendredi 31 août 2018 - 09:25:57
Document(s) archivé(s) le : mardi 8 juin 2010 - 21:36:00

Fichiers

petri-nets-formats05.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

IRCCYN-MEFORBIO | UNIV-NANTES | IRCCYN | UNAM | UPMC | LIP6 | ENS-CACHAN | PSL

Citation

Béatrice Berard, Franck Cassez, Serge Haddad, Didier Lime, Olivier Henri Roux. Comparison of the Expressiveness of Timed Automata and Time Petri Nets. FORMATS 2005 - 3rd International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2005, Uppsala, Sweden. Springer-Verlag, 3829, pp.211-225, 2005, Lecture Notes in Computer Science. 〈10.1007/11603009_17〉. 〈inria-00368577〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

458

Téléchargements de fichiers

175

Contact


archive-ouverte@inria.fr