Relational differential dynamic logic

DOI10.1007/978-3-030-45190-5_11MaRDI QIDQ5039509zbMATH OpenOpenAlexFDO

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

Publication date 13 October 2022

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

hybrid systemtheorem provingdynamic logicformal verificationcyber-physical system

Mathematics Subject Classification ID

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) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Differential Dynamic Logic for Verifying Parametric Hybrid Systems
• Differential dynamic logic for hybrid systems
• Differential Refinement Logic
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Quantified Differential Dynamic Logic for Distributed Hybrid Systems

Cites work

• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• A complete uniform substitution calculus for differential dynamic logic
• Approximate bisimulation: a bridge between computer science and control theory
• Differential Refinement Logic
• Differential dynamic logic for hybrid systems
• Differential equation axiomatization. The impressive power of differential ghosts
• Hyperstream processing systems, nonstandard modeling of continuous-time signals
• Logical foundations of cyber-physical systems
• Modeling in Event B. System and software engineering.
• Non-standard analysis
• Ordinary differential equations with applications
• Programming with Infinitesimals: A While-Language for Hybrid System Modeling
• Ranking and repulsing supermartingales for reachability in probabilistic programs
• Simple relational correctness proofs for static analyses and program transformations
• The Complete Proof Theory of Hybrid Systems

Cited in

(4)

• scientific article; zbMATH DE number 4128794 (Why is no real title available?)
• Distributed Relation Logic
• Differential Refinement Logic
• A Kleene algebra with tests for union bound reasoning about probabilistic programs

Describes a project that uses

Uses Software

• Rodin
• Mathematica

This page was built for publication: Relational differential dynamic logic

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