Model Checking, Monitoring, Performance Analysis, Synthesis and Learning for Cyber-Physical Systems
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 CORA providing efficient support for optimization. Also the branch UPPAAL SMC, provides 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.
More 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, as well as successful on-going applications (water-management, heating systems, and traffic control, swarm robotics). Most recently, methods for shielding and reinforcement learning has been extended to multi-agent systems.
Finally, the lecture will also cover a recent series of work on developing efficient methods for on-line monitoring the conformance of a real-time systems with respect to logical specifications (e.g. MITL).
Most of the methods and techniques presented are to be found in the recently released UPPAAL 5.0.