Franck van Breugel - Towards quantitative verification of systems: a coalgebraic approach

The majority of the verification methods for software systems only produce qualitative information. Questions like ``Does the system satisfy the specification?'' and ``Are the systems semantically equivalent?'' are answered. However, this information is often too restrictive in practice and a (complementary) quantitative approach to verification is needed. For example, answers to questions like ``What is the probability that the system satisfies its specification?'' and ``Do the systems behave almost (up to some small time fluctuations, say of one millisecond) the same?'' provide us with (often more useful) quantitative information about the systems.

Metric spaces (and generalizations thereof) seem a good candidate for measuring the difference in behaviour of systems. The behaviour of many software systems can be described by means of coalgebras (of an endofunctor on the category of sets). For most systems, the endofunctor (on sets) associated to the coalgebra can be naturally extended to an endofunctor on metric spaces. This extended endofunctor having a terminal coalgebra is the key to the success of my approach to quantitative verification. The approach will be illustrated by considering restricted classes of real-time and probabilistic systems.