Symbolic reachability computation for families of linear vector fields
Quantifier elimination, model completeness, and related topics (03C10) Applications of computability and recursion theory (03D80) Symbolic computation and algebraic computation (68W30) Attainable sets, reachability (93B03) Eigenvalue problems (93B60) Control/observation systems governed by ordinary differential equations (93C15) Discrete event control/observation systems (93C65)
The authors identify classes of linear control systems of the type \(\dot{x}(t)=Ax(t)+u(t)\), for which the finite time reachable set can be computed using symbolic computation tools by means of quantifier elimination. NEWLINENEWLINENEWLINEDepending on the eigenvalue structure of \(A\), admissible spaces of control functions are derived, described by linear combinations of basis functions. The main idea behind this construction is that -- after suitable changes of variables, if necessary -- the exponential terms vanish in the description of the reachable set, which eventually allows for the use of symbolic computation tools. NEWLINENEWLINENEWLINEProceeding this way, the following three classes of systems are derived: NEWLINENEWLINENEWLINE(i) \(A\) is nilpotent and \(u\) is a linear combination of polynomials \(t^k\) NEWLINENEWLINENEWLINE(ii) \(A\) is diagonalizable with real rational eigenvalues and \(u\) is a linear combination of exponentials \(e^{\mu t}\) satisfying a non-resonance condition NEWLINENEWLINENEWLINE(iii) \(A\) is diagonalizable with purely imaginary eigenvalues and \(u\) is a linear combination of \(\sin(\mu t)\) and \(\cos(\mu t)\) satisfying a non-resonance condition NEWLINENEWLINENEWLINEFor each of these classes, the results are illustrated by examples.
- Reachability analysis of rational eigenvalue linear systems
- Approximating reachable sets for a class of linear control systems†
- scientific article; zbMATH DE number 1794361
- Algorithm for determining the reachability set of a linear control system
- Reachable, controllable sets and stabilizing control of constrained linear systems
- A theory of timed automata
- Cylindrical Algebraic Decomposition I: The Basic Algorithm
- Ellipsoidal techniques for reachability analysis: Internal approximation
- scientific article; zbMATH DE number 1574496 (Why is no real title available?)
- scientific article; zbMATH DE number 3937151 (Why is no real title available?)
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 1263213 (Why is no real title available?)
- scientific article; zbMATH DE number 1303067 (Why is no real title available?)
- scientific article; zbMATH DE number 1157666 (Why is no real title available?)
- scientific article; zbMATH DE number 1160037 (Why is no real title available?)
- scientific article; zbMATH DE number 1169378 (Why is no real title available?)
- scientific article; zbMATH DE number 1744838 (Why is no real title available?)
- scientific article; zbMATH DE number 1444360 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- Hybrid systems: computation and control. 2nd international workshop, HSCC '99. Berg en Dal, the Netherlands, March 29--31, 1999. Proceedings
- Logic and structure.
- Model theory.
- Nonlinear control system design by quantifier elimination
- O-minimal hybrid systems.
- Output feedback stabilization and related problems-solution via decision methods
- Partial cylindrical algebraic decomposition for quantifier elimination
- Robust multi-objective feedback design by quantifier elimination
- Symbolic model checking for real-time systems
- Testing stability by quantifier elimination
- The algorithmic analysis of hybrid systems
- First-order orbit queries
- A semantic model for interacting cyber-physical systems
- Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming
- Pegasus: sound continuous invariant generation
- Conservative time discretization: a comparative study
- Algorithmic analysis of polygonal hybrid systems. I: Reachability
- Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
- Positive root isolation for poly-powers by exclusion and differentiation
- \(\epsilon\)-semantics computations on biological systems
- Algorithmic analysis of polygonal hybrid systems. II: Phase portrait and tools
- Abstractions for hybrid systems
- Constructing invariants for hybrid systems
- Characterization and computation of control invariant sets for linear impulsive control systems
- A piecewise ellipsoidal reachable set estimation method for continuous bimodal piecewise affine systems
- Some decidable results on reachability of solvable systems
- Formal modelling, analysis and verification of hybrid systems
- Reachability analysis of rational eigenvalue linear systems
- Theory and computational techniques for analysis of discrete-time control systems with disturbances
- Verification of Hybrid Systems
- Linear temporal logic satisfaction in adversarial environments using secure control barrier certificates
- Reachability and optimal control for linear hybrid automata: a quantifier elimination approach
- Sampling-based algorithm for testing and validating robot controllers
- Interrupt Timed Automata
- scientific article; zbMATH DE number 1953286 (Why is no real title available?)
- Interrupt timed automata: verification and expressiveness
- scientific article; zbMATH DE number 1794361 (Why is no real title available?)
- Quantifier-free encoding of invariants for hybrid systems
- Barrier certificates revisited
- scientific article; zbMATH DE number 7559488 (Why is no real title available?)
- scientific article; zbMATH DE number 7559115 (Why is no real title available?)
- Reachability computation for polynomial dynamical systems
- Synthesis of controllers for target problems of hybrid systems using approximate computation
- Adaptive parameter tuning for reachability analysis of nonlinear systems
- Limit cycles of linear vector fields on \(( \mathbb{S}^2)^m \times \mathbb{R}^N\)
- On the decidability of reachability in continuous time linear time-invariant systems
- Pegasus: a framework for sound continuous invariant generation
- Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis
- Reachability analysis of linear systems
- Invariants for continuous linear dynamical systems
- Reduction of transcendental decision problems over the reals
- Synthesizing invariant barrier certificates via difference-of-convex programming
- Geometry and topology of parameter space: Investigating measures of robustness in regulatory networks
- Hybridization methods for the analysis of nonlinear systems
- Exact safety verification of hybrid systems using sums-of-squares representation
- Understanding deadlock and livelock behaviors in hybrid control systems
- Solving and visualizing nonlinear parametric constraints in control based on quantifier elimination
- MetiTarski: An automatic theorem prover for real-valued special functions
- Span-reachability and observability of bilinear hybrid systems
- Inclusion dynamics hybrid automata
This page was built for publication: Symbolic reachability computation for families of linear vector fields
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5945290)
