“Using model checking verifications online: Handling runtime state uncertainty, human-in-the-loop shared control and sampled data feedback” Dr. Ian M. Mitchell, University of British Columbia Wednesday, April 12, 2017 2:00 – 3:00PM EEB 248 Abstract: Recent advances in model checking algorithms for continuous state systems allow us to demonstrate the existence of safe control policies robust to model error for cyber-physical systems (CPS) of practical interest, such as shared control drones or wheelchairs, or automated delivery of anesthesia. However, these verification results are only relevant if we can implement those policies. In this talk I will discuss investigations into three challenges that arise when it comes time to synthesize a feedback control signal that will keep the system safe: Online state uncertainty, human-in-the-loop shared control for older adults with cognitive impairment, and the sampled data nature of that feedback control in typical cyber-physical systems. Bio: Ian M. Mitchell completed his doctoral work in engineering at Stanford University in 2002, spent a year as a postdoctoral researcher at the University of California at Berkeley, and is now an Associate Professor of Computer Science at the University of British Columbia. He is the author of the Toolbox of Level Set Methods, the first publicly available high accuracy implementation of solvers for dynamic implicit surfaces and the time dependent Hamilton-Jacobi equation that works in arbitrary dimension. His research interests include development of algorithms and software for nonlinear differential equations, formal verification, control and planning in cyber-physical and robotic systems, assistive technology and reproducible research.