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.
Petri Nets – Theory and Applications [link]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