Falsification of Autonomous Systems in Rich Environments

To operate autonomously, such systems and agents often rely on automated controllers, which are designed to translate a stream of sensor observations or system states into a stream of commands (controls) to execute, in order to maintain a safe behavior, or robustly perform a specified task. Traditionally, controllers had to be expertly designed, e.g., by meticulously considering physical and mechanical aspects of the system. In recent years, however, computational Neural-Network (NN) controllers have been experiencing tremendous popularity. These can handle complex, highdimensional sensor observations, such as images, and enable effective control of highly-complex dynamical systems, such as racing cars, snake robots, high Degree-of-Freedom (DoF) manipulators, and dexterous robot hands, which have been a great challenge in the controls and robotics communities. Such controllers are typically built ("trained") by compressing numerous examples ("training data") using statistical machine learning techniques, in an attempt to yield a certain behavior. Common techniques include Reinforcement Learning (RL) [2], from repeated trial-and-error control attempts, until apparent convergence to a desired behavior, and Imitation Learning [3], from demonstrations of either a human operator or a traditional controller. Unfortunately, such learning methods generally do not provide a guarantee that the resulting controller will robustly exhibit the desired behavior; hence, relying on these controllers can cause the system to suffer from unpredictable or unsafe behavior on edge cases. While there has been a recent efforts to advance controller synthesis [4-6]--that is, the automated creation of controllers that are guaranteed to comply to given specification by design--these usually fail to scale beyond simple scenarios; and, more importantly, are only certified in relation to the assumed (and often simplified) system models.