Approximation Based Safety and Stability Verification of Hybrid Systems

Prabhakar, Pavithra

Permalink

https://hdl.handle.net/2142/26102 Copy

Description

Title

Approximation Based Safety and Stability Verification of Hybrid Systems

Author(s)

Prabhakar, Pavithra

Issue Date

2011-08-25T22:12:59Z

Director of Research (if dissertation) or Advisor (if thesis)

Viswanathan, Mahesh

Doctoral Committee Chair(s)

Viswanathan, Mahesh

Committee Member(s)

• Agha, Gul A.
• Dullerud, Geir E.
• Gupta, Aarti
• Mitra, Sayan

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• Verification
• Hybrid Systems
• Safety
• Stability
• Approximations
• Polynomial Approximations
• Abstraction Refinement
• Stability preserving Approximations

Abstract

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

Graduation Semester

2011-08

Permalink

http://hdl.handle.net/2142/26102

Copyright and License Information

Copyright 2011 Pavithra Prabhakar

Owning Collections