Sound Control Synthesis with Logics and Data

Abstract:
We are witnessing an inter-disciplinary convergence between scientific areas underpinned by model-based reasoning and by data-driven learning. Access to information-rich data has to be traded off with a demand for safety criticality: cyber-physical systems are exemplar applications. 

In this talk, I will report on ongoing research in this cross-disciplinary domain at OXCAV, the Oxford Control and Verification group. 

I will, in particular, focus on control synthesis for complex objectives, and describe how techniques from formal verification (logics and SAT, automata theory, abstractions) and from learning (sample-driven approaches and neural architectures) can be together leveraged to attain both sound and effective synthesis outcomes. 

More broadly, throughout this contribution I will argue that, on the one hand, control theory and formal methods can provide certificates to learning algorithms and, on the other hand, that learning can bolster formal verification and strategy synthesis objectives. 


Bio:
Alessandro Abate is Professor of Verification and Control in the Department of Computer Science at the University of Oxford, where he was also Deputy Head. Earlier, he did research at Stanford University and at SRI International, and was an Assistant Professor at the Delft Center for Systems and Control, TU Delft. He received a Laurea degree from the University of Padua and MS/PhD at UC Berkeley. His research work spans logics, probability, control, and AI.