Computational Approaches for Stochastic Shortest Path on Succinct MDPs

1 Introduction

Markov decision processes. Markov decision processes (MDPs) [Howard, 1960] are a standard mathematical model for sequential decision making, with a wide range of applications in artificial intelligence and beyond [Puterman, 1994; Filar and Vrieze, 1997; Bertsekas, 2005]. An MDP consists of a set of states, a finite set of actions (that represent the nondeterministic choices), and a probabilistic transition function that describes the transition probability over the next states, given the current state and action. One of the most classical optimization objectives in MDPs is the stochastic shortest path (SSP) problem, where the transitions of the MDP are labeled with rewards/costs, and the goal is to optimize the expected total rewards until a target set is reached.

Curse of dimensionality. In many typical applications, the computational analysis of MDPs suffers from the curse of dimensionality. The state space of the MDP is huge as it represents valuations to many variables that constitute the MDP. A well-studied approach for algorithmic analysis of large MDPs is to consider factored MDPs [Guestrin et al., 2003; Delgado et al., 2011], where the transition and reward function dependency can be factored only on few variables.

† Corresponding Author

‡A full version of this paper, including details and formal proofs, is available at [Chatterjee et al., 2018].

Succinct MDPs. In the spirit of factored MDPs, which aim to deal with the curse of dimensionality, we consider succinct MDPs, where the MDP is described implicitly by a set of variables, and a set of rules that describe how the variables are updated. The rules can be chosen non-deterministically from this set at every time step to update the variables, until a target set (of valuations) is reached. The rules and the target set represent the succinct description of the MDP. We consider the SSP problem for succinct MDPs.

Our contributions. Our main contributions are as follows:

