Approximation Based Safety and Stability Verification of Hybrid Systems

With the advent of computers to control various physical processes, there has emerged a new class of systems which contain tight interactions between the "discrete" digital world and the "continuous" physical world. These systems which exhibit mixed discrete-continuous behaviors, called "hybrid systems", are present everywhere - in automotives, aeronautics, medical devices, robotics - and are often deployed in safe-critical applications. Hence, reliability of the performance of these systems is a very important issue, and this thesis concerns automatic verification of their models to improve the confidence in these systems. Automatic verification of hybrid systems is an extremely challenging task, owing to the many undecidability results in the literature. Automated verification has been seen to be feasible for only simple classes of systems. These observations have emphasized the need for simplifying the complexity of the system before applying traditional verification techniques. This thesis explores the feasibility of such an approach for verifying complex systems. In this thesis, we take the approach of verifying a complex system by approximating it to a "simpler" system. We consider two important classes of properties that are required of hybrid systems in practice, namely, "safety" and "stability". Intuitively, safety properties are used to express the fact that something bad does not happen during the execution of the system; and stability is used to capture the notion that small perturbations in the initial conditions or inputs to the system, do not result in drastic changes in the behaviors of the system. For safety verification, we present two techniques for approximation, an error based technique which allows one to compute as precise an approximation as desirable in terms of a quantified error between the original and the approximate system, and a property based technique which takes into account the property being analysed in constructing and refining the approximate system. With regard to error based approximation, we provide a technique for approximating a general hybrid system to a polynomial hybrid system with bounded error. The above technique is in general semi-automatic; and we present a fully automatic efficient method for analysing a subclass of hybrid systems by constructing piecewise polynomial approximations. In terms of property based approximation, we propose a novel "counterexample guided abstraction refinement" (CEGAR) technique called "hybrid CEGAR", which constructs a hybrid abstraction of a system unlike the previous methods which were based on constructing finite state abstractions. Our method has several advantages in terms of simplifying the various subroutines in an iteration of the CEGAR loop. We have implemented the hybrid CEGAR algorithm for a subclass of hybrid systems called "rectangular hybrid systems" in a tool called HARE, and the experimental results show that the method has the potential to scale. Though automated verification of safety properties has been well studied, verification of stability properties is still in its preliminary stages with respect to automation. In this thesis, we present certain foundational results which could potentially be used to develop automated methods for analysis of stability properties. We present a framework for verifying "asymptotic" stability or convergence of (distributed) hybrid systems which operate in discrete steps. We then ask a fundamental question related to approximation based verification, namely, what kinds of simplifications preserve stability properties? It turns out that stability properties are not invariant under bisimulation which is a canonical transformation under which various discrete-time properties (including safety) are known to be invariant. We enrich bisimulation with uniform continuity conditions which suffice to preserve various stability properties. These reductions are widely prevelant in the traditional techniques for stability analysis thereby emphasizing the potential use of these techniques for stability verification by approximation