We present abstraction techniques that transform a given non-linear dynamical system into a linear system or an algebraic system described by polynomials of bounded degree, such that, invariant properties of the resulting abstraction can be used to infer invariants for the original system. The abstraction techniques rely on a change-of-basis transformation that associates each state variable of the abstract system with a function involving the state variables of the original system. We present conditions under which a given change of basis transformation for a non-linear system can define an abstraction. Furthermore, the techniques developed here apply to continuous systems defined by Ordinary Differential Equations (ODEs), discrete systems defined by transition systems and hybrid systems that combine continuous as well as discrete subsystems. The techniques presented here allow us to discover, given a non-linear system, if a change of bases transformation involving degree-bounded polynomials yielding an algebraic abstraction exists. If so, our technique yields the resulting abstract system, as well. This approach is further extended to search for a change of bases transformation that abstracts a given non-linear system into a system of linear differential inclusions. Our techniques enable the use of analysis techniques for linear systems to infer invariants for non-linear systems. We present preliminary evidence of the practical feasibility of our ideas using a prototype implementation.
Many different types of have been studied for hybrid systems @cite_12 including predicate abstraction @cite_30 and abstractions based on invariants @cite_17 . The use of counter-example guided iterative abstraction-refinement has also been investigated in the past (Cf. @cite_18 and @cite_9 , for example). In this paper, we consider continuous abstractions for continuous systems specified as ODEs, discrete systems and hybrid systems using a change of bases transformation. As noted above, not all transformations can be used for this purpose. Our abstractions for ODEs bear similarities to the notion of topological semi-conjugacy between flows of dynamical systems @cite_13 .
@cite_30 @cite_18 @cite_9 @cite_13 @cite_12 @cite_17
2060369194 1793594870 2127574686 226431050 2117218135 2138239212
We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions. Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counter-examples generated by the search in the abstract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counter-examples, optimizations of these techniques, implementation of these in the verification tool, and case studies demonstrating the promise of the approach. The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring considerable creativity and insight.In this article, we present an automatic iterative abstraction-refinement methodology that extends symbolic model checking. In our method, the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or "spurious") counterexamples. We devise new symbolic techniques that analyze such counterexamples and refine the abstract model correspondingly. We describe aSMV, a prototype implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach. Preface List of figures List of tables 1. Introduction 2. Linear systems 3. Existence and uniqueness 4. Dynamical systems 5. Invariant manifolds 6. The phase plane 7. Chaotic dynamics 8. Bifurcation theory 9. Hamiltonian dynamics A. Mathematical software Bibliography Index. A hybrid system is a dynamical system with both discrete and continuous state changes. For analysis purposes, it is often useful to abstract a system in a way that preserves the properties being analysed while hiding the details that are of no interest. We show that interesting classes of hybrid systems can be abstracted to purely discrete systems while preserving all properties that are definable in temporal logic. The classes that permit discrete abstractions fall into two categories. Either the continuous dynamics must be restricted, as is the case for timed and rectangular hybrid systems, or the discrete dynamics must be restricted, as is the case for o-minimal hybrid systems. In this paper, we survey and unify results from both areas. Hybrid systems combine discrete state dynamics which model mode switching, with continuous state dynamics which model physical processes. Hybrid systems can be controlled by affecting both their discrete mode logic and continuous dynamics: in many systems, such as commercial aircraft, these can be controlled both automatically and using manual control. A human interacting with a hybrid system is often presented, through information displays, with a simplified representation of the underlying system. This user interface should not overwhelm the human with unnecessary information, and thus usually contains only a subset of information about the true system model, yet, if properly designed, represents an abstraction of the true system which the human is able to use to safely interact with the system. In safety-critical systems, correct and succinct interfaces are paramount: interfaces must provide adequate information and must not confuse the user. We present an invariance-preserving abstraction which generates a discrete event system that can be used to analyze, verify, or design user-interfaces for hybrid human-automation systems. This abstraction is based on hybrid system reachability analysis, in which, through the use of a recently developed computational tool, we find controlled invariant regions satisfying a priori safety constraints for each mode, and the controller that must be applied on the boundaries of the computed sets to render the sets invariant. By assigning a discrete state to each computed invariant set, we create a discrete event system representation which reflects the safety properties of the hybrid system. This abstraction, along with the formulation of an interface model as a discrete event system, allows the use of discrete techniques for interface analysis, including existing interface verification and design methods. We apply the abstraction method to two examples: a car traveling through a yellow light at an intersection, and an aircraft autopilot in a landing go-around maneuver.