For the most recent entries see the Petri Nets Newsletter.

Comparison of the Expressiveness of Timed Automata and Time Petri Nets.

Berard, Beatrice; Cassez, Franck; Haddad, Serge; Lime, Didier; Roux, Olivier

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:,.

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography