Deductive verification of continuous dynamical systems

DOI10.4230/LIPICS.FSTTCS.2009.2334zbMATH Open1248.68336OpenAlexW1520660718MaRDI QIDQ2920146FDOQ2920146

Authors Ankur Taly, Ashish Tiwari

Publication date 24 October 2012

Full work available at URL http://subs.emis.de/LIPIcs/frontdoor_ee1b.html

zbMATH Keywords

deductive verificationtheory of realsinductive invariantscontinuous and hybrid dynamical systems

Mathematics Subject Classification ID

Dynamics induced by flows and semiflows (37C10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Applications of dynamical systems (37N99)

Recommendations

• A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets
• A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
• A method for invariant generation for polynomial continuous systems
• Logics of dynamical systems
• Computing Differential Invariants of Hybrid Systems as Fixedpoints

Cited in

(19)

• Proving properties of continuous systems: Qualitative simulation and temporal logic
• Implicit semi-algebraic abstraction for polynomial dynamical systems
• Sufficient conditions for forward invariance and contractivity in hybrid inclusions using barrier functions
• Convex Programs for Temporal Verification of Nonlinear Dynamical Systems
• Safety verification of nonlinear systems based on rational invariants
• Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
• Characterizing positively invariant sets: inductive and topological methods
• A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
• Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
• Exact safety verification of hybrid systems using sums-of-squares representation
• Synthesizing switching controllers for hybrid systems by generating invariants
• Pegasus: a framework for sound continuous invariant generation
• Formal modelling, analysis and verification of hybrid systems
• Direct formal verification of liveness properties in continuous and hybrid dynamical systems
• Model verification in dynamics through strict upper error bounds
• Deductive verification of alternating systems
• Numerically-robust inductive proof rules for continuous dynamical systems
• Barrier certificates revisited
• On converse zeroing barrier functions

This page was built for publication: Deductive verification of continuous dynamical systems

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