The structure of differential invariants and differential cut elimination

DOI10.2168/LMCS-8(4:16)2012MaRDI QIDQ4899116zbMATH OpenFDO

Authors André Platzer

Publication date 7 January 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1104.1987

zbMATH Keywords

differential cut eliminationdifferential dynamic logicdifferential equationsdifferential invariantshybrid systemslogics of programsproof search complexityproof theoryreal differential semialgebraic geometryverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Hybrid systems of ordinary differential equations (34A38) Symmetries, invariants of ordinary differential equations (34C14) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather ad-hoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze trade-offs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics.

Recommendations

• A differential operator approach to equational differential invariants (invited paper)
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Computing differential invariants of hybrid systems as fixed points
• A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets
• Differential dynamic logic for hybrid systems

Cited in

(13)

• A complete uniform substitution calculus for differential dynamic logic
• Vector barrier certificates and comparison systems
• Numerically-aided deductive safety proof for a powertrain control system
• Synthesizing switching controllers for hybrid systems by generating invariants
• A differential operator approach to equational differential invariants (invited paper)
• Verification of Hybrid Systems
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Differential equation axiomatization. The impressive power of differential ghosts
• Differential game logic
• A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
• Refining constructive hybrid games
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Change-of-bases abstractions for non-linear hybrid systems

Describes a project that uses

Uses Software

• PHAVer
• ETPS
• HyTech

This page was built for publication: The structure of differential invariants and differential cut elimination

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