Logical Foundations of Cyber-Physical Systems

Presented as part of the 2014 HCSS conference.

We study the logical foundations of cyber-physical systems (CPS), i.e. 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 air traffic protocols for aircraft collision avoidance maneuvers, the European Train Control System protocol, several automotive systems, mobile robot navigation with the dynamic window algorithm, and a surgical robotic system for skull-base surgery.

Speaker Bio:

André Platzer is an Assistant Professor of Computer Science at Carnegie Mellon University. His interests include logic in computer science, cyber-physical systems, programming languages, formal methods, and automated theorem proving. He received an ACM Doctoral Dissertation Honorable Mention Award, an NSF CAREER Award, the Best Paper Awards at TABLEAUX'07 and at FM'09. André Platzer was also named one of the Brilliant 10 Young Scientists by the Popular Science magazine 2009 and one of the AI's 10 to Watch 2010 by the IEEE Intelligent Systems Magazine.