It is widely acknowledged that problems detected early in the system development process are less expensive to fix than those detected later; for example, an IBM study estimates the cost of fixing an error after release is 100 times the cost of resolving an error in the design phase. Formal modelling and verification techniques can be used to detect errors or inefficiencies in the design phase, allowing us to thoroughly check and understand a system design before its construction. Model checking is an automatic verification method for determining whether the model of a system satisfies a specification, and has been applied in a wide variety of contexts, including safety-critical systems, robotics and system biology.
For many systems, it is important to represent faithfully aspects not only of the digital components but also of the continuous environment in which they are embedded. This has led to two major directions in model checking. The first is probabilistic model checking, in which the likelihood of system behaviour is modelled explicitly using formalisms such as Markov chains; using such methods, we may be able to determine, for example, that system errors can occur but do so with a sufficiently low probability. The second direction concerns model checking of systems with both discrete and continuous components, which are called hybrid systems: typical examples are systems with complex timed behaviour, systems controlling the ambient temperature of buildings, or autonomous robots.
We consider the combination of these two directions of model checking, to obtain methods for the verification of probabilistic hybrid systems. We give examples of formalisms for such systems and show how the degree of interaction between probabilistic and continuous aspects of the system is vital for the decidability of their associated model-checking methods.