Algorithmic Formal Methods in Continuous Control
Abstract: Algorithmic formal methods such as model checking and reactive synthesis were originally developed in the context of discrete systems such as hardware circuits and software. Over the last few years, these techniques have played an increasingly important role in the development of high assurance cyber-physical systems, in which discrete components interact with continuous physical systems. I will survey some recent results applying formal methods to continuous systems, pointing out how notions such as invariants, variants, bisimulation, and trace equivalence can be adapted in the context of continuous systems. Specifically, I will show two examples of theoretical ideas from formal methods applied to continuous control: a deductive system for controller synthesis for continuous systems against temporal specifications, and a semi-formal conformance testing procedure based on a metric generalization of trace equivalence. I will conclude with some current challenges in the area.
[Joint work with Jyo Deshmukh, Rayna Dimitrova, and Vinayak Prabhu]