Computing probabilities over DBM domains to integrate qualitative verification and quantitative evaluation of timed stochastic models

In the development of reactive systems with nondeterministic densely-valued temporal parameters, qualitative verification and quantitative evaluation play complementary roles, supporting the identification of feasible behaviors and their association with a measure of probability. Though inherently coupled in the application perspective, the two aspects yield contrasting needs that resulted in separate formalisms and techniques developed upon different theoretical grounds. We report the results of our research towards a unified approach of the two aspects based on the method of stochastic state classes, which extends state space analysis based on Difference Bounds Matrix zones (DBM) with the symbolic calculus of a density-function providing a measure for the probability of individual states. To this end, we extend Time Petri Nets by associating a general probability distribution to the static firing interval of each nondeterministic transition, and we explain how this stochastic information induces a probability distribution for the states contained within a DBM class and how this probability evolves in the enumeration of the reachability relation among classes. In particular, we show that the state-density function accepts a continuous piecewise representation over a partition in DBM-shaped subdomains, we develop a closed-form symbolic calculus of state-density functions under the assumption that transitions in the sTPN model have expolynomial distributions over possibly bounded intervals, and we provide an efficient approximation approach based on Bernstein Polynomials. % This enables the construction of a stochastic transition system that supports correctness verification based on the theory of TPNs, provides a measure of probability for each feasible run, enables steady-state analysis based on Markov Renewal Theory.