A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets

DOI10.1016/J.CL.2015.11.003MaRDI QIDQ681340zbMATH OpenOpenAlexFDO

Authors Khalil Ghorbal, Andrew Sogokon, André Platzer

Publication date 30 January 2018

Published in Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.cl.2015.11.003

zbMATH Keywords

dynamical systemsformal verificationpolynomial differential equationspositive invariancedeductive power

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets
• Deductive verification of continuous dynamical systems
• Characterizing positively invariant sets: inductive and topological methods
• A method for invariant generation for polynomial continuous systems
• Simple LP-type criteria for positively invariant polyhedral sets

Cites work

• scientific article; zbMATH DE number 1183917 (Why is no real title available?)
• scientific article; zbMATH DE number 1414330 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• scientific article; zbMATH DE number 3100403 (Why is no real title available?)
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets
• A differential operator approach to equational differential invariants (invited paper)
• Abstractions for hybrid systems
• Constructing invariants for hybrid systems
• Deductive verification of continuous dynamical systems
• Differential dynamic logic for hybrid systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Generating invariants for non-linear hybrid systems by linear algebraic methods
• Hybrid Systems: Computation and Control
• Integrability and nonintegrability of dynamical systems
• Membership in polynomial ideals over \(\mathcal{Q}\) is exponential space complete
• On the combinatorial and algebraic complexity of quantifier elimination
• Partial cylindrical algebraic decomposition for quantifier elimination
• Qualitative theory of planar differential systems
• Set-theoretic methods in control
• Simplification of quantifier-free formulae over ordered fields
• Some undecidable problems involving elementary functions of a real variable
• Tangent cone and contingent cone to the intersection of two closed sets
• The structure of differential invariants and differential cut elimination

Cited in

(10)

• Implicit semi-algebraic abstraction for polynomial dynamical systems
• Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
• Vector barrier certificates and comparison systems
• Numerically-robust inductive proof rules for continuous dynamical systems
• Characterizing positively invariant sets: inductive and topological methods
• Deductive verification of continuous dynamical systems
• Pegasus: sound continuous invariant generation
• A formal proof in Coq of Lasalle's invariance principle
• A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets
• Pegasus: a framework for sound continuous invariant generation

Describes a project that uses

Uses Software

• QEPCAD

This page was built for publication: A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets

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