State-density functions over DBM domains in the analysis of non-Markovian models

Quantitative evaluation of models with generally-distributed transitions requires analysis of non-Markovian processes that may be not isomorphic to their underlying untimed models and may include any number of concurrent non-exponential timers. The analysis of stochastic Time Petri Nets copes with the problem by covering the state space with stochastic-classes, which extend Difference Bounds Matrices (DBM) with a state probability density function. We show that the state-density function accepts a continuous piecewise representation over a partition in DBM-shaped sub-domains. We then develop a closed-form symbolic calculus of state-density functions assuming that model transitions have expolynomial distributions. The calculus shows that within each sub-domain the state-density function is a multivariate expolynomial function and makes explicit how this form evolves through subsequent transitions. This enables an efficient implementation of the analysis process and provides the formal basis that supports introduction of an approximate analysis based on Bernstein Polynomials. The approximation attacks practical and theoretical limits in the applicability of stochastic state-classes, and devises a new approach to the analysis of non Markovian models, relying on approximations in the state space rather than in the structure of the model.