Comparison of the expressiveness of timed automata and time Petri nets

Beatrice Bérard*, Franck Cassez, Serge Haddad, Didier Lime, Olivier H. Roux

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

69 Citations (Scopus)

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 expressiveness 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 preserving timed language acceptance. Further on, we prove that the previous (slightly extended) translation also preserves weak timed bisimilarity for a syntactical subclass TAsyn(≤, ≥) 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 TA syn(≤,≥), bounded and 1-safe TPNs "à la Merlin" are equally expressive w.r.t. timed bisimilarity.

Original languageEnglish
Title of host publicationFormal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings
Place of PublicationHeidelberg
PublisherSpringer, Springer Nature
Pages211-225
Number of pages15
Volume3829 LNCS
ISBN (Print)3540309462, 9783540309468
Publication statusPublished - 2005
Externally publishedYes
Event3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005 - Uppsala, Sweden
Duration: 26 Sep 200528 Sep 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3829 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005
CountrySweden
CityUppsala
Period26/09/0528/09/05

Keywords

  • Expressiveness
  • Time Petri Nets
  • Timed Automata
  • Timed Bisimilarity
  • Timed Language

Fingerprint Dive into the research topics of 'Comparison of the expressiveness of timed automata and time Petri nets'. Together they form a unique fingerprint.

Cite this