SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes

Pranav Ashok, Jan Křetínský, Kim Guldstrand Larsen +3

For hybrid Markov decision processes, UPPAAL Stratego can compute strategies that are safe for a given safety property and (in the limit) optimal for a given cost function. Unfortu…