In: 2nd International Conference on the Quantitative Evaluation of Systems (QEST), pages 13-22. 2005.
Abstract: Several techniques have been proposed for symbolic enumeration and analysis of the state space of reactive systems with non-deterministic temporal parameters taking values within a dense domain. In a large part of these techniques, the state space is covered by collecting states within equivalence classes each comprised 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 the ordering of events along critical runs and the satisfaction of stimulus/response deadlines. However, up to now, no results have been proposed which extend state class enumeration so as to combine the verification of the possibility of critical behaviors with a quantitative evaluation of their probability. In this paper, we extend the concept of equivalence classes based on DBM encoding with a density function which provides a measure for the probability associated with individual states collected in the class itself. To this end, we extend the formalism of Time Petri Nets by associating the static firing interval of each transition with a probability density function. We then expound how this probabilistic information determines a probability for the states collected within a class and how this probability evolves in the enumeration of the reachability relation among state classes. This opens the way to characterizing the possibility of critical behaviors with a quantitative measure of probability.
Keywords: Real-time reactive systems; correctness verification; performance evaluation; Time Petri nets.