Computer Science Thesis Proposal

Wednesday, September 5, 2018 - 10:00am to 11:00am


Traffic21 Classroom 6501 Gates Hillman Centers



Verifiably Safe Autonomy for Cyber-Physical Systems

This thesis focuses on verifiably safe reinforcement learning for cyber-physical systems. Cyber-physical systems, such as autonomous vehicles and medical devices, are increasingly common and increasingly autonomous. Designing safe cyber-physical systems is difficult because of the interaction between the discrete dynamics of control software and the continuous dynamics of the vehicle's physical movement.

Formal methods capable of reasoning about these hybrid discrete-continuous dynamics can help engineers obtain strong safety guarantees about safety-critical control systems. Several recent successes in applying formal methods to hybrid dynamical systems demonstrate that these tools provide a promising foundation for establishing safety properties about planes, trains, and cars. However, existing theory and tooling does not explain how to obtain formal safety guarantees for systems that use reinforcement learning to discover efficient control policies from data. This gap in existing knowledge is important because modern approaches toward building cyber-physical systems combine machine learning with classical controls engineering to navigate in open environments.

Previously completed work introduces KeYmaera X, a theorem prover for hybrid systems and uses KeYmaera X to obtain verified safety guarantees for control policies generated by reinforcementlearning algorithms. These contributions enable strong safety guarantees for optimized control policies
when the underlying environment matches a first-principles model. However, classical hybrid systems verification results do not provide guarantees for systems that deviate from an engineer's modeling assumptions.

This thesis introduces an approach toward providing safety guarantees for learned control policies even when reality deviates from modeling assumptions. The core technical contribution will be a new class of algorithms that learn safe ways to update a model in response to newly observed dynamics in the environment. We propose achieving this goal by discovering verification-preserving model updates (VPMUs), thus leveraging hybrid systems theorem proving during the learning process. These contributions will provide verifiable safety guarantees for systems that are controlled by policies obtained through reinforcement learning, justifying the use of reinforcement learning in safety-critical settings.

Thesis Committee:
André Platzer (Chair)
Jeremy Avigad
Zico Kolter
Stefan Mitsch
Goran Frehse (Université Grenoble)

Thesis Summary

Location: Traffic21 Classroom 6501

Title: Verifiably Safe Autonomy for Cyber-Physical Systems

Nathan Fulton, Ph.D. Student

For More Information, Contact:


Thesis Proposal