In: Paul Pettersson, Wang Yi (Eds.): Lecture Notes in Computer Science, 3829: Formal Modeling and Analysis of Timed Systems: Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005., pages 211-225. Springer-Verlag, November 2005. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1160300917,.
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 [...] s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to [...]. 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 [...] 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 [...], bounded and 1-safe TPNs "à la Merlin" are equally expressive w.r.t. timed bisimilarity.
Keywords: Timed Language, Timed Bisimilarity, Time Petri Nets, Timed Automata, Expressiveness.