Talk by Prof. Andre Platzer (CMU): Logical Foundations of Cyber-Physical Systems

Title: Logical Foundations of Cyber-Physical Systems

Abstract: Logical foundations of cyber-physical systems (CPS) study systems that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPS applications abound.  Ensuring their correct functioning, however, is a serious challenge.  Scientists and engineers need analytic tools to understand and predict the behavior of their systems.  That's the key to designing smart and reliable control.

This talk identifies a mathematical model for CPS called multi-dynamical systems, i.e. systems characterized by combining multiple facets of dynamical systems, including discrete and continuous dynamics, but also uncertainty resolved by nondeterministic, stochastic, and adversarial dynamics.  Multi-dynamical systems help us understand CPSs better, as being composed of multiple dynamical aspects, each of which is simpler than the full system.  The family of differential dynamic logics surveyed in this talk exploits this compositionality in order to tame the complexity of CPS and enable their analysis.

In addition to providing a strong theoretical foundation for CPS, differential dynamic logics have also been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, several automotive systems, mobile robot navigation with the dynamic window algorithm, and a surgical robotic system for skull-base surgery. The approach is implemented in the theorem prover KeYmaera X.