The majority of the verification methods for software systems only produce qualitative information. Questions like Does the system satisfy the specification?'' andAre 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?'' andDo 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 a restricted class of probabilistic systems.