Petri Nets – Theory and Applications. Cassez, F. & Roux, O. H. Petri Nets – Theory and Applications, pages 225–252. Advanced Robotic Systems, Vienna, Austria, 2008. Free download from ˘rlhttp://intechweb.org/books.php.
Paper abstract bibtex In this chapter we introduce a formalism, \emphTime Petri Nets (TPNs), to model real-time systems. We compare it with another well-known formalism, \emphTimed Automata (TA), used for specifying timed systems. We precisely define the semantics of TPNs and TA and compare them according to two criteria: the \emphlanguages (or set of behaviours) then can generate, and the \emphtrees (or branching behaviours) they can generate. We show that every TPN can be translated into an equivalent TA. Then, we introduce a real-time logic to specify properties of real-time systems. We show how to check that a given TPN satisfies a property written in this logic. For this we use our translation\footnoteThis translation preserves the properties of this logic. from TPNs to TA and check the property on the equivalent TA. Finally we briefly report on experiments for checking real-time properties of TPNs using this framework.
@INBOOK{ars-petri-nets,
AUTHOR = {Cassez, Franck and Roux, Olivier H.},
EDITOR = {Kordic, Vedran},
TITLE = {Petri Nets -- Theory and Applications},
CHAPTER = {From Time Petri Nets to Timed Automata},
PUBLISHER = ARS-VIENNA,
YEAR = {2008},
SERIES = {{I}-Tech {E}ducation {O}nline},
URL= {http://intechweb.org/books.php},
PAGES = {225--252},
PDF = {papers/tpn-book-08.pdf},
ISBN = {ISBN 978-3-902613-12-7},
NOTE={Free download from \url{http://intechweb.org/books.php}.},
ABSTRACT = {In this chapter we introduce a formalism, \emph{Time
Petri Nets (TPNs)}, to model real-time systems. We
compare it with another well-known formalism,
\emph{Timed Automata (TA)}, used for specifying
timed systems. We precisely define the semantics of
TPNs and TA and compare them according to two
criteria: the \emph{languages} (or set of
behaviours) then can generate, and the \emph{trees}
(or branching behaviours) they can generate. We
show that every TPN can be translated into an
equivalent TA. Then, we introduce a real-time logic
to specify properties of real-time systems. We show
how to check that a given TPN satisfies a property
written in this logic. For this we use our
translation\footnote{This translation preserves the
properties of this logic.} from TPNs to TA and check
the property on the equivalent TA. Finally we
briefly report on experiments for checking real-time
properties of TPNs using this framework. },
Type = {C - Book Chapters},
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 2007
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Downloads: 0
{"_id":"YRDjHuSfkRczgsTch","bibbaseid":"cassez-roux-petrinetstheoryandapplications-2008","author_short":["Cassez, F.","Roux, O. H."],"bibdata":{"bibtype":"inbook","type":"C - Book Chapters","author":[{"propositions":[],"lastnames":["Cassez"],"firstnames":["Franck"],"suffixes":[]},{"propositions":[],"lastnames":["Roux"],"firstnames":["Olivier","H."],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Kordic"],"firstnames":["Vedran"],"suffixes":[]}],"title":"Petri Nets – Theory and Applications","chapter":"From Time Petri Nets to Timed Automata","publisher":"Advanced Robotic Systems, Vienna, Austria","year":"2008","series":"I-Tech Education Online","url":"http://intechweb.org/books.php","pages":"225–252","pdf":"papers/tpn-book-08.pdf","isbn":"ISBN 978-3-902613-12-7","note":"Free download from ˘rlhttp://intechweb.org/books.php.","abstract":"In this chapter we introduce a formalism, \\emphTime Petri Nets (TPNs), to model real-time systems. We compare it with another well-known formalism, \\emphTimed Automata (TA), used for specifying timed systems. We precisely define the semantics of TPNs and TA and compare them according to two criteria: the \\emphlanguages (or set of behaviours) then can generate, and the \\emphtrees (or branching behaviours) they can generate. We show that every TPN can be translated into an equivalent TA. Then, we introduce a real-time logic to specify properties of real-time systems. We show how to check that a given TPN satisfies a property written in this logic. For this we use our translation\\footnoteThis translation preserves the properties of this logic. from TPNs to TA and check the property on the equivalent TA. Finally we briefly report on experiments for checking real-time properties of TPNs using this framework. ","bibtex":"@INBOOK{ars-petri-nets,\n AUTHOR = {Cassez, Franck and Roux, Olivier H.},\n EDITOR = {Kordic, Vedran},\n TITLE = {Petri Nets -- Theory and Applications},\n CHAPTER = {From Time Petri Nets to Timed Automata},\n PUBLISHER = ARS-VIENNA,\n YEAR = {2008},\n SERIES = {{I}-Tech {E}ducation {O}nline},\n URL= {http://intechweb.org/books.php},\n PAGES = {225--252},\n PDF = {papers/tpn-book-08.pdf},\n ISBN = {ISBN 978-3-902613-12-7},\nNOTE={Free download from \\url{http://intechweb.org/books.php}.},\n ABSTRACT = {In this chapter we introduce a formalism, \\emph{Time\n Petri Nets (TPNs)}, to model real-time systems. We\n compare it with another well-known formalism,\n \\emph{Timed Automata (TA)}, used for specifying\n timed systems. We precisely define the semantics of\n TPNs and TA and compare them according to two\n criteria: the \\emph{languages} (or set of\n behaviours) then can generate, and the \\emph{trees}\n (or branching behaviours) they can generate. We\n show that every TPN can be translated into an\n equivalent TA. Then, we introduce a real-time logic\n to specify properties of real-time systems. We show\n how to check that a given TPN satisfies a property\n written in this logic. For this we use our\n translation\\footnote{This translation preserves the\n properties of this logic.} from TPNs to TA and check\n the property on the equivalent TA. Finally we\n briefly report on experiments for checking real-time\n properties of TPNs using this framework. },\n Type = {C - Book Chapters},\n}\n\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n%%% 2007\n%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n\n\n","author_short":["Cassez, F.","Roux, O. H."],"editor_short":["Kordic, V."],"key":"ars-petri-nets","id":"ars-petri-nets","bibbaseid":"cassez-roux-petrinetstheoryandapplications-2008","role":"author","urls":{"Paper":"http://intechweb.org/books.php"},"metadata":{"authorlinks":{}}},"bibtype":"inbook","biburl":"http://science.mq.edu.au/~fcassez/bib/franck-bib.bib","dataSources":["8742EsvjQfyP2fYBW","qbqYFWskmoonRB43F","yYF8uwWqay28JyxZC"],"keywords":[],"search_terms":["petri","nets","theory","applications","cassez","roux"],"title":"Petri Nets – Theory and Applications","year":2008}