When are Timed Automata weakly timed bisimilar to Time Petri Nets ?

Abstract : In this paper, we compare Timed Automata (TA) with Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is included in the class of TA. It is thus natural to try and identify the (strict) subclass $\taminus$ of TA that is equivalent to TPN for the weak time bisimulation relation. We give a characterisation of this subclass and we show that the membership problem and the reachability problem for $\taminus$ are $PSPACE$-complete. Furthermore we show that for a TA in $\taminus$ with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.
Type de document :
Communication dans un congrès
25th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05), Dec 2005, Chennai, India. pp.276--284, 2005
Liste complète des métadonnées

https://hal.inria.fr/inria-00368578
Contributeur : Franck Cassez <>
Soumis le : mardi 17 mars 2009 - 04:58:11
Dernière modification le : jeudi 15 mars 2018 - 14:28:03
Document(s) archivé(s) le : mardi 8 juin 2010 - 23:32:13

Fichier

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

Identifiants

  • HAL Id : inria-00368578, version 1

Citation

Béatrice Berard, Franck Cassez, Serge Haddad, Didier Lime, Olivier Henri Roux. When are Timed Automata weakly timed bisimilar to Time Petri Nets ?. 25th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'05), Dec 2005, Chennai, India. pp.276--284, 2005. 〈inria-00368578〉

Partager

Métriques

Consultations de la notice

318

Téléchargements de fichiers

96