The logical path to autonomous cyber-physical systems

Abstract

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 paper identifies the logical path toward autonomous cyber-physical systems in multiple steps. First, differential dynamic logic () provides a logical foundation for developing cyber-physical system models with the mathematical rigor that their safety-critical nature demands. Then, its ModelPlex technique provides a logically correct way to tame the subtle relationship of CPS models to CPS implementations. Finally, 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.