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

DOI10.1016/j.cl.2015.11.003zbMath1379.68238OpenAlexW2217989345MaRDI QIDQ681340

Andrew Sogokon, Khalil Ghorbal, 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 verificationpositive invariancepolynomial differential equationsdeductive power

Mathematics Subject Classification ID

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

Related Items (4)

Implicit semi-algebraic abstraction for polynomial dynamical systems ⋮ Pegasus: sound continuous invariant generation ⋮ Vector barrier certificates and comparison systems ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants

Uses Software

• QEPCAD

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Tangent cone and contingent cone to the intersection of two closed sets
• Differential dynamic logic for hybrid systems
• Partial cylindrical algebraic decomposition for quantifier elimination
• Simplification of quantifier-free formulae over ordered fields
• Abstractions for hybrid systems
• Constructing invariants for hybrid systems
• Qualitative theory of planar differential systems
• A Differential Operator Approach to Equational Differential Invariants
• Deductive Verification of Continuous Dynamical Systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• On the combinatorial and algebraic complexity of quantifier elimination
• The Structure of Differential Invariants and Differential Cut Elimination
• Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods
• Membership in polynomial ideals over Q is exponential space complete
• A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• Hybrid Systems: Computation and Control
• Some undecidable problems involving elementary functions of a real variable
• Set-theoretic methods in control

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