Linear hybrid automata are of interest in verification because sets of successor states can be computed exactly and efficiently using integer arithmetic. This fact is exploited in a number of formal verification algorithms that upon termination give a mathematically sound answer on whether a property holds or not. This chapter gives an overview of verification algorithms for safety properties of linear hybrid automata, and some of the over-approximation techniques that help to make the tools applicable in practice.

Formal verification and linear hybrid automata

Formal verification tries to establish with absolute certainty, in the sense of being mathematically provable, whether or not a given property is satisfied or violated by a system. In this chapter we consider algorithmic approaches to verification of safety properties such as whether a set of forbidden states is reachable. If a verification algorithm is exact (no over-approximations, no floating point computations, no rounding of any kind, etc.) and terminates, it gives the provably correct answer: safe or unsafe. Exact verification algorithms are of limited use for hybrid systems in general, since the solution of a differential equation can only be computed up to some accuracy. One may have to resort to an over-approximative algorithm, i.e. use over-approximations in the sense that when the algorithm terminates with result safe, the system really is safe. If the algorithm finds a violation, one might not know whether the violation is real or an artifact of over-approximations.