Comparison of the expressiveness of timed automata and time Petri nets

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

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 proceeding › Conference proceeding contribution › peer-review

72 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 TA_syn(≤, ≥) 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 language	English
Title of host publication	Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings
Place of Publication	Heidelberg
Publisher	Springer, Springer Nature
Pages	211-225
Number of pages	15
Volume	3829 LNCS
ISBN (Print)	3540309462, 9783540309468
Publication status	Published - 2005
Externally published	Yes
Event	3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005 - Uppsala, Sweden Duration: 26 Sep 2005 → 28 Sep 2005

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3829 LNCS
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Other

Other	3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005
Country/Territory	Sweden
City	Uppsala
Period	26/09/05 → 28/09/05

Keywords

Expressiveness
Time Petri Nets
Timed Automata
Timed Bisimilarity
Timed Language

Cite this

Bérard, B., Cassez, F., Haddad, S., Lime, D., & Roux, O. H. (2005). Comparison of the expressiveness of timed automata and time Petri nets. In Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings (Vol. 3829 LNCS, pp. 211-225). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3829 LNCS). Springer, Springer Nature.

Bérard, Beatrice ; Cassez, Franck ; Haddad, Serge ; Lime, Didier ; Roux, Olivier H. / Comparison of the expressiveness of timed automata and time Petri nets. Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings. Vol. 3829 LNCS Heidelberg : Springer, Springer Nature, 2005. pp. 211-225 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{fc9562b84ffa4f53bc1303e42d0a4fdf,

title = "Comparison of the expressiveness of timed automata and time Petri nets",

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 {"}{\`a} la Merlin{"} are equally expressive w.r.t. timed bisimilarity.",

keywords = "Expressiveness, Time Petri Nets, Timed Automata, Timed Bisimilarity, Timed Language",

author = "Beatrice B{\'e}rard and Franck Cassez and Serge Haddad and Didier Lime and Roux, {Olivier H.}",

year = "2005",

language = "English",

isbn = "3540309462",

volume = "3829 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Springer Nature",

pages = "211--225",

booktitle = "Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings",

address = "United States",

note = "3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005 ; Conference date: 26-09-2005 Through 28-09-2005",

}

Bérard, B, Cassez, F, Haddad, S, Lime, D & Roux, OH 2005, Comparison of the expressiveness of timed automata and time Petri nets. in Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings. vol. 3829 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3829 LNCS, Springer, Springer Nature, Heidelberg, pp. 211-225, 3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005, Uppsala, Sweden, 26/09/05.

Comparison of the expressiveness of timed automata and time Petri nets. / Bérard, Beatrice; Cassez, Franck; Haddad, Serge; Lime, Didier; Roux, Olivier H.

Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings. Vol. 3829 LNCS Heidelberg : Springer, Springer Nature, 2005. p. 211-225 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3829 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Comparison of the expressiveness of timed automata and time Petri nets

AU - Bérard, Beatrice

AU - Cassez, Franck

AU - Haddad, Serge

AU - Lime, Didier

AU - Roux, Olivier H.

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

KW - Expressiveness

KW - Time Petri Nets

KW - Timed Automata

KW - Timed Bisimilarity

KW - Timed Language

UR - http://www.scopus.com/inward/record.url?scp=33745442289&partnerID=8YFLogxK

M3 - Conference proceeding contribution

AN - SCOPUS:33745442289

SN - 3540309462

SN - 9783540309468

VL - 3829 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 211

EP - 225

BT - Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings

PB - Springer, Springer Nature

CY - Heidelberg

T2 - 3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005

Y2 - 26 September 2005 through 28 September 2005

ER -

Bérard B, Cassez F, Haddad S, Lime D, Roux OH. Comparison of the expressiveness of timed automata and time Petri nets. In Formal Modeling and Analysis of Timed Systems - Third International Conference, FORMATS 2005, Proceedings. Vol. 3829 LNCS. Heidelberg: Springer, Springer Nature. 2005. p. 211-225. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Comparison of the expressiveness of timed automata and time Petri nets

Abstract

Publication series

Other

Keywords

Other files and links

Fingerprint

Cite this