Kim Larsen (Aalborg University)
In this talk I will present the most recent version of the tool UPPAAL STRATEGO (www.uppaal.org). Taking as inputs 1) an Euclidian Markov Decision Processes E, 2) asafe constraint S and 3) an objective functions O to be optimized, UPPAAL STRATEGO first provides a most permissive safety strategy ensuring S using a Timed Automata abstraction of E. Here well-known symbolic model checking techniques are used. Next, applying various learning methods, sub-strategies (thus still safe) optimizing O are subsequent. The talk will present the new (Q-, M-, ..) learning methods developed, preliminary results on their convergence, the ability to learn and output small and explainable strategies using decision trees, and the approach for taking partial observability into account. The talk will provide a demonstration of the new UPPAAL STRATEGO on the Smart Farming Challenge of the recent Dagstuhl seminar “Analysis of Autonomous Mobile Collectives in Complex Physical Environments” (October 2019). Also on-going applications of UPPAAL STRATEGO on water-management, traffic-light control, energy-aware building ao will be pointed out. Finally, we call the audience to suggest additional features to be incorporated in the tool to be pursued during the newly granted 5-year Villum-Investigator Center S4OS of the speaker.