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

B. Bérard*, F. Cassez, S. Haddad, D. Lime, O. H. Roux

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

16 Citations (Scopus)

Abstract

In this paper, we compare Timed Automata (TA) and Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is strictly included in the class of TA. It is thus natural to try and identify the subclass T Aw t b of TA equivalent to some TPN for the weak timed bisimulation relation. We give a characterization of this subclass and we show that the membership problem and the reachability problem for T Aw t b are P S P A C E-complete. Furthermore we show that for a TA in T Aw t b 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.

Original languageEnglish
Pages (from-to)202-220
Number of pages19
JournalTheoretical Computer Science
Volume403
Issue number2-3
DOIs
Publication statusPublished - 28 Aug 2008
Externally publishedYes

Keywords

  • Time Petri nets
  • Timed automata
  • Weak timed bisimilarity

Fingerprint

Dive into the research topics of 'When are Timed Automata weakly timed bisimilar to Time Petri Nets?'. Together they form a unique fingerprint.

Cite this