Change-of-bases abstractions for non-linear hybrid systems. (February 2016)

• Record Type: Journal Article
• Authors: Sankaranarayanan, Sriram
• Is Part Of: Nonlinear analysis. Volume 19(2016)
• Page Start: 107
• Page End: 133
• Publication Date: 2016-02
• Subjects: Hybrid systems -- Abstraction -- Verification -- Linearization -- Invariants -- Abstract interpretation; Nonlinear functional analysis -- Periodicals; Analyse fonctionnelle non linéaire -- Périodiques; Nonlinear functional analysis; Periodicals; 515.7248
• DOI: 10.1016/j.nahs.2015.08.006
• Languages: English
• ISSNs: 1751-570X

Abstract

Abstract: We present abstraction techniques that transform a given non-linear dynamical system into a linear system, or more generally, an algebraic system described by polynomials of bounded degree, so 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-bases 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-bases 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. 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.