
$$\forall s\;.\;\bigvee_{a\in{\mathcal{A}}}\quad\bigwedge_{i=1,\ldots,T}\left(E(s,i)=r(s)+\sum_{s^{\prime}\in n_{a}(s)}t(s,s^{\prime},P(s))\cdot E(s^{\prime},i-1)\right).$$

Considering a given s only, the condition can be checked in polynomial time. Since **this**
condition have to be checked for all possible s ∈ S**, the problem is in coNP. The case of**
history-dependent policies is dealt with by replacing ∀s with ∀s0, . . . , sj and i **with** T − j.

Hardness can be proved as follows: given a formula Q over variables X = {x1**, . . . , x**n},
we build the succinct MDP with V = X and with a single action a**. This action takes**
a number i ∈ {1, . . . , n} with equal probability and changes the value of xi**. The reward**
function is 1 in a state if it satisfies Q, and 0 otherwise. The value function with E(s, i**) = 0**
for all s ∈ S and i = 1, . . . , T **is consistent with the MDP if and only if the formula** Q is unsatisfiable. Indeed, since the MDP only contains one action, the only possible stationary or history-dependent policy is that of always executing the action a**. Such a policy leads** to a random interpretation. The expected reward of this policy is 1 if and only if no interpretation satisfies Q.

Checking the existence of a consistent succinct value function of size bounded by z and expected reward bounded by k **is therefore in Σ**p 2
, as it can be done by guessing a succinct value function E**, checking its consistency with the MDP and the horizon, and determining**
the expected reward of the initial state E(s0, T**). Since consistency is in coNP for boundedaction MDPs, the problem is in Σ**p 2
. The following theorem also shows that the problem is complete for this class.

Theorem 9 Given a bounded-action MDP M, a horizon T **in unary notation, a size bound**
z in unary notation, and a reward bound k**, checking the existence of a succinct value**
function E that is consistent with M and T, of size bounded by z **and expected reward**
bounded by k is Σ
p 2
-complete both for stationary and history-dependent policies.

Proof. Membership: guess a succinct value function E **(i.e., guess a circuit with a state or**
history and an integer as input) of size at most z**; check whether it is consistent with the**
MDP and the horizon, and whether E(s0, T) ≥ k**. Since checking consistency in in coNP**
for both stationary and history-dependent policies, the problem is in Σp 2 in both cases.

Hardness is proved as in Theorem 6. We use the problem of checking whether there exists a truth evaluation over X whose extensions to X ∪ Y are all models of Q**, where** Q
is a formula over X ∪ Y and |X| = |Y | = n.

The MDP that corresponds to Q has sequences of literals over X ∪ Y **as states. There**
is an action aifor each variable in Y and two actions bi and cifor each variable in X**. The**
effect of aiis to add either yi or ¬yi **to the state, with the same probability. The actions** bi and ci add xi and ¬xi**, respectively, and are therefore deterministic actions. The reward of**
a state is 1 if and only if the state is a sequence comprised of either x1 or ¬x1 **followed by** x2 or ¬x2, etc., and its literals form a model of Q**. All other states have reward 0.**
A policy with nonzero reward executes either bi or ci at time i**, and then execute the**
actions a1, . . . , an in sequence. After the first n **actions, the state is exactly a model over** X.

The reward of the policy is the number of models that extend it and satisfy Q**. Therefore,**