In: Valette, R.: Lecture Notes in Computer Science, Vol. 815; Application and Theory of Petri Nets 1994, Proceedings 15th International Conference, Zaragoza, Spain, pages 79-98. Springer-Verlag, 1994.
Abstract: We present an approach to construct the occurrenc e graph for ITCPN (Interval Timed Coloured Petri Nets). These models, defined by van der Aalst can simulate other timed Petri nets and allow to describe large and complex real-time systems. We define classes as sets of states between two occurrences, and we use these classes to define the occurrenc e graph of an ITCPN. Then an equivalence relation based on time is defined for classes, and we show that occurrence graphs reduced using this equivalence relation are finite if and only if the set of reachable markings is finite. These graphs can be used to verify all the dynamic properties such as reachability, boundedness, home, liveness and fairness properties but also performance properties: minimal and maximal bounds along an occurrence sequence or a cycle. Finally we complete delay based equivalence with a colour based equivalence in order to achieve further reduction