Strategy Synthesis for Global Window PCTL

TL;DR

This paper investigates the decidability of strategy synthesis in Markov decision processes for a fragment of PCTL with local, bounded horizon properties, showing decidability for deterministic strategies.

Contribution

It introduces a new fragment of PCTL with local properties and linear expressions, analyzing its decidability depending on strategy types.

Findings

Decidability for deterministic strategies in the proposed logic.

Undecidability for general strategies.

Characterization of the logic's frontier of decidability.

Abstract

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$. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.