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
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.