A complete uniform substitution calculus for differential dynamic logic
From MaRDI portal
Publication:1707599
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Abstract: This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms, which uniform substitutions instantiate soundly. The static semantics of differential dynamic logic and the soundness-critical restrictions it imposes on proof steps is captured exclusively in uniform substitutions and variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this article introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivatives as first-class axioms to reason about differential equations axiomatically. The resulting axiomatization of differential dynamic logic is proved to be sound and relatively complete.
Recommendations
Cites work
- scientific article; zbMATH DE number 3122413 (Why is no real title available?)
- scientific article; zbMATH DE number 4069224 (Why is no real title available?)
- scientific article; zbMATH DE number 1183917 (Why is no real title available?)
- scientific article; zbMATH DE number 1556014 (Why is no real title available?)
- scientific article; zbMATH DE number 755666 (Why is no real title available?)
- scientific article; zbMATH DE number 3068536 (Why is no real title available?)
- A uniform substitution calculus for differential dynamic logic
- Banishing the rule of substitution for functional variables
- Classes of Recursively Enumerable Sets and Their Decision Problems
- Differential Hybrid Games
- Differential dynamic logic for hybrid systems
- Differential game logic
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- HRELTL: a temporal logic for hybrid systems
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Logical frameworks
- The Complete Proof Theory of Hybrid Systems
- The structure of differential invariants and differential cut elimination
- Theorem proving modulo
Cited in
(29)- An axiomatic approach to existence and liveness for differential equations
- Differential equation invariance axiomatization
- Schematic program proofs with abstract execution. Theory and applications
- Constructive game logic
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Implicit definitions with differential equations for KeYmaera X (system description)
- Skill-based verification of cyber-physical systems
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
- Relational differential dynamic logic
- Deductive stability proofs for ordinary differential equations
- A uniform substitution calculus for differential dynamic logic
- Differential equation axiomatization. The impressive power of differential ghosts
- \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
- Pegasus: sound continuous invariant generation
- Verification of Hybrid Systems
- Verified interactive computation of definite integrals
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- scientific article; zbMATH DE number 2080012 (Why is no real title available?)
- Uniform substitution for differential game logic
- From post-conditions to post-region invariants
- Verifiably safe exploration for end-to-end reinforcement learning
- Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems
- Dynamical properties of logical substitutions
- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
- Uniform substitution at one Fell swoop
- Bellerophon: tactical theorem proving for hybrid systems
- An axiomatic approach to liveness for differential equations
- Parallel composition and modular verification of computer controlled systems in differential dynamic logic
- Verifying Switched System Stability With Logic
This page was built for publication: A complete uniform substitution calculus for differential dynamic logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1707599)
