Strategy Synthesis for Global Window PCTL

Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha +1

Given a Markov decision process (MDP) $M$ and a formula $\Phi$, the strategy synthesis problem asks if there exists a strategy $\sigma$ s.t. the resulting Markov chain $M[\sigma ]$ satisfies $\Phi$…