The expressive power of time Petri nets. Bérard, B., Cassez, F., Haddad, S., Lime, D., & Roux, O. H. Theoretical Computer Science, 474:1-20, 2013.
Paper doi abstract bibtex We investigate expressiveness questions for time Petri nets (TPNs) and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs) as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs. We give a syntactical translation from bounded GTPNs to timed automata (TA) that generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l ess expressive than TA w.r.t. weak timed bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance. Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs "á la Merlin" w.r.t. weak timed bisimilarity. These results provide a unified comparison of the expressiveness of many variants of timed models often used in practice. It leads to new important results for TPNs. Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; $ε$-transitions strictly increase the expressive power of TPNs; self modifying nets as well as read, inhibitor and reset arcs do not add expressiveness to bounded TPNs.
@article{tpn-13,
author = {Béatrice Bérard and
Franck Cassez and
Serge Haddad and
Didier Lime and
Olivier H. Roux},
title = {The expressive power of time {Petri} nets},
journal = {Theoretical Computer Science},
Type = {A - Journal},
volume = {474},
year = {2013},
pages = {1-20},
doi = {http://dx.doi.org/10.1016/j.tcs.2012.12.005},
bibsource = {DBLP, http://dblp.uni-trier.de},
category= {Timed Petri nets},
mywebpage = {timed},
keywords = {time petri nets, timed automata},
urlpaper = {papers/tcs-2013.pdf},
abstract = {We investigate expressiveness questions for time Petri nets (TPNs)
and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs)
as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs.
We give a syntactical translation from bounded GTPNs to timed automata (TA)
that generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l
ess expressive than TA w.r.t. weak timed bisimilarity.
We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance.
Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs "á la Merlin" w.r.t.
weak timed bisimilarity. These results provide a unified comparison of the expressiveness of
many variants of timed models often used in practice. It leads to new important results for TPNs.
Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; $\epsilon$-transitions strictly
increase the expressive power of TPNs; self modifying nets as well as read,
inhibitor and reset arcs do not add expressiveness to bounded TPNs.
}
}
Downloads: 0
{"_id":"BYDnREoWzJCrXuSrG","bibbaseid":"brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013","author_short":["Bérard, B.","Cassez, F.","Haddad, S.","Lime, D.","Roux, O. H."],"bibdata":{"bibtype":"article","type":"A - Journal","author":[{"firstnames":["Béatrice"],"propositions":[],"lastnames":["Bérard"],"suffixes":[]},{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]},{"firstnames":["Serge"],"propositions":[],"lastnames":["Haddad"],"suffixes":[]},{"firstnames":["Didier"],"propositions":[],"lastnames":["Lime"],"suffixes":[]},{"firstnames":["Olivier","H."],"propositions":[],"lastnames":["Roux"],"suffixes":[]}],"title":"The expressive power of time Petri nets","journal":"Theoretical Computer Science","volume":"474","year":"2013","pages":"1-20","doi":"http://dx.doi.org/10.1016/j.tcs.2012.12.005","bibsource":"DBLP, http://dblp.uni-trier.de","category":"Timed Petri nets","mywebpage":"timed","keywords":"time petri nets, timed automata","urlpaper":"papers/tcs-2013.pdf","abstract":"We investigate expressiveness questions for time Petri nets (TPNs) and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs) as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs. We give a syntactical translation from bounded GTPNs to timed automata (TA) that generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l ess expressive than TA w.r.t. weak timed bisimilarity. We prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance. Finally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs \"á la Merlin\" w.r.t. weak timed bisimilarity. These results provide a unified comparison of the expressiveness of many variants of timed models often used in practice. It leads to new important results for TPNs. Among them are: 1-safe TPNs and bounded-TPNs are equally expressive; $ε$-transitions strictly increase the expressive power of TPNs; self modifying nets as well as read, inhibitor and reset arcs do not add expressiveness to bounded TPNs. ","bibtex":"@article{tpn-13,\n author = {Béatrice Bérard and\n Franck Cassez and\n Serge Haddad and\n Didier Lime and\n Olivier H. Roux},\n title = {The expressive power of time {Petri} nets},\n journal = {Theoretical Computer Science},\n Type = {A - Journal},\n volume = {474},\n year = {2013},\n pages = {1-20},\n doi = {http://dx.doi.org/10.1016/j.tcs.2012.12.005},\n bibsource = {DBLP, http://dblp.uni-trier.de},\n category= {Timed Petri nets},\n mywebpage = {timed},\n keywords = {time petri nets, timed automata},\n urlpaper = {papers/tcs-2013.pdf},\n abstract = {We investigate expressiveness questions for time Petri nets (TPNs)\n and some of their most useful extensions. We first introduce generalised time Petri nets (GTPNs)\n as an abstract model that encompasses variants of TPNs such as self modifications and read, reset and inhibitor arcs.\nWe give a syntactical translation from bounded GTPNs to timed automata (TA)\nthat generates isomorphic transition systems. We prove that the class of bounded GTPNs is strictly l\ness expressive than TA w.r.t. weak timed bisimilarity.\nWe prove that bounded GTPNs, bounded TPNs and TA are equally expressive w.r.t. timed language acceptance.\nFinally, we characterise a syntactical subclass of TA that is equally expressive to bounded GTPNs \"á la Merlin\" w.r.t.\nweak timed bisimilarity. These results provide a unified comparison of the expressiveness of\nmany variants of timed models often used in practice. It leads to new important results for TPNs.\nAmong them are: 1-safe TPNs and bounded-TPNs are equally expressive; $\\epsilon$-transitions strictly\nincrease the expressive power of TPNs; self modifying nets as well as read,\ninhibitor and reset arcs do not add expressiveness to bounded TPNs.\n}\n}\n\n\n","author_short":["Bérard, B.","Cassez, F.","Haddad, S.","Lime, D.","Roux, O. H."],"key":"tpn-13","id":"tpn-13","bibbaseid":"brard-cassez-haddad-lime-roux-theexpressivepoweroftimepetrinets-2013","role":"author","urls":{"Paper":"http://science.mq.edu.au/~fcassez/bib/papers/tcs-2013.pdf"},"keyword":["time petri nets","timed automata"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":["time petri nets","timed automata"],"search_terms":["expressive","power","time","petri","nets","bérard","cassez","haddad","lime","roux"],"title":"The expressive power of time Petri nets","year":2013}