Max. reachability in infinite-state MDP

189 Views Asked by At

Following [1], the maximum probability to reach a set of states $B\subseteq S$ from state $s\in S$ in a Markov decision process with finite state space $S$ can be expressed as the unique solution to the following system of equations over variables $(x_s)_{s\in S}$:

$x_s = \begin{cases} 1 & \text{if } s\in B\\ 0 & \text{if } s\not\models\exists\Diamond B\\ \max\{ \sum_{t\in S} P(s,\alpha,t)\cdot x_t \mid \alpha\in Act(s) \} & \text{otherwise} \end{cases}$

where $P(s,\alpha,t)$ is the transition probability from $s$ to $t$ under action $\alpha$, and $Act(s)$ are the enabled actions in state $s$.

Is there any reason this wouldn't also hold when $S$ is infinite?

[1] Baier, Katoen. Principles of Model Checking.

1

There are 1 best solutions below

0
On BEST ANSWER

Theorem 10.100 in [1] also holds for MDPs with a countable state space S. But be aware that there is a small errata, the solution is not unique $\sum_{s \in S} x_s$ needs to be minimal.

A general proof can be found in Christel Baier's Habilitation thesis (Proposition 3.7.3, page 67).