Dynamic Logics of Dynamical Systems

TL;DR

This survey reviews dynamic logics for specifying and verifying properties of various dynamical systems, emphasizing differential dynamic logics and their applications in safety-critical domains.

Contribution

It provides a comprehensive overview of the semantics, axiomatizations, proof calculi, and theoretical results of dynamic logics for dynamical systems, especially differential dynamic logics.

Findings

Differential dynamic logics can express complex properties of continuous and hybrid systems.

They have been successfully implemented in theorem provers for safety-critical applications.

Theoretical results include soundness, completeness, and deductive power of these logics.

Abstract

We survey dynamic logics for specifying and verifying properties of dynamical systems, including hybrid systems, distributed hybrid systems, and stochastic hybrid systems. A dynamic logic is a first-order modal logic with a pair of parametrized modal operators for each dynamical system to express necessary or possible properties of their transition behavior. Due to their full basis of first-order modal logic operators, dynamic logics can express a rich variety of system properties, including safety, controllability, reactivity, liveness, and quantified parametrized properties, even about relations between multiple dynamical systems. In this survey, we focus on some of the representatives of the family of differential dynamic logics, which share the ability to express properties of dynamical systems having continuous dynamics described by various forms of differential equations. We explain the dynamical system models, dynamic logics of dynamical systems, their semantics, their axiomatizations, and proof calculi for proving logical formulas about these dynamical systems. We study differential invariants, i.e., induction principles for differential equations. We survey theoretical results, including soundness and completeness and deductive power. Differential dynamic logics have been implemented in automatic and interactive theorem provers and have been used successfully to verify safety-critical applications in automotive, aviation, railway, robotics, and analogue electrical circuits.