Differential dynamic logic for hybrid systems

DOI10.1007/s10817-008-9103-8zbMath1181.03035OpenAlexW1977444293MaRDI QIDQ1040772

André Platzer

Publication date: 25 November 2009

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-008-9103-8

zbMATH Keywords

differential equationssequent calculusdynamic logicautomated theorem provingaxiomatisationEuropean Train Control Systemverification of hybrid systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Related Items

A mechanically verified theory of contracts, Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B, Differential Game Logic, Relational Differential Dynamic Logic, Skill-Based Verification of Cyber-Physical Systems, Implicit semi-algebraic abstraction for polynomial dynamical systems, Simulation of hybrid systems under Zeno behavior using numerical infinitesimals, Rigorous Discretization of Hybrid Systems Using Process Calculi, Verification of Hybrid Systems, Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent, KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems, Quantified Differential Temporal Dynamic Logic for Verifying Properties of Distributed Hybrid Systems, Pegasus: sound continuous invariant generation, Axiomatizing Analog Algorithms, A deductive approach towards reasoning about algebraic transition systems, The refinement calculus of reactive systems, Bellerophon: tactical theorem proving for hybrid systems, Exact safety verification of hybrid systems using sums-of-squares representation, Reusable contracts for safe integration of reinforcement learning in hybrid systems, Certified reinforcement learning with logic guidance, \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic, Computing Differential Invariants of Hybrid Systems as Fixedpoints, Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata, A program logic to verify signal temporal logic specifications of hybrid systems, Verifiably safe exploration for end-to-end reinforcement learning, Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions, Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems, Formal verification and quantitative metrics of MPSoC data dynamics, A complete uniform substitution calculus for differential dynamic logic, Unnamed Item, Algebra, Coalgebra, and Minimization in Polynomial Differential Equations, KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description), Rigorous Simulation-Based Analysis of Linear Hybrid Systems, Programming with Infinitesimals: A While-Language for Hybrid System Modeling, A Simulink-based software solution using the infinity computer methodology for higher order differentiation, A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets, ModelPlex: verified runtime validation of verified cyber-physical system models, Reachability computation for polynomial dynamical systems, Real World Verification, Fifty years of Hoare's logic, Safe \& robust reachability analysis of hybrid systems, Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems, A formal framework for Hybrid Event B, Verified interactive computation of definite integrals, \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic, Computing differential invariants of hybrid systems as fixed points, Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants, A denotational semantics of simulink with higher-order UTP, Constructive hybrid games, Implicit definitions with differential equations for KeYmaera X (system description), The possibilistic Horn non-clausal knowledge bases, A Survey on Analog Models of Computation, Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point

Uses Software

• QEPCAD
• PHAVer
• HyTech
• STeP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Universal computation and other capabilities of hybrid and continuous dynamical systems
• Using branching time temporal logic to synthesize synchronization skeletons
• Partial cylindrical algebraic decomposition for quantifier elimination
• First-order dynamic logic
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• Theorem proving modulo
• Verification of clocked and hybrid systems
• Cooperation of background reasoners in theory reasoning by residue sharing
• Hybrid action systems
• First-order modal logic
• Computability with polynomial differential equations
• Verification of cooperating traffic agents
• Automating Verification of Cooperation, Control, and Design in Traffic Applications
• The Image Computation Problem in Hybrid Systems Model Checking
• Dynamic Logic with Non-rigid Functions
• “Sometimes” and “not never” revisited
• Differential automata and their discrete simulators
• Proving termination with multiset orderings
• Soundness and Completeness of an Axiom System for Program Verification
• A unified framework for hybrid control: model and optimal control theory
• Computational techniques for hybrid system verification
• Differential Dynamic Logic for Verifying Parametric Hybrid Systems
• A Temporal Dynamic Logic for Verifying Hybrid System Invariants
• Automated Technology for Verification and Analysis
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Hybrid Systems: Computation and Control
• On differentiability of Peano type functions