Reduced Occurrence Graphs for Timed CPN via Equivalences

Thomas Mailund, Soren Christensen, and Lars Kristensen

Address

Abstract

History repeats itself. Time does not. Time progresses. The same event will never occur again at exactly the same time. For Timed Coloured Petri Nets (TCPN) this is reflected in the state space. A cyclic net is likely to have an infinite state space, even when the underlying un-timed net has a finite state space. All because of the progression of time.

In many cases, however, we are not really interested in "time" as such but rather interested in "delay". We use TCPN to model that certain events take a certain amount of time to complete, modelled in the way that the results of such events, i.e. the generated tokens, will not be available until after a certain delay. The actual time at which tokens become available is not important. Only the relative delay between one token and another becoming available matters.

We would like to be able to exploit this when generating occurrence graphs for timed nets. When history repeats itself, i.e., when we reach a state similar to a state we have already seen, where only the actual time differs, we would like to make a "loop" in the graph back to the earlier state. If only the delay of events matters for the behaviour of a net, clearly the same behaviour is expected to be repeated from this later point in time. Only time stamps will differ. For all intended purposes, the two states should be considered equal.

In our work we define an equivalence relation to formalise what we mean by two states being "similar" in this sense, and exploit the idea above to reduce the infinite O-graphs to finite OE-graphs, for a large class of TCPN. We also present a modified OE-graph extended with some time information, which can be used to re-calculate time information of the TCPN from the finite reduced OE-graph.

Keywords:

Timed CPN, Occurrence Graphs, Occurrence Graphs with Equivalences (OE-Graphs).