Change-of-bases abstractions for non-linear hybrid systems
From MaRDI portal
(Redirected from Publication:901261)
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.
Recommendations
- Automatic abstraction of non-linear systems using change of bases transformations
- Algorithms for exact and approximate linear abstractions of polynomial continuous systems
- Hybrid Systems: Computation and Control
- Generating invariants for non-linear hybrid systems
- scientific article; zbMATH DE number 2085344
Cites work
- scientific article; zbMATH DE number 44444 (Why is no real title available?)
- scientific article; zbMATH DE number 51932 (Why is no real title available?)
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 1956582 (Why is no real title available?)
- scientific article; zbMATH DE number 1516499 (Why is no real title available?)
- scientific article; zbMATH DE number 3451986 (Why is no real title available?)
- scientific article; zbMATH DE number 1821399 (Why is no real title available?)
- scientific article; zbMATH DE number 1905118 (Why is no real title available?)
- scientific article; zbMATH DE number 868107 (Why is no real title available?)
- scientific article; zbMATH DE number 872231 (Why is no real title available?)
- scientific article; zbMATH DE number 1444352 (Why is no real title available?)
- Abstractions for hybrid systems
- Accurate hybridization of nonlinear systems
- Affine relationships among variables of a program
- Automata, Languages and Programming
- Automatic Generation of Polynomial Loop Invariants
- Automatic abstraction of non-linear systems using change of bases transformations
- Automatic invariant generation for hybrid systems using ideal fixed points
- Computation of polytopic invariants for polynomial dynamical systems using linear programming
- Computing differential invariants of hybrid systems as fixed points
- Conflict resolution for air traffic management: a study in multiagent hybrid systems
- Constructing invariants for hybrid systems
- Counterexample-guided abstraction refinement for symbolic model checking
- Differential dynamical systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Ideals, varieties, and algorithms. An introduction to computational algebraic geometry and commutative algebra
- MARCO: A Reachability Algorithm for Multi-affine Systems with Applications to Biological Systems
- Morphisms for Non-trivial Non-linear Invariant Generation for Algebraic Hybrid Systems
- Non-linear loop invariant generation using Gröbner bases
- Partial cylindrical algebraic decomposition for quantifier elimination
- Pre-orders for reasoning about stability
- Precise interprocedural analysis through linear algebra
- Preservation of stability of dynamical systems under homomorphisms
- Reachability analysis of linear systems using support functions
- Reachability of Uncertain Nonlinear Systems Using a Nonlinear Hybridization
- Reasoning Algebraically About P-Solvable Loops
- Semidefinite programming relaxations for semialgebraic problems
- Static Analysis
- Static Analysis
- Static Analysis
- Symbolic computation of recursion operators for nonlinear differential-difference equations
- The structure of differential invariants and differential cut elimination
- Validated solutions of initial value problems for ordinary differential equations
- Verification, Model Checking, and Abstract Interpretation
- Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
Cited in
(12)- 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
- Cone-based abstract interpretation for nonlinear positive invariant synthesis
- Computing difference abstractions of linear equation systems
- Decoupling abstractions of non-linear ordinary differential equations
- Differential elimination and algebraic invariants of polynomial dynamical systems
- Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
- Hybrid Systems: Computation and Control
- Modelling and supervisory control of hybrid dynamical systems via fuzzy \(l\)-complete approximation approach
- Reachability of weakly nonlinear systems using Carleman linearization
- Reachability of Koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement
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)
