Title: Model Checking, Performance Analysis, Synthesis and Learning for Cyber-Physical Systems

Abstract: Timed automata and priced timed automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. During the last 20 years the real-time model checker UPPAAL has developed a number of methods allowing for efficient verification of hard timing constraints of timed automata. Moreover a number of significant branches exists, e.g. UPPAAL SMC, providing a highly scalable new engine supporting (parallel and distributed) statistical model checking of stochastic hybrid automata with significant applications to performance of energy-aware sensor networks as well as evaluation of lock-down measures in Denmark under COVID. Most recently the new branch  UPPAAL Stratego offers a neuro-symbolic approach to achieve safe and  near-optimal decision tree control strategies.   The tool  combines a dynamic partition-refinement Q-learning algorithm with symbolic methods for synthesizing  safety shields that ensures correctness by design. To make synthesis of shields tractable, UPPAAL Stratego are using various abstraction and state-space transformation techniques. We demonstrate superiority of applying the shield before learning (pre-shielding) compared to after (post-shielding).   In addition trade-offs between efficiency of strategy representation and degree of optimality subject to safety constraints will be discussed  The tutorial will also highlight recent extensions to shielding and reinforcement learning of multi-agent systems. Besides providing demonstrations of UPPAAL Stratego, the tutorial will give insight into a number of successful  CPS applications including traffic control, water-management, heating systems, swarm robotics and many more.