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

DOI10.1016/J.CL.2015.11.003zbMATH Open1379.68238OpenAlexW2217989345MaRDI QIDQ681340FDOQ681340

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

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

zbMATH Keywords

dynamical systemsformal verificationpolynomial differential equationspositive invariancedeductive power

Mathematics Subject Classification ID

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

Cites Work

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

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

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)