Equivalence notions and refinement for timed Petri nets

The paper is contributed to develop a family of equivalence notions for real¬time systems represented by labelled Merlin’s time Petri nets with zero length time intervals (i.e., with fixed time delays). We call them “timed Petri nets”. In particular, we introduce timed (time-sensitive), untimed (time-abstracting) and region (based on the notion of region equivalences in both the trace and bisimulation semantics. The interrelations of all the equivalence notions are examined for a general class of timed nets as well as for a subclass of untimed nets (timed nets with time delays equal to zero’s). Further we define a timed variant of state-mashine refinement and investigate how the proposed equivalence notions behave with respect to this class of refinements.