1. First, we show that many examples from the AI literature (e.g., Gambler's Ruin, Robot Planning, and variants of Roulette) can be naturally modeled as succinct MDPs.
2. Second, we present mathematical and computational results for the SSP problem for succinct MDPs. For the SSP problem the sup-value (resp. inf-value) represents the expected shortest path value with supremum (resp., infimum) over all policies. We consider linear bounds for the SSP problem and our algorithmic bounds are as follows: (a) for the sup-value (resp. inf-value) we show that an upper (resp., lower) bound can be computed in polynomial time in the implicit description of the MDP; (b) for the sup-value (resp. inf-value) we show that a lower (resp., upper) bound can be computed by a polynomial-time (in the implicit description) reduction to quadratic programming. Our approach is as follows: we use results from probability theory to establish a mathematical approach to compute bounds for the SSP problem for succinct MDPs (Section 3), and reduce the mathematical approach to constraint solving to obtain a computational method (Section 4).
3. Finally, we present experimental results on several classical examples from the literature where our method computes tight bounds (i.e., lower and upper bounds are quite close) on the SSP problem extremely efficiently.

Comparison with approaches for factored MDPs. Some key advantages of our approach are the following. First, our approach gives a provably polynomial-time algorithm or polynomial-time reduction to quadratic programming in terms of the size of the implicit description of the MDP. Second, while algorithms for factored MDPs are typically suitable for finite-state MDPs, our method can handle MDPs with countable state space (e.g., when the domains of the variables are integers), or even uncountable state space (e.g., when the domains of the variables are reals). See Remark 1 for details.

2 Definitions and Examples

We define succinct Markov Decision Processes, the stochastic shortest path problem, and provide illustrative examples.

2.1 Succinct Markov Decision Processes

Markov decision processes (MDPs). MDPs are a standard mathematical model for sequential decision making. An MDP consists of a state space S and a finite action space A, and given a state s and an action a permissible in s, there is a probability distribution function P that describes the transition probability from the current state to the next states (i.e., P(s′ | s, a) is the transition probability from s to s′ given action a). Moreover, there is a reward assigned to each state and action pair.

Factored MDPs. In many applications of MDPs, the state space of the MDP is high-dimensional and huge (i.e., the state space consists of valuations to many variables). For computational analysis it is often considered that the MDP can be factored, i.e., the transition and reward probabilities depend only on a small number of variables. For algorithmic analysis of finite-state factored MDPs see [Guestrin et al., 2003].

Succinct MDPs. In this work, we consider succinct MDPs, which are related to factored MDPs. First, we present an informal description and then the details. A succint MDP is described by a set of variables, and a set of rules that update them. The update rule can be chosen non-deterministically or stochastically. Thus the MDP is described implicitly with the set of rules and a condition that describes the target set of states, and the MDP terminates when the target set is reached. We describe succinct MDPs as a special class of programs with a single while loop.

Simple-while-loop succinct MDPs. We consider succinct MDPs described by a simple while loop program. There are two types of variables, namely, program and sampling variables. Program variables are normal variables, while sampling variables are those whose values are sampled independently wrt some probability distribution. In general, both program and sampling variables can take integer, or even real values. The succinct MDP is described by a simple while loop of the form:

• φ is the loop guard defined as a single comparison between linear arithemtic expressions over program variables (e.g. x ≤ y + 1);
• in the loop body, Q1, . . . ,Qk are sequential compositions of assignment statements, grouped by the nondeterminism operator □.

Every assignment statement has a program variable as its lefthand-side and a linear arithmetic expression over program and sampling variables as its right-hand-side. The operator □ is the nondeterministic choice which means that the decision as to which Qi will be executed in the current loop iteration depends on a scheduler (or policy) that resolves nondeterminism. We first provide the formal syntax and then an example.

Formal syntax of simple-while-loop programs. A succinct MDP is specified by a simple-while-loop program equipped with probability distributions for sampling variables. We now formalize the intuitive description provided in Equation (1). Formally, a simple-while-loop program can be produced using the following grammar, where each <pvar> is chosen from a finite fixed set X of program variables, each <svar> from a finite fixed set R of sampling variables and each <constant> denotes a floating point number:

〈nondet-block-list〉 '}' 'od' 〈guard〉 ::= 〈linear-pvar-expr〉 〈cmp〉 〈linear-pvar-expr〉 〈linear-pvar-expr〉 := 〈constant〉 | 〈constant〉 '*' 〈pvar〉 | 〈linear-pvar-expr〉 '+' 〈linear-pvar-expr〉 〈cmp〉 ::= '>=' | '>' | '<=' | '<' 〈nondet-block-list〉 ::= 〈block〉 | 〈block〉 □ 〈nondet-block-list〉 〈block〉 ::= 〈assignment〉 | 〈assignment〉 〈block〉 〈assignment〉 ::= 〈pvar〉 ':=' 〈linear-expr〉 ';' 〈linear-expr〉 ::= 〈constant〉 | 〈constant〉 '*' 〈pvar〉 | 〈constant〉 '*' 〈svar〉 | 〈linear-expr〉 '+' 〈linear-expr〉 Example 1. Consider the following program

where x is a program variable and r is a sampling variable that observes the two-point distribution P(r = -1) = P(r = 1) = 1 2 . Informally, the program performs either decrement or random increment/decrement on x until its value is zero.

Informal description of the semantics. Given a simplewhile-loop program in the form (1), an MDP is obtained as follows: the state space S consists of values assigned to program variables (i.e., valuations for program variables); the action space A correponds to the non-deterministic choice between Q1, . . . ,Qk; and the transition function P depends on the sampling of the sampling variables, which given the current valuation for program variables probabilistically updates the valuation. The assignments are linear functions, and the loop guard φ describes the target states as those which do not satisfy φ. Given the above components, the notion of a policy (or scheduler) σ that resolves the non-deterministic choices, and that of the probability space Pσ given a policy is standard [Puterman, 1994]. For a more formal treatment of the semantics, see [Chatterjee et al., 2018].

Remark 1 (Simple-while-loop MDPs and Factored MDPs). The principle behind factored MDPs and simple-while-loop succinct MDPs is similar. Both aim to consider highdimensional and large MDPs described implicitly in a succinct way. In factored MDPs the transitions and reward functions can be factored based on small sets of variables, but the dependency on the variables in these sets can be arbitrary. In contrast, in simple-while-loop succinct MDPs, we only allow linear arithmetic expressions as guards and assignments. Moreover, our MDPs do not allow nesting of while loops. The goal of our work is to consider linear upper and lower bounds, and nesting of linear loops can result in super-linear bounds. Hence, we do not consider nesting of loops. Therefore, simple-while-loop succinct MDPs are a special class of factored MDPs.

For algorithmic approaches with theoretical guarantees on computational complexity, the analysis of factored MDPs has typically been restricted to finite-state MDPs. However, we will present solutions for simple-while-loop programs, where the variables can take integer or real values, and thus the underlying state space is infinite or even uncountable. Thus the class of simple-while-loop MDPs consists of large finite-state MDPs (when the variables are bounded); countable state MDPs (variables are integer); and even uncountable state MDPs (variables are real-valued). Moreover, our algorithmic approaches provide computational complexity guarantee on the input size of the implicit representation of the MDP. Note that for finite-state MDPs, the implicit representation can be exponentially more compact than the explicit MDP. For example, n boolean variables lead to a state-space of size 2n .

In the sequel we consider MDPs obtained from simplewhile-loop programs and, for brevity, call them succinct MDPs.

2.2 Stochastic Shortest Path on Succinct MDPs

We consider the stochastic shortest path (SSP) problem on succinct MDPs. Below we fix a succinct MDP described by a while-loop in the form (1).

Reward function. We consider a reward function R that assigns a reward R(u, ℓ) when the sampling valuation for sampling variables is u and the non-deterministic choice is Qℓ (in a loop iteration). We assume that there is a maximal constant Rmax ≥ 0 such that |R(u, ℓ)| ≤ Rmax for all u, ℓ. The rewards need not be nonnegative as our approach is able to handle negative rewards as well. Moreover, our approach can be extended to allow bounded reward functions that depend on program variables, too. See [Chatterjee et al., 2018] for a more detailed discussion.

Stochastic shortest path. Given an initial valuation v for program variables and a policy σ, the definition of expected total reward/cost until termination is standard. The inf-value (resp., sup-value) of a succinct MDP, given an initial valu-

whi le x ≥ 1 do □ i f (0.4) { x := x+1 reward=1 } e l s e { x := x-1 } □ i f (0.3) { x := x+1 reward=1 } e l s e { x := x-1 }

ation v for program variables, is the infimum (resp., supremum) expected reward value over all policies that ensure finite expected termination time, which we denote as infval(v) (resp., supval(v)).

Computational problem. We consider the computational problem of obtaining upper and lower bounds for the infvalue and sup-value for succinct MDPs. Due to the similarity of the problems, we focus on computing lower and upper bounds for the sup-value. The results for inf-value are similar and omitted. For formal details, see [Chatterjee et al., 2018].

2.3 Illustrative Examples

Example 2 (Gambler's Ruin). We start with a simple and classical example. A gambler has x0 tokens for gambling. In each round he can choose one of the two types of gambling. In type 1, he wins with probability p1 < 1/2 and in type 2 with probability p2 < 1/2. A win leads to a reward of w and an extra token. A loss costs one token. The player gambles as long as he has tokens left. His goal is to maximize overall expected reward. Letting p1 = 0.4, p2 = 0.3 and w = 1, a succinct MDP for this example is shown in Figure 1.

Remark 2. Note that above we use probabilistic if as syntactic sugar, where the assignments in if(p) run with probability p and those in the else part with probability 1 - p. Given that the assignments are linear, this can be translated back to a succinct MDP, e.g. the first if-else block in Figure 1 is equivalent to:

x := x+ r reward=0.4

where r is a sampling variable with P(r = 1) = 0.4 and P(r = -1) = 0.6.

Example 3 (Continuous variant). We can also consider a continuous variant of the example where the sampling variable r is chosen from some continuous distribution with expected value -0.2 (e.g., uniform distribution [-0.8, 0.4]).

3 Theoretical Results

In this section we present the main theoretical results which forms the basis of our algorithms of the following section.

Notation. Given a succinct MDP in the form (1), we let X be the set of program variables in the program, |X| be the size of X, R|X| be the set of |X|-dimensional real-valued vectors, v ∈ R|X| be a valuation for program variables such that the value for the ith program variable is the ith coordinate of v, u be a valuation for sampling variables, N := {1, . . . , k}

be the set of non-deterministic choices, ℓ ∈ N be a nondeterministic choice, and Fℓ (ℓ ∈ N) be the function such that Fℓ(v, u) is the valuation for program variables resulting from executing Qℓ with the valuation v for program variables and the sampled valuation u for sampling variables. Table 1 summarizes the notation.

Upper bounds. We first introduce the main concept for computing an upper bound for supval(v) formally, and then present the informal description.

Definition 1 (Linear Upper Potential Functions (LUPFs)). A linear upper potential function (LUPF) is a function h : R|X| → R that satisfies the following conditions:

• (C1) h is linear, i.e., there exist a ∈ R|X| and b ∈ R such that for all v ∈ R|X| , we have h(v) = aT · v + b;
• (C2) for all v, u, ℓ such that v |= φ, Fℓ(v, u) |= ¬φ and ℓ ∈ N, we have K ≤ h(Fℓ(v, u)) ≤ K′ for some fixed constants K and K′ ;
• (C3) for all ℓ ∈ N and all valuations v such that v |= φ,

where Eu(h(Fℓ(v, u))), Eu(R(u, ℓ)) are the expected values over the sampling u when fixing v and ℓ;

• (C4) for all v such that v |= φ, all sampling valuations u and all ℓ ∈ N, we have |h(v) - h(Fℓ(v, u))| ≤ M for some fixed constant M ≥ 0.

Informally, (C1) specifies the linearity of LUPFs, (C2) specifies that the value of the function at terminating valuations should be bounded, (C3) specifies that the current value of the function at v is no less than that of the next step at Fℓ(v, u) plus the cost/reward at the current step, and finally (C4) specifies that the change of value between the current step v and the next step Fℓ(v, u) is bounded. Note that Eu(h(Fℓ(v, u))) is linear in v since h and Fℓ are linear. Note that the function h (only) depends on the valuations of the variables before the loop execution, and hence it is only loopdependent (but not dependent on each assignment).

The following theorem shows that LUPFs indeed serve as upper bounds for supval(▪).

Theorem 1. If h is an LUPF, then supval(v) ≤ h(v) -K for all valuations v ∈ R|X| such that v |= φ.

Proof sketch. The key ideas of the proof are as follows: Fix any scheduler σ that ensures finite expected termination time.

• We first construct a stochastic process based on h. Using the condition (C3) which is non-increasing property we establish that the stochastic process obtained is a supermartingale (for definitions of supermartingale see [Williams, 1991, Chapter 10]). The supermartingale in essence preserve the non-increasing property.
• Given the supermartingale, we apply Optional Stopping Theorem (OST) ([Williams, 1991, Chapter 10.10]), and use condition (C4) to establish the required boundedness condition of OST, to arrive at the desired result.

See [Chatterjee et al., 2018] for the full formal proof.

While conditions (C1) and (C2) are not central to the proof, the condition (C1) ensures linearity, which will be required by our algorithms, and the condition (C2) is the boundedness after termination, that derives the desired upper bounds (i.e., contribution of the term K comes from condition (C2)).

Lower bounds. We now consider the lower bounds.

Definition 2 (Linear Lower Potential Functions (LLPFs)). A linear lower potential function (LLPF) is a function h : R|X| → R that satisfies (C1),(C2),(C4) and in addition (C3') (instead of (C3)) as follows:

Similar to Theorem 1, we obtain the following result on lower bounds for supval(▪).

Theorem 2. If h is an LLPF, then supval(v) ≥ h(v) -K′ for all valuations v ∈ R|X| such that v |= φ.

4 Computational Results

By Theorem 1 and Theorem 2, to obtain tight upper and lower bounds for the SSP problem, we need an algorithm to obtain good LUPFs and LLPFs, respectively. We present the results for upper and lower bounds separately.

4.1 Computational Approach for Upper Bound

The key steps to obtain an algorithmic approach is as follows: (i) we first establish a linear template with unknown coefficients for a LUPF from (C1); (ii) then we transform logical conditions (C2)-(C4) equivalently into inclusion assertions between polyhedrons; (iii) next we transform inclusion assertions into linear inequalities through Farkas' Lemma; (iv) finally we solve the linear inequalities through linear programming, where the solution for unknown coefficients in the template synthesizes a concrete LUPF that serves as an upper bound for the sup-value. We now recall Farkas' Lemma.

Theorem 3 (Farkas' Lemma [Farkas, 1894]). Let A ∈ Rm×n , b ∈ Rm, c ∈ Rn and d ∈ R. Suppose that {x ∈ Rn | Ax ≤ b} ̸= ∅. Then

iff there exists y ∈ Rm such that y ≥ 0, ATy = c and bTy ≤ d.

Intuitively, Farkas' Lemma transforms the inclusion problem of a nonempty polyhedron within a halfspace into a feasibility problem of a system of linear inequalities. As a result, one can decide the inclusion problem in polynomial time through linear programming.

The Algorithm UpperBound. Consider as input a succinct MDP in the form (1).

1. Template. The algorithm sets up a column vector a of |X| fresh variables and a fresh scalar variable b such that the template for an LUPF h is h(v) = aT · v + b.
2. Constraints on a and b. We first encode the condition (C2) for the template h as the inclusion assertion

parameterized with a, b,K,K′ for every ℓ ∈ N, where K,K′ are fresh unknown constants.

Then for every ℓ ∈ N, the algorithm encodes (C3) as

where cℓ, dℓ are unique linear combinations of unknown coefficients a, b satisfying that cTℓ · v ≤ dℓ is equivalent to h(v) ≥ Eu(h(Fℓ(v, u))) + Eu(R(u, ℓ)). Finally, the algorithm encodes (C4) as inclusion assertions with a fresh unknown constant M using similar transformations. All the inclusion assertions (with parameters a, b,K,K′ ,M) are grouped conjunctively so that these inclusions should all hold.

1. Applying Farkas' Lemma. The algorithm applies Farkas' Lemma to all the inclusion assertions generated in the previous step and obtains a system of linear inequalities involving the parameters a, b,K,K′ ,M.
2. Constraint Solving. The algorithm calls a linear programming solver on the linear program consisting of the system of linear inequalities generated in the previous step and the minimizing objective function aT · v0 + b - K where v0 is an initial valuation for program variables.

Correctness and running time. The above algorithm obtains concrete values for a, b,K,K′ ,M and leads to a concrete LUPF h. The correctness that aT ·v+b-K is an upper bound for the sup-value follows from Theorem 1. The main optimization solution required by the algorithm is linear programming, and thus our algorithm runs in polynomial time in the size of the input succinct MDP.

Theorem 4. Given a succinct MDP and the SSP problem, the best linear upper bound (wrt an initial valuation) on the sup-value can be computed in polynomial-time in the implicit description of the MDP.

Example 4. Consider the Gambler's Ruin example (from Section 2.3, Figure 1).

Let h : R → R be an LUPF for this example, we have: (C1) ∃λ1, λ2 ∈ R ∀x ∈ R h(x) = λ1x+λ2

(C2) ∃K,K′ ∈ R ∀x ∈ [1, 2) K ≤ h(x) ≤K′

(C3) ∀x∈ [1, ∞) h(x) ≥ 0.4·(1+h(x+1))+0.6·h(x-1)

Note that for condition (C2) we need to quantify over x ∈ [1, 2), as if x is not in this range, then the loop does not terminate in the next iteration. Given condition (C1), the two (C4) conditions are equivalent to M ≥ λ1. Also, the (C2) condition is equivalent to K ≤ min{h(1), h(2)} and K′ ≥ max{h(1), h(2)} or more precisely K ≤ λ1 + λ2, K ≤ 2λ1+λ2, K′ ≥ λ1+λ2 and K′ ≥ 2λ1+λ2. By expanding the occurrences of h in the first (C3) condition and simplifying, we get ∀x ∈ [1,∞) 0 ≥ 0.4-0.2λ1 and we can drop the quantification given that x does not appear. Similarly, the second (C3) condition is equivalent to 0 ≥ 0.3-0.4λ1. In our method, such equivalences are automatically obtained by applying Farkas' Lemma rather than manual inspection of the inequalities. Now that all necessary conditions are replaced by equivalent linear inequalities, we can solve the linear program to find an LUPF. An optimal answer (with minimal λ1) is the following: λ1 = M = 2, λ2 = K = 0, K′ = 4. Therefore by Theorem 1, we have supval(x0) ≤ 2x0 for all initial valuations x0 that satisfy the loop guard.

Remark 3. Note that our approach is applicable to succinct MDPs with integer as well as real-valued variables, (i.e., the underlying state-space of the MDP is infinite). Even when we consider integer variables, since h gives upper bounds, the reduction is to linear programming, rather than integer linear programming. Note that our approach only depends on expectation of sampling variables, and thus applicable even to continuous sampling variables with same expectation, e.g., our results apply uniformly to Example 2 and Example 3, given that the sampling variable r has same expectation.

4.2 Computational Approach for Lower Bound

The algorithm for lower bound is similar to the upper bound, however, there are some subtle and key differences. An important difference is that while in Step 2 of the algorithm for upper bound, there is a conjunction of contraints, for the lower bound problem it requires a disjunction. This has two important implications: first, we need to consider a generalization of Farkas' lemma and in this case we use Motzkin's Transposition Theorem (which extends Farkas' Lemma with strict inequalities) and second, instead of linear programming we require quadratic programming.

Theorem 5 (Motzkin's Transposition Theorem [Motzkin, 1936]). Let A ∈ Rm×n , B ∈ Rk×n and b ∈ Rm, c ∈ Rk . Assume that {x ∈ Rn | Ax ≤ b} ̸= ∅. Then

iff there exist y ∈ Rm and z ∈ Rk such that y, z ≥ 0, 1T · z > 0, ATy + BTz = 0 and bTy + cTz ≤ 0.

The Algorithm LowerBound. Our algorithm is similar to UpperBound. For brevity, we only explain the differences.

1. Template h. Same as in the AlgorithmUpperBound.
2. Constraints on a and b. The algorithm first encodes (C2) and (C4) as inclusion assertions in the same way as in UpperBound and transforms them into linear inequalities over a, b, K, K′ , M through Farkas' Lemma.

Then the algorithm transforms (C3') equivalently into the inclusion assertion

where cℓ, dℓ are determined in the same way as in UpperBound. Furthermore, this inclusion assertion is equivalently written as

and then transformed into a system of quadratic inequalities over a and b through Motzkin's Transposition Theorem. The system may involve quadratic inequalities since cℓ contains the unknown parameters a and b.

1. Constraint Solving. The algorithm calls a nonlinearprogramming solver on the system of linear and quadratic inequalities generated in the previous step with the maximizing objective function aT ·v0+b-K′ where v0 is an appropriate initial valuation.

Correctness and optimization problem. As for the upper bound, once a, b, K, K′ , M are found, we obtain an concrete lower bound aT ·v+b-K′ for the sup-value from Theorem 2, establishing the correctness of our algorithm. The reduction leads to a quadratic optimization problem of polynomial size wrt the succinct MDP, implying the following result.

Theorem 6. Given a succinct MDP and the SSP problem, the best linear lower bound (wrt an initial valuation) on the supvalue can be computed via a polynomial (in the implicit description of the MDP) reduction to quadratic programming.

Example 5. Let h : R → R be an LLPF for the Gambler's Ruin example (Figure 1 in Section 2.3). The conditions of the form (C1), (C2) and (C4) are exactly the same as in Example 4. In addition, h must also satisfy the following condition:

Expanding the occurrences of h in the condition above using h(x) = λ1x + λ2, and discarding the quantification, we obtain the following equivalent disjunctive system of inequalities: 0 ≤ 0.4 - 0.2λ1 or 0 ≤ 0.3 - 0.4λ1. This system is obviously equivalent to λ1 ≤ 2. Note that in general we have disjunction of linear inequalities, which require quadratic programming. As explained previously, such equivalences are automatically obtained by our algorithm using Motzkin's transposition theorem.

Adding the equivalent linear forms of conditions (C1), (C2) and (C4) as in Example 4 and considering the resulting linear program with the objective of maximizing λ1 leads to the following solution: λ1 = M = 2, λ2 = -2,K =

0,K′ = 2. Therefore, by Theorem 2, supval(x0) ≥ 2x0 for every initial valuation x0 that satisfies the loop guard. This is the same upper bound we found in Example 4. The bound is tight.

5 Case Studies and Experiments

5.1 Additional Examples

We consider several other classical problems in probabilistic planning that can be described as succinct MDPs.

Two-dimensional Robot Planning. Consider a robot that is placed on an initial point (x0, y0) of a grid. A player controls the robot and at each step, can order it to move one unit in either direction. However, the robot is not perfect. It follows the order with probability p < 1 and ignores it and goes to the left with probability 1 - p. The process ends when the robot leaves the x ≥ y half-plane and the player's objective is to keep the robot in this half-plane. The player gets a reward of 1 each time the robot moves. Note that our method can handle any half-plane and starting point.

Multi-robot Planning. Our approach can handle many variables and is only polynomially dependent on the succinct representation of the MDP. To demonstrate this, we consider a scenario similar to the previous case, in which there are now two robots r1 and r2 starting at positions (x0, y0) and (x′0 , y′0 ). The robot r1 follows the orders with probability p1 and malfunctions and goes right with probability 1-p1. Similarly, r2 follows the commands with probability p2 and goes left with probability 1-p2. The player's goal is to keep r1 to the left of r2, i.e. to keep the robots in the four-dimensional half-space x ≤ x′ . The process ends when the robots leave this half-space and the player gets a reward of 1 per step.

Mini-roulette. We model Mini-roulette which is a game on a 13-slot wheel. A player starts with x0 chips. She needs one chip bet and she bets as long as she has chips. If she loses, the chip will not be returned, but a win will not consume the chip and results in a specific amount of (monetary) reward, and possibly even more chips. These types of bets can be placed: (i) Even money bets: 6 specific slots are chosen. Then the ball is rolled and the player wins if it lands in one of the 6 slots. So the winning probability is 6/13. Winning gives a unit reward and one extra chip. (ii) 2-to-1 bets: 4 slots are chosen and winning gives a reward of 2 and 2 extra chips. (iii,iv,v) 3-to-1, 5-to-1 and 11-to-1 bets: These correspond to winning probabilities of 3/13, 2/13 and 1/13 respectively.

American Roulette. The game is like Mini-roulette, except that there are more types of bets and the wheel has 38 slots. The player can now have half-chips. A bet can lead to one of three outcomes: definite loss, partial loss or win. A definite loss costs one chip and a partial loss half a chip. A win pays a reward and more chips. Table 2 summarizes the bets.

5.2 Experimental Results

We implemented our approach in Java and experimented on all examples mentioned previously. The results are summarized in Table 3, where "Parameters" shows concrete parameters for our examples, "Upper bound" (resp. "Lower bound") presents the LUPFs (resp. LLPFs) obtained through our approach, and finally "Time" shows the running time in milliseconds. The reported upper bounds on sup-values are the results of h(v)-K as in Theorem 1. Similarly, lower bounds on sup-values are obtained from h(v) -K′ as in Theorem 2. Finally, our approach is not sensitive to parameters as varying them will only change coefficients of our LUPFs/LLPFs.

Runtime. Our approach is extremely efficient and handles all these MDPs, even when the succinct representation is large, in less than a second. The results were obtained on an Intel Core i5-2520Mmachine, running Ubuntu. We used lpsolve [Berkelaar et al., 2004], JavaILP [Lukasiewycz, 2008] and JOptimizer [Tivellato, 2017] for optimization tasks.

Significance of our results. First, observe that in most experimental results the upper and lower bounds are tight. Thus our approach provides precise bounds on the SSP problem for several classical examples. Second, our results apply to infinite-state MDPs: in all the above examples, we consider infinite-state MDPs, where algorithmic approaches for factored MDPs do not work. Finally, in the above examples, instead of infinite-state MDPs if we consider large finite-state MDP variants (e.g., bounding x in Gambler's Ruin with a large domain), then as the MDP becomes larger, the SSP value of the finite-state MDP approaches the infinite-state value. Hence, our tight bounds on the infinite-state SSP value provide efficient approximation for large finite-state MDPs.

6 RelatedWorks

MDPs. MDPs are widely studied in the AI literature [Sigaud and Buffet, 2010; Dean et al., 1997; Singh et al., 1994; Williams and Young, 2007; Poupart et al., 2015; Gilbert et al., 2017; Topin et al., 2015; Perrault and Boutilier, 2017;

Boutilier and Lu, 2016; Ferns et al., 2004]; and factored MDPs are considered as an effective approach [Guestrin et al., 2003]. We introduced succinct MDPs and efficient algorithms which are applicable to several problems in AI.

PPDDL and RDDL. There are a variety of languages for specifying MDPs and especially factored MDPs. Two of the most commonly used are PPDDL [Younes and Littman, 2004] and RDDL [Sanner, 2010]. These are general languages capturing all factored MDPs. Instead, we consider succinct MDPs with linear guards and assignments and no nested while-loops. Hence, our language is simpler than them.

Programming language results. Besides the AI community, research in programming languages also considers probabilistic programs and algorithmic approaches [Chakarov and Sankaranarayanan, 2013; Chatterjee et al., 2016]; but the main focus is on termination, whereas we consider the SSP and compute precise bounds. While both approaches use the theory of martingales, the key differences are as follows:

• Problem difference: [Chatterjee et al., 2016] considers the number of steps to termination. There is no notion of reward or stochastic shortest path. In contrast, we consider rewards and SSP. In particular, we have negative rewards that cannot be modeled by the notion of steps.
• Result difference: [Chatterjee et al., 2016] considers the qualitative question of whether expected termination time is finite or not, and then applies Azuma's inequality to martingales for concentration bounds. In contrast, we present upper and lower bounds on expected SSP. Thus our results provide quantitative (rather than qualitative) bounds for expected SSP that significantly generalize expected termination time. However, our results are applicable to a more restricted class of programs.
• Proof-technique difference: [Chatterjee et al., 2016] considers qualitative expected termination time characterization, and the main mathematical tool is martingale convergence that does not handle negative rewards. In contrast, we present quantitative bounds for SSP and our mathematical tool is Optional Stopping Theorem.

Comparison with [Hansen and Abdoulahi, 2015]. This work provides convergence tests for heuristic search valueiteration algorithms. While both approaches provide bounds for SSPs, the main differences are as follows: (i) our approach can handle negative costs whereas [Hansen and Abdoulahi, 2015] can handle only positive costs; (ii) our results are on the implicit representation of MDPs, while [Hansen and Abdoulahi, 2015] evaluates parts of the explicit MDP; and (iii) our approach presents polynomial reductions to optimization problems and is not dependent on value-iteration.

7 Conclusion

We consider succinct MDPs and present algorithms for the SSP problem on them. A direction for future work is to consider other algorithmic approaches for succinct MDPs. Also, we consider linear templates and extending our approach to more general templates is another interesting direction.

Acknowledgements

The research was partially supported by Vienna Science and Technology Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Starting grant (279307: Graph Games).