When Are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?

When Are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?. Bérard, B., Cassez, F., Haddad, S., Lime, D., & Roux, O. H. In Ramanujam, R. & Sen, S., editors, FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Hyderabad, India, December 15-18, 2005, Proceedings, volume 3821, of Lecture Notes in Computer Science, pages 273–284, 2005. Springer.

Paper

When Are Timed Automata Weakly Timed Bisimilar to Time Petri Nets? [link]

Link doi abstract bibtex

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 T 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 T are PSPACE-complete. Furthermore we show that for a TA in T 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.

@inproceedings{DBLP:conf/fsttcs/BerardCHLR05,
  author    = {B{\'{e}}atrice B{\'{e}}rard and
               Franck Cassez and
               Serge Haddad and
               Didier Lime and
               Olivier H. Roux},
        Type = {B - International Conferences},

  title     = {When Are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?},
  booktitle = {{FSTTCS} 2005: Foundations of Software Technology and Theoretical
               Computer Science, 25th International Conference, Hyderabad, India,
               December 15-18, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3821},
  publisher = {Springer},
  editor    = {Ramaswamy Ramanujam and
               Sandeep Sen},
  pages     = {273--284},
  year      = {2005},
  urlpaper = {papers/petri-nets-fsttcs05.pdf},
  url_link       = {http://dx.doi.org/10.1007/11590156_22},
  doi       = {10.1007/11590156_22},
  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 T  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 T  are PSPACE-complete. Furthermore we show that for a TA in T  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.},
  keywords = {Petri nets, timed automata, bisimulation},
}

Downloads: 0