Age semantics based state space computation of time Petri nets

This paper deals with time Petri nets while assuming multiple-server semantics. The latter has been proved to be more expressive than standard semantics (single-server). However, the state space of the model is more complex to compute in this case as it involves to consider many instances of a same enabled transition. This results in a high cost in terms of computation and memory usage. Within this context, we consider the token-age based multiple server semantics and provide an efficient algorithm to compute the state class graph of the model. For this effect, we represent the time constraints of a class by means of an alternative form that we call, the time distance system. The latter makes it possible to compact the representation of a class and to reduce its computation complexity. Quantitative properties of the model can be easily extracted without performing further computations.