Change-of-bases abstractions for non-linear hybrid systems

DOI10.1016/J.NAHS.2015.08.006zbMATH Open1329.93046arXiv1204.4347OpenAlexW1621444007MaRDI QIDQ901261FDOQ901261

Sriram Sankaranarayanan

Publication date: 23 December 2015

Published in: Nonlinear Analysis. Hybrid Systems (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1204.4347

zbMATH Keywords

verificationhybrid systemsinvariantsabstract interpretationabstractionlinearization

Mathematics Subject Classification ID

Geometric methods in ordinary differential equations (34A26) Linear systems in control theory (93C05) Nonlinear systems in control theory (93C10) Transformations (93B17)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• MARCO: A Reachability Algorithm for Multi-affine Systems with Applications to Biological Systems
• Hybrid Systems: Computation and Control
• Counterexample-guided abstraction refinement for symbolic model checking
• Reachability analysis of linear systems using support functions
• Partial cylindrical algebraic decomposition for quantifier elimination
• Semidefinite programming relaxations for semialgebraic problems
• Computation of polytopic invariants for polynomial dynamical systems using linear programming
• Hybrid Systems: Computation and Control
• Affine relationships among variables of a program
• Constructing invariants for hybrid systems
• Conflict resolution for air traffic management: a study in multiagent hybrid systems
• Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
• Non-linear loop invariant generation using Gröbner bases
• Precise interprocedural analysis through linear algebra
• Automatic Generation of Polynomial Loop Invariants
• Validated solutions of initial value problems for ordinary differential equations
• Reachability of Uncertain Nonlinear Systems Using a Nonlinear Hybridization
• Static Analysis
• Computing differential invariants of hybrid systems as fixed points
• Abstractions for hybrid systems
• Verification, Model Checking, and Abstract Interpretation
• Automatic invariant generation for hybrid systems using ideal fixed points
• Accurate hybridization of nonlinear systems
• Preservation of stability of dynamical systems under homomorphisms
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• The Structure of Differential Invariants and Differential Cut Elimination
• Symbolic computation of recursion operators for nonlinear differential-difference equations
• Reasoning Algebraically About P-Solvable Loops
• Morphisms for Non-trivial Non-linear Invariant Generation for Algebraic Hybrid Systems
• Automatic abstraction of non-linear systems using change of bases transformations
• Pre-orders for reasoning about stability
• Automata, Languages and Programming
• Static Analysis
• Static Analysis
• Hybrid Systems: Computation and Control

Cited In (6)

• Linearization, model reduction and reachability in nonlinear ODEs
• Automatic abstraction of non-linear systems using change of bases transformations
• Compiling elementary mathematical functions into finite chemical reaction networks via a polynomialization algorithm for ODEs
• Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
• Modelling and supervisory control of hybrid dynamical systems via fuzzy \(l\)-complete approximation approach
• Reachability of weakly nonlinear systems using Carleman linearization

Uses Software

• QEPCAD
• MARCO
• PHAVer
• HyTech
• REDLOG
• d/dt
• SpaceEx
• Flow*

This page was built for publication: Change-of-bases abstractions for non-linear hybrid systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q901261)