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.
Fixed point techniques for deriving invariants of differential equations have been proposed by the author in previous papers @cite_37 @cite_41 These techniques have addressed the derivation of polyhedral invariants for affine systems @cite_37 and algebraic invariants for systems with polynomial right-hand sides @cite_41 . In this technique, we employ the machinery of fixed-points. Our primary goal is not to derive invariants, per se, but to search for abstractions of non-linear systems into linear systems.
@cite_41 @cite_37
2137258051 2477967262
We present computational techniques for automatically generating algebraic (polynomial equality) invariants for algebraic hybrid systems. Such systems involve ordinary differential equations with multivariate polynomial right-hand sides. Our approach casts the problem of generating invariants for differential equations as the greatest fixed point of a monotone operator over the lattice of ideals in a polynomial ring. We provide an algorithm to compute this monotone operator using basic ideas from commutative algebraic geometry. However, the resulting iteration sequence does not always converge to a fixed point, since the lattice of ideals over a polynomial ring does not satisfy the descending chain condition. We then present a bounded-degree relaxation based on the concept of "pseudo ideals", due to Colon, that restricts ideal membership using multipliers with bounded degrees. We show that the monotone operator on bounded degree pseudo ideals is convergent and generates fixed points that can be used to generate useful algebraic invariants for non-linear systems. The technique for continuous systems is then extended to consider hybrid systems with multiple modes and discrete transitions between modes. We have implemented the exact, non-convergent iteration over ideals in combination with the bounded degree iteration over pseudo ideals to guarantee convergence. This has been applied to automatically infer useful and interesting polynomial invariants for some benchmark non-linear systems. We investigate techniques for automatically generating symbolic approximations to the time solution of a system of differential equations. This is an important primitive operation for the safety analysis of continuous and hybrid systems. In this paper we design a time elapse operator that computes a symbolic over-approximation of time solutions to a continuous system starting from a given initial region. Our approach is iterative over the cone of functions (drawn from a suitable universe) that are non negative over the initial region. At each stage, we iteratively remove functions from the cone whose Lie derivatives do not lie inside the current iterate. If the iteration converges, the set of states defined by the final iterate is shown to contain all the time successors of the initial region. The convergence of the iteration can be forced using abstract interpretation operations such as widening and narrowing. We instantiate our technique to linear hybrid systems with piecewise-affine dynamics to compute polyhedral approximations to the time successors. Using our prototype implementation TIMEPASS, we demonstrate the performance of our technique on benchmark examples.