Quantitative Verification of Probabilistic Transition Systems

The majority of the verification methods for concurrent systems only produce qualitative information. Questions like ``Does the system satisfy its specification?'' and ``Do the systems behave the same?'' are answered. The latter question boils down to ``Are the systems the same with respect to some behavioural equivalence?'' For concurrent systems bisimilarity is the key behavioural equivalence. For instance, the transition systems
are bisimilar.

Discrete probabilistic transition systems are considered to behave the same if they are probabilistic bisimilar. For example, the probabilistic transition systems

are probabilistic bisimilar. Recall that bisimilar states have equal probability of making a transition to any bisimilarity equivalence class of states.

For probabilistic systems qualitative information, like probabilistic bisimilarity, is often too restrictive in practice and a (complementary) quantitative approach to verification is needed. For instance, the probabilistic transition systems

are only probabilistic bisimilar if ε is 0. However, the two systems behave almost the same for very small ε different from 0. Behavioural equivalences like probabilistic bisimilarity are not robust, since they are too sensitive to the exact probabilities of the various transitions. Often the probabilities of the transitions are approximations themselves. For example, 1/π may be approximated by 0.32. Since the systems
are not probabilistic bisimilar, one cannot use the latter to reason about the former when using probabilistic bisimulations.

In a quantitative approach to verification, answers to questions like ``What is the probability that the system satisfies its specification?'' and ``Do the systems behave almost (up to some small fluctuations) the same?'' provide us with (often more useful) quantitative information about the systems. In my current research, the latter kind of questions are addressed.

The difference in behaviour of systems can be naturally captured by means of a pseudometric. It provides a quantitative notion of behavioural equivalence. A pseudometric differs from an ordinary metric in that different states may have distance 0. The distance between (initial) states of probabilistic transition systems, a real number between 0 and 1, expresses the similarity of the behaviour of the systems. The smaller the distance, the more alike the systems behave. Systems behave almost the same, up to ε-fluctuations, if their distance is at most ε. Furthermore, the distance between systems is 0 if they are indistinguishable, that is, they are probabilistic bisimilar.

This research is supported by the Natural Sciences and Research Council of Canada.


Talk at CONCUR 2001