Programming and Proving with Dynamical Systems
Dynamic logic has been introduced for understanding programs, but its real calling are dynamical systems.
Dynamic logic excels at providing simple and elegant logical foundations for the dynamical systems arising in
cyber-physical systems. Since these CPSs combine cyber aspects such as communication and computer control with
physical aspects such as movement in space, their dynamical system models also combine discrete dynamics with
continuous dynamics. Differential dynamic logic provides a programming language for these models and comes with
a compositional axiomatization and strong completeness guarantees. Its implementation in the KeYmaera X theorem
prover has been instrumental in verifying applications such as the Airborne Collision Avoidance System ACAS X
and ground robot navigation.
- 1. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, Cham, 2018.
- 2. André Platzer. Logics of dynamical systems, LICS, 2012: 13-24. http://doi.org/10.1109/LICS.2012.13.
- 3. André Platzer. The complete proof theory of hybrid systems. LICS, 2012: 541-550.
- 4. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated
Reasoning 59(2), pp. 219-265, 2017. https://doi.org/10.1007/s10817-016-9385-1
- 5. André Platzer and Yong Kiam Tan. Differential equation invariance axiomatization. J. ACM 67(1), 6:1-6:66,
- 6. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer. KeYmaera X: An aXiomatic
tactical theorem prover for hybrid systems. CADE, 2015: 527-538. http://keymaeraX.org/