Relational Differential Dynamic Logic

DOI10.1007/978-3-030-45190-5_11OpenAlexW3021147957MaRDI QIDQ5039509

Akihisa Yamada, Jérémy Dubut, Shin-ya Katsumata, Ichiro Hasuo, David Sprunger, Juraj Kolčák

Publication date: 13 October 2022

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

zbMATH Keywords

theorem provingformal verificationdynamic logichybrid systemcyber-physical system

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Mathematica
• Rodin

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Approximate bisimulation: a bridge between computer science and control theory
• Differential dynamic logic for hybrid systems
• A complete uniform substitution calculus for differential dynamic logic
• Hyperstream processing systems
• The Complete Proof Theory of Hybrid Systems
• Programming with Infinitesimals: A While-Language for Hybrid System Modeling
• Simple relational correctness proofs for static analyses and program transformations
• Differential Refinement Logic
• Logical Foundations of Cyber-Physical Systems
• Differential Equation Axiomatization
• Non-standard analysis
• Ranking and repulsing supermartingales for reachability in probabilistic programs

This page was built for publication: Relational Differential Dynamic Logic