Close form derivation of state-density functions over DBM domains in the analysis of non-Markovian models

Quantitative evaluation of models allowing multiple concurrent non-exponential timers requires enumeration and analysis of non-Markovian processes. In general, these processes may be not isomorphic to those obtained from the corresponding untimed models, due to implicit precedences induced by timing constraints on concurrent events. The analysis of stochastic Time Petri Nets (sTPNs) copes with the problem by covering the state space with stochastic classes, which extend Difference Bounds Matrix (DBM) theory with a state density function providing a measure of probability for the variety of states collected within a class. In this paper, we extend the theory of stochastic classes providing a close form calculus for the derivation of the state density function under the assumption that all transitions have an expolynomial distribution. The characterization provides insight on how the form of the state density function evolves when transitions fire and the stochastic class accumulates memory and provide the basis for an efficient implementation which drastically reduces analysis complexity.