Using Stochastic State Classes in Quantitative Evaluation of Dense-Time Reactive Systems

In the verification of reactive systems with nondeterministic densely valued temporal parameters, the state-space can be covered through equivalence classes, each composed of a discrete logical location and a dense variety of clock valuations encoded as a difference bounds matrix (DBM). The reachability relation among such classes enables qualitative verification of properties pertaining events ordering and stimulus/response deadlines, but it does not provide any measure of probability for feasible behaviors. We extend DBM equivalence classes with a density-function which provides a measure for the probability of individual states. To this end, we extend time Petri nets by associating a probability density-function to the static firing interval of each nondeterministic transition. We then 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. This enables the construction of a stochastic transition system which 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. In so doing, we provide a means to identify feasible behaviors and to associate them with a measure of probability in models with multiple concurrent generally distributed nondeterministic timers.