Runtime Enforcement for Reactive Systems: Shield Synthesis

This lecture covers the concept of runtime enforcement for reactive systems, focusing on shield synthesis to ensure correct system behavior while deviating only when necessary. Topics include symbolic reasoning, shield synthesis using games, and examples like traffic light controllers. The instructor discusses the application of shields in machine learning for safe reinforcement learning, with a case study on shielding Pac-Man. The lecture also explores optimal shield synthesis, dealing with rush-hour traffic, and probabilistic safety shields for Pac-Man. The use of shields for performance improvement and scalability in large Markov Decision Processes is also addressed.