In: 06, 2006: Proceedings of the Fourth International Workshop on Modelling of Objects, Components and Agents, MOCA'06, Bericht 272, FBI-HH-B-272, pages 223-244. June 06.
Abstract: This paper aims at extending modular state space analysis to time Petri nets. The basic model is time Petri nets, where the timing is a firing interval attached to each transition. They are here extended to allow for modules. A state is composed by both a marking and a clock valuation function. The state spaces of time Petri nets are in general infinite even if the net is bounded, because the transitions fire in a continuous time domain. For the analysis some techniques are necessary to reduce the state space to a finite one. In this paper, we consider state spaces obtained by restricting the behaviour of time Petri nets so that transitions fire only at integer times. A modular version of such a graph is proposed as well as an algorithm for its construction.