We present two recently developed state space methods for timed Petri nets. The two methods reconciles state space methods and time concepts based on the introduction of a global clock and associating time stamps to tokens. The first method is based on an equivalence relation on states which makes it possible to condense the usually infinite state space of a timed Petri net into a finite condensed state space without loosing analysis power. The second method supports on-the-fly verification of certain safety properties of timed systems. We discuss the application of the two methods in a number of different areas.
Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based Systems: Dfg Research Group "petri Net Technology", 2001, p. 33-42
Main Research Area:
Colloquium on Petri Net Technologies for Modeling Communication Based Systems, 2001