# Strategy Synthesis for Global Window PCTL

arXiv: https://arxiv.org/abs/2204.14107 · HTML: https://mlsanity.com/paper/2204.14107/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Apr 2022.

## Built on by (most cited first, 1 of 1)

- [Synthesis of Safety Specifications for Probabilistic Systems](https://mlsanity.com/paper/2511.16579/) (2025)

## Abstract (arXiv)

Given a Markov decision process (MDP) M and a formula Phi, the strategy synthesis problem asks if there exists a strategy σ s.t. the resulting Markov chain M[σ] 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.