Change-Of-Bases Abstractions for Non-Linear Systems

TL;DR

This paper introduces abstraction techniques that transform non-linear systems into linear or polynomial-based algebraic systems via change-of-basis, enabling the use of linear analysis methods to infer invariants for complex systems.

Contribution

It develops conditions and methods for constructing change-of-basis transformations that produce algebraic abstractions of non-linear systems, applicable to continuous, discrete, and hybrid systems.

Findings

Techniques can identify polynomial-based abstractions for non-linear systems.

The approach enables analysis of non-linear systems using linear system techniques.

Preliminary implementation shows practical feasibility.

Abstract

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.