Aarhus University Seal / Aarhus Universitets segl

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

18.06.2019 | Sofia Rasmussen

Date Thu 20 Jun
Time 10:00 11:00
Location Nygaard-295 (5335-295), Department of Computer Science, Åbogade 34, 8200 Aarhus N

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.

Lecture / talk, CS frontpage, Featured, Public/media