André Platzer

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.

Some references

• 1. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, Cham, 2018. https://doi.org/10.1007/978-3-319-63588-0
• 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. https://doi.org/10.1109/LICS.2012.64
• 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, 2020. https://doi.org/10.1145/3380825
• 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/