The 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT

Title: Symbolic and Numeric Challenges in Neural Network Verification Methods

Abstract: The field of formal verification has traditionally looked at proving properties about finite state machines or software programs. Recent research has also looked at other classes of systems such as CPS models given with differential equations, or even systems that include neural networks. We present verification methods and symbolic and numerical challenges and optimizations that make scalable analysis increasingly practical.

Title: Autonomous CPS: Verification and Control

Abstract: As Cyber-Physical Systems are becoming more autonomous, there is an increasing need for methods that ensure safety and reliability. In this talk, we present requirements-based approaches that can be used for automated testing, monitoring, and control synthesis of CPS. The methods utilize ideas from three important areas in CPS research: formal methods, machine learning, and control theory. We illustrate our methods on problems from the automotive industry.

Title: Safe Planning under Epistemic Uncertainty and Partial Information

Abstract: This talk concerns planning problems that are subject to various sources of uncertainty. For example, an autonomous agent may operate under perceptual limitations due to imperfect knowledge about the accuracy of its sensors. To capture such problems with a formal model, we extend partially observable Markov decision processes (POMDPs) to account for epistemic uncertainty. The resulting uncertain POMDPs reflect uncertainty via uncountable sets of probability distributions caused by, for instance, a lack of data available. We present a novel method to compute finite-memory policies for uncertain POMDPs that robustly satisfy temporal logic specifications. In general, computing such policies is theoretically and practically intractable. Our solution is based on efficient convexification techniques for the underlying non-convex optimization problem. We demonstrate the applicability using examples from aircraft collision-avoidance and spacecraft motion planning.