André Platzer is an Associate Professor of Computer Science at Carnegie Mellon University. He develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to answer the question how we can trust a computer to control physical processes. André Platzer has a Ph.D. from the University of Oldenburg, Germany, received an ACM Doctoral Dissertation Honorable Mention and NSF CAREER Award, and was named one of the Brilliant 10 Young Scientists by the Popular Science magazine and one of the AI’s 10 to Watch by the IEEE Intelligent Systems Magazine.
AG 1, AG 2, AG 3, INET, AG 4, AG 5, SWS, RG1, MMCI
Autonomous cyber-physical systems are systems that combine the physics of motion with advanced cyber algorithms to act
on their own without close human supervision. The present consensus is that reasonable levels of autonomy, such as for
self-driving cars or autonomous drones, can only be reached with the help of artificial intelligence and machine learning
algorithms that cope with the uncertainties of the real world. That makes safety assurance even more challenging than it
already is in cyber-physical systems (CPSs) with classically programmed control, precisely because AI techniques are
lauded for their flexibility in handling unpredictable situations, but are themselves harder to predict.
This talk identifies the logical path toward autonomous cyber-physical systems. With the help of differential dynamic logic
(dL) do we provide a logical foundation for developing cyber-physical system models with the mathematical rigor that their
safety-critical nature demands. Its ModelPlex technique provides a logically correct way to tame the subtle relationship of
CPS models to CPS implementations. The resulting logical monitor conditions can then be exploited to safeguard the
decisions of learning agents, guide the optimization of learning processes, and resolve the nondeterminism frequently
found in verification models. Overall, logic leads the way in combining the best of both worlds: the strong predictions that
formal verification techniques provide alongside the strong flexibility that the use of AI provides.