In this DIREC talk Kim Guldstrand Larsen will present and discuss how to combine formal verification and AI in order to obtain optimal AND guaranteed safe strategies.
The ultimate goal of synthesis is to disrupt traditional software development. Rather than tedious manual programming with endless testing and revision effort, synthesis comes with the promise of automatic correct-by-construction control software.
In formal verification synthesis has a long history for discrete systems dating back to Church’s problem concerning realization of logic specifications by automata. Within AI the use of (deep) reinforcement learning (Q- and M-learning) has emerged as a popular method for learning optimal control strategies through training, e.g. as applied by autonomous driving.
The formal verification approach and the AI approach to synthesis are highly complementary: Formal verification synthesis comes with absolute guarantees but are computationally expensive with resulting strategies being extremely large. In contrast, AI synthesis comes with no guarantees but is highly scalable with neural networks providing compact strategy representation.
Kim Guldstrand Larsen will present the tool UPPAAL Stratego that combines symbolic techniques with reinforcement learning to achieve (near-)optimality and safety for hybrid Markov decision processes and highlight some of the applications that include water management, traffic light control, and energy aware building.
Emphasis will be on the challenges of implementing learning algorithms, argue for their convergence and designing data structures for compact and understandable strategy representation.