Quantitative Verification

The majority of the verification methods for concurrent systems only produce qualitative information. Questions like ``Does the system satisfy a particular property?'' and ``Do the systems behave the same?'' are answered. However, for systems that depend on quantitative information such as time and probabilities, answers to these yes-no questions are of little value. Small changes to the quantitative information, which is often obtained experimentally and, hence, is just an approximation, may change the answer from yes to no or vice versa.

Behavioural Pseudometrics

Rather than answering yes or no to the question ``Do the systems behave the same?'', one can also use a real number in the interval [0, 1] as an answer. The smaller the number, the more alike the systems behave. Zero captures that the systems behave exactly the same. In collaboration with James Worrell (Oxford University), Franck van Breugel introduced such a quantitative notion of equivalence for probabilistic systems and coined the term behavioural pseudometric.

Approximation Algorithms

To determine the behavioural difference (or distance) of two probabilistic systems, graduate student Babita Sharma, James Worrell and Franck van Breugel developed algorithms that approximate the difference up to arbitrary precision.