Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice (Invited Talk)

摘要

Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying quantitative probabilistic specifications such as the probability of a critical failure occurring or expected