When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?. Bérard, B., Cassez, F., Haddad, S., Lime, D., & Roux, O. H. Theoretical Computer Science, 403(2–3):202–220, Elsevier, 2008.
Paper abstract bibtex 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 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 are PSPACE-complete. Furthermore we show that for a TA in this class 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.
@article{BCHLR08-tcs,
AUTHOR = {B{\'e}rard, B{\'e}atrice and Franck Cassez and Haddad, Serge and Lime, Didier and Roux, Olivier H.},
JOURNAL = {Theoretical Computer Science},
PUBLISHER = {Elsevier},
VOLUME = 403,
NUMBER = {2--3},
PAGES = {202--220},
Type = {A - Journal},
TITLE = {When are Timed Automata Weakly Timed Bisimilar to Time {P}etri Nets?},
YEAR = {2008},
urlpaper = {papers/tcs-2008.pdf},
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 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 are PSPACE-complete. Furthermore we show that for a TA in this class 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.}
}
Downloads: 0
{"_id":"bkaKobrccKqmTBEvj","bibbaseid":"brard-cassez-haddad-lime-roux-whenaretimedautomataweaklytimedbisimilartotimepetrinets-2008","author_short":["Bérard, B.","Cassez, F.","Haddad, S.","Lime, D.","Roux, O. H."],"bibdata":{"bibtype":"article","type":"A - Journal","author":[{"propositions":[],"lastnames":["Bérard"],"firstnames":["Béatrice"],"suffixes":[]},{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"propositions":[],"lastnames":["Haddad"],"firstnames":["Serge"],"suffixes":[]},{"propositions":[],"lastnames":["Lime"],"firstnames":["Didier"],"suffixes":[]},{"propositions":[],"lastnames":["Roux"],"firstnames":["Olivier","H."],"suffixes":[]}],"journal":"Theoretical Computer Science","publisher":"Elsevier","volume":"403","number":"2–3","pages":"202–220","title":"When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?","year":"2008","urlpaper":"papers/tcs-2008.pdf","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 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 are PSPACE-complete. Furthermore we show that for a TA in this class 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.","bibtex":"@article{BCHLR08-tcs,\n AUTHOR = {B{\\'e}rard, B{\\'e}atrice and Franck Cassez and Haddad, Serge and Lime, Didier and Roux, Olivier H.},\n JOURNAL = {Theoretical Computer Science},\n PUBLISHER = {Elsevier},\n VOLUME = 403,\n NUMBER = {2--3},\n PAGES = {202--220},\n Type = {A - Journal},\n\n TITLE = {When are Timed Automata Weakly Timed Bisimilar to Time {P}etri Nets?},\n YEAR = {2008},\n urlpaper = {papers/tcs-2008.pdf},\n 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 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 are PSPACE-complete. Furthermore we show that for a TA in this class 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.}\n}\n\n\n","author_short":["Bérard, B.","Cassez, F.","Haddad, S.","Lime, D.","Roux, O. H."],"key":"BCHLR08-tcs","id":"BCHLR08-tcs","bibbaseid":"brard-cassez-haddad-lime-roux-whenaretimedautomataweaklytimedbisimilartotimepetrinets-2008","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/tcs-2008.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":[],"search_terms":["timed","automata","weakly","timed","bisimilar","time","petri","nets","bérard","cassez","haddad","lime","roux"],"title":"When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?","year":2008}