Formal Verification and Machine Learning Joining Forces
The growing pervasiveness of computerised systems such as intelligent traffic control or energy supply makes our society vulnerable to faults or attacks on such systems. Rigorous software engineering methods and supporting efficient verification tools are crucial to encounter this threat.
- Online webinar
- 9 December 2021
- 15.00 - 16.00
- Language: English
- Price: free
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.
KIM GULDSTRAND LARSEN
PROFESSOR OF COMPUTER SCIENCE,
AALBORG UNIVERSITY
KIM GULDSTRAND LARSEN
Kim Guldstrand Larsen is a Professor of Computer Science at Aalborg University since 1993. He received Honorary Doctorate from Uppsala University (1999), ENS Cachan (2007), International Chair at INRIA (2016) and Distinguished Professor at North-Eastern University, Shenyang, China (2018). His research interests cover modeling, verification, performance analysis of real-time and embedded systems with applications to concurrency theory, model checking and machine learning.
He is the prime investigator of the verification tool UPPAAL for which he received the CAV Award in 2013. Other prizes received include Danish Citation Laureates Award, Thomson Scientific Award as the most cited Danish Computer Scientist in the period 1990-2004 (2005), Grundfos Prize (2016), Ridder af Dannebrog (2007). He is member of the Royal Danish Academy of Sciences and Letters, The Danish Academy of Technical Science, where he is Digital wiseman. Also, he is member of the Academia Europaea.
In 2015 he received the prestigious ERC Advanced Grant (LASSO), and in 2021 he won Villum Investigator Grant (S4OS). He has been PI and director of several large centers and initiatives including CISS (Center for Embedded Software systems, 2002-2008), MT-LAB (Villum-Kahn Rasmussen Center of Excellence, 2009-2013), IDEA4CPS (Danish-Chinese Research Center, 2011-2017), INFINIT National ICT Innovation Network, 2009-2020), DiCyPS (Innovation Fund Center, 2015-2021). Finally, he is co-founder of the companies UP4ALL (2000), ATS (2017) and VeriAal (2020).
