Planning for Stochastic Games with Co-Safe Objectives

1 Introduction

Markov Decision Processes (MDPs) are powerful models for systems involving both decision-making and probabilistic dynamics [Puterman, 1994]. In an MDP, states can be partitioned into controller states and probabilistic states. At a controller state, a decision has to be made to choose a successor, while at a probabilistic state, the successor will be sampled with prescribed probability distribution. One popular research area of MDPs in Artificial Intelligence (AI) is probabilistic planning [Mausam and Kolobov, 2012]: Given an objective, can controller states choose successors in such a way that the objective is fulfilled. Most of previous work restricted to reachability properties, for which memoryless deterministic strategies suffice, namely, given a set of goal states and a threshold, can we find a map from controller states to their successors such that the probability of reaching the goal states is greater than the threshold? See for instance [Xu and Mannor, 2011; Mausam and Kolobov, 2012; Pineda et al., 2013]. Robust planning for reachability properties has also been studied [Nilim and Ghaoui, 2005; Delage and Mannor, 2007] to deal with MDPs where transitions probabilities are not known precisely.

In practice, however, we often encounter sophisticated objectives beyond reachability properties, hence making previous work not applicable. To see this, let us consider a gambling

Lijun Zhang

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China

game between a gambler G with an initial credit c > 0 and a machine M with two buttons: an optimistic one and a pessimistic one. By pressing the optimistic button, with probability 12 , M will award G 10 credits, while with probability 12 , M will take 8 credits from G. If the pessimistic button is chosen, M will award G 2 credits or take 1 credit from G with probability 23 and 13 , respectively. The gambler can repeat the game as many times as he wishes unless he loses all credits. In case the number of credits is less than 8, then only the pessimistic button is available. Suppose c = 10 initially. We would like to know (*)"whether G has a strategy such that: 1) with probability greater than 0.2 that G will have no less than 20 credits, and 2) in the next n rounds, with probability equal to or less than 0.3 that at each game the probability of losing all credits eventually is greater than 0.5." Such a requirement can be specified by the Probabilistic Computation Tree Logic [Hansson and Jonsson, 1994] (PCTL) as follows:

Intuitively, ♦someting and □something mean "something will happen eventually" and "something will always hold", respectively. The probability operator [some event]>0.2 denotes that the probability of some event happening is greater than 0.2. The formal syntax and semantics of PCTL can be found in Section 2.2. Clearly, the requirement in Eq. (1) cannot be represented as a reachability property.

In this paper we study stochastic games with branching time winning objectives given by PCTL formulas, which have been studied extensively in the model checking community [Baier et al., 2004; Kucera and Strazovsk´y, 2008; Br´azdil et al., 2006; Baier et al., 2012]. Different from reachability properties, winning strategies of PCTL objectives may require memory and randomization [Baier et al., 2004], hence makes the problem much harder to be solved. In [Baier et al., 2004], it was shown that the problem of deciding whether there exists a memoryless deterministic winning strategy for a PCTL objective is NPcomplete. An algorithm in EXPTIME was given in [Kucera and Strazovsk´y, 2008] to solve the same problem except that randomized strategies were taken into account. When strategies with prefect recall are considered, the problem turns to be highly undecidable [Br´azdil et al., 2006], no matter whether strategies are deterministic or randomized. These results are summarized in Table 1 and 2.

The main contribution of the current paper is shown in the middle column of Table 2. To be specific, we focus on cosafe PCTL [Katoen et al., 2014], a subset of PCTL which includes a wide range of practical properties, in particular reachability ones and the one in Eq. (1). For this set of properties, memoryless deterministic strategies do not suffice, unlike the case for reachability. We show that stochastic games with co-safe PCTL objectives are decidable, even when the most general strategies, i.e. randomized strategies with perfect recall, are considered. Other contributions of this paper include:

• We show that robust stochastic games [Kucera and Strazovsk´y, 2008] with co-safe PCTL objectives are also decidable, where a winning strategy is tolerant to a certain amount of perturbation.
• We prove that satisfiability of co-safe PCTL properties is decidable as well. This partially solves the PCTL satisfiability problem, which has been open for quite a long time [Br´azdil et al., 2008; Bertrand et al., 2012].

RelatedWork Stochastic planning with co-safe objectives has been studied in [Lacerda et al., 2014]. However, the properties under consideration are in linear-time and incomparable with co-safe properties in branching-time [Baier and Katoen, 2008]. In [Teichteil-K¨onigsbuch, 2012], planning problems with path constraints specified by PCTL were proposed. Different from our work, [Teichteil-K¨onigsbuch, 2012] restricted to memoryless strategies.

Related work also includes research on pATL and pATL∗ and their model checking issues [Chen and Lu, 2007; Huang et al., 2012; Huang and Luo, 2013]. However, we mention that for stochastic games pATL∗ and pATL still cannot express properties like the one in Eq. (1). Recall that a pATL formula in form of 〈〈A〉〉>q (φ) means that players in A can enforce a strategy such that φ is satisfied with probability greater than q no matter what other players do. In case there is only one player, it simply means that the player has a strategy such that φ will be satisfied with probability greater than q. At the first glance, it seems that probabilistic planning problems can be encoded by pATL. However, the semantics of pATL does not bind a unique strategy for players appearing in scopes of different qualifiers in form of 〈〈A〉〉>q (·). For instance, a natural choice for expressing the requirement in Eq. (1) is a pATL formula Φ1 ∧ Φ2, where Φ1 = 〈〈A1〉〉>0.2♦(c ⩾ 20)

and

with A1 = A2 = A3 = {G}. Note G appears for three times in Φ1 ∧ Φ2. In order to satisfy this formula, G can use different strategies when at A1, A2, and A3. For instance, suppose c = 10 initially, by choosing the optimistic button, G can satisfy ♦(c ⩾ 20) with probability 12 , i.e., Φ1 is satisfied. On the other hand, by a simple calculation, if the pessimistic button is always chosen, then Φ2 will be satisfied for any n > 0. Therefore, the whole formula is satisfied by choosing different strategies for G in A1 and A2,A3. However, this is different from our requirement (*) given before, where we would like to find a single strategy which satisfies the two requirements at the same time.

Organization of the Paper Section 2 introduces some preliminary notations. Co-safe PCTL is formally defined in Section 3. We show the decidability of stochastic games with co-safe PCTL objectives in Section 4, where strategies are deterministic. Section 5 generalizes results in Section 4 to randomized strategies, where robust planning problems are also addressed. We conclude the paper in Section 6.

2 Preliminaries

We introduce some preliminary notations. Let N be the set of nature numbers and N+ contain only positive ones. Let R be the set of real numbers, while Q contains only rationals. For a countable set S, let P(S) denote its powerset. A distribution is a function µ : S → [0, 1] satisfying ∑s∈S µ(s) = 1. Let Dist(S) denote the set of distributions over S. We shall use s, r, t, . . . and µ, ν, . . . to range over S and Dist(S), respectively. Let S∗ and Sω denote the set of finite and infinite sequences, respectively, over the set S. The set of all (finite and infinite) sequences over S is given by S∞ = S∗ ∪Sω . Let |π| denote the length of π ∈ S∗ . For i ∈ N, let π[i] denote the (i+1)-th element of π provided i < |π|, and π↓ = π[|π|-1] denote the last element of π provided π ∈ S∗ . The concatenation of π1 and π2, denoted π1 · π2, is the sequence obtained by appending π2 to the end of π1, provided π1 is finite. A sequence π1 is a prefix of π2, denoted π1 ⪯ π2, if there exists π ∈ S∞ (possibly empty, i.e., π ∈ S0 ) such that π1 ·π = π2. If π ̸∈ S0 , then π1 is a proper prefix of π2, denoted π1 ≺ π2. The set Π ⊆ S∞ is prefix-closed iff for all π1 ∈ Π and π2 ∈ S∗ , π2 ⪯ π1 implies π2 ∈ Π.

2.1 Probabilistic Models

In this subsection we recall some probabilistic models widely used in AI community. We shall first introduce the definition of Markov chain as below:

Definition 1. A Markov chain (MC) D = (S, ¯ s, P,AP,L) is a tuple where S is a countable set of states; ¯ s ∈ S is the initial state; P : S×S ↦→ ([0, 1]∩Q) is a transition matrix such that ∑t∈S P(s, t) = 1 for each s ∈ S; AP is a finite set of atomic propositions; and L : S → P(AP) is a labelling function.

A path π ∈ S∞ through an MC D is a (finite or infinite) sequence of states. The cylinder set Cπ of π ∈ S ∗

is defined as: Cπ = {π′ ∈ S ω | π ≺ π′}. The σalgebra F of D is the smallest σ-algebra containing all cylinder sets Cπ. By standard probability theory [Halmos, 1974; Rudin, 2006], there exists a unique probability measure Pr on F such that: Pr(Cπ) = 1 if π = ¯ s, and Pr(Cπ) = Π0⩽i<n P(si, si+1) if π = s0 . . . sn with ¯ s = s0 and n > 0; otherwise Pr(Cπ) = 0. We are restricted to rational probabilities in this paper, which is standard and essential to guarantee our decidability results.

While being fully probabilistic, MCs cannot handle systems involving decision-making. For these cases, Markov Decision Processes (MDPs) shall be introduced.

Definition 2. A Markov Decision Process (MDP) is a tuple M = (S, (S©, S□), ¯ s, E, P,AP,L), where ¯ s, AP, L are as in Definition 1 and S is a finite set of states; (S©, S□) is a partition of S with S© containing probabilistic states and S□ all controller states; E ⊆ S□ × S is a set of transitions; P : S© ×S ↦→ ([0, 1] ∩Q) is a probability function such that ∑t∈S P(s, t) = 1 for each s ∈ S©.

In Definition 2, we explicitly distinguish between probabilistic states and controller states which is typical in the setting of stochastic games, see for instance [Br´azdil et al., 2006]. A player at controller states has full flexibility to choose its successors, while at probabilistic states, successor states have to be chosen with probabilities given by the function P, hence a player at S© has limited flexibility. We mention that the distinguishing S□ and S© is only to ease the presentation. Actually, our definition of MDP is of no essential difference from the standard definition, as they can be transformed into each other directly. In the sequel we write P(s, ·) to denote the distribution such that P(s, ·)(t) = P(s, t) for each t ∈ S.

Due to existence of controller states, the notion of strategies has to be introduced in order to resolve all non-deterministic choices at controller states.

Definition 3. Let M be an MDP as in Definition 2. A strategy σ of M is a function such that for any π ∈ S ∗ with π↓∈ S□, σ(π) ∈ Dist(S), where σ(π)(s) > 0 implies (π↓, s) ∈ E for each s ∈ S.

Intuitively, a strategy takes a history execution as an input, represented as a finite path π, and decides for state π↓ the probabilities with which it should choose all its successors. Sometimes, the output of a strategy given a finite path will be referred as the decisions of the strategy.

Given an MDP M and a strategy σ of M, we can always induce an MC, denoted Mσ, for which a unique probability measure can be defined. As the inputs of a strategy, i.e., all history executions, are of infinitely many, the state space of the resultant MC may be infinite even if M is finite, which explains why in Definition 1 we are not restricted to MCs of finite states.

Depending on the information available when decisions are made, strategies can be classified into different categories according to criteria in Table 1: (i) Perfect recall v.s. Memoryless: Strategies whose decisions are based on the full history are with perfect recall. In contrast, a memoryless strategy σ makes decisions only based on the current state. Hence, all memoryless strategies can be written as a function

σ : S□ ↦→ Dist(S), and each MC induced by a memoryless strategy has the same state space as the original MDP. (ii) Randomized v.s. Deterministic: Strategies defined in Definition 3 are randomized, as decisions of strategies are distributions over successor states. In contrast, a deterministic strategy σ always chooses a successor with probability 1. The combinations of the above criteria result in four classes of strategies: Randomized with Perfect recall (RP), Randomized Memoryless (RM), Deterministic with Perfect recall (DP), and Deterministic Memoryless (DM).

2.2 Probabilistic CTL

Probabilistic Computation Tree Logic (PCTL for short, [Hansson and Jonsson, 1994]) is a branching-time logic for specifying properties of probabilistic systems. Its syntax is defined by the grammar:

where a ∈ AP, ▷◁ ∈ {<,>,⩽,⩾} is a binary comparison operator on the reals, q ∈ [0, 1], and n ∈ N+ ∪ {∞}. We will simply write U and W for U⩽∞ and W⩽∞ in the sequel. Let F := a ∧ ¬a denote false and T := ¬F denote true. As usual, ♦⩽nΦ := TU⩽nΦ, □⩽nΦ := ΦW⩽n F, and (Φ1 =⇒ Φ2) := (¬Φ1 ∨Φ2). We will refer to Φ and ϕ as state and path formulas, respectively. The satisfaction relation s |= Φ is defined in the standard manner for the Boolean connectives. For the probabilistic operator, it is defined by: s |= [ϕ]▷◁q iff Pr{π ∈ S ω (s) | π |= ϕ} ▷◁ q, where S ω (s) denotes the set of infinite paths starting from s. For an MC D, we write D |= Φ iff its initial state satisfies Φ, i.e., ¯ s |= Φ. The satisfaction relation for π ∈ S ω and ϕ is defined by: π |= XΦ iff π[1] |= Φ, π |= Φ1U⩽nΦ2 iff

π |= Φ1W⩽nΦ2 iff π |= Φ1U⩽nΦ2 ∨∀0 ⩽ i ⩽ n.π[i] |= Φ1. The until U and weak until W modalities are dual:

Eq. (2) also holds if we: i) replace ⩾ and ⩽ with > and <, and/or ii) replace U and W with bounded until U⩽n and bounded weak until W⩽n , respectively. By applying duality laws, every PCTL formula can be transformed into an equivalent PCTL formula in positive normal form. A formula is in positive normal form, if negation only occurs adjacent to atomic propositions. In the sequel, we assume PCTL formulas to be in positive normal form.

2.3 Probabilistic Trees

In this subsection we introduce the notion of probabilistic trees [Katoen et al., 2014], which are closely related to MCs, as each MC can be equivalently represented as a probabilistic tree. Let A, B, . . . range over P(AP), where {a} is abbreviated by a. Let ϵ be the empty sequence.

Definition 4. A probabilistic tree (PT) over a set of states S is a tuple T = (W, L, P) where ϵ ̸∈ W, and (W ∪{ϵ}) ⊆ S∗ is prefix-closed and there exists one (and only one) π ∈ W such that |π| = 1; L : W ↦→ P(AP) is a node labelling function; P : W ↦→ Dist(W) is an edge labelling function, which is a partial function satisfying P(π)(π′ ) > 0 iff π′ = π · s ∈ W for some s ∈ S.

The node π with |π| = 1 is referred to as the root 1 , while all nodes π such that ∀π′ ∈ W.π ̸≺ π′ are referred to as the leaves. A PT T = (W,L,P) is total iff for each π1 ∈ W there exists π2 ∈ W such that π1 ≺ π2. T is finite-depth if there exists n ∈ N such that |π| ⩽ n for each π ∈ W. The least such n is called the depth of T . Let Tω and T∗ denote the sets of all total PTs and finite-depth PTs respectively.

Below defines a prefix relation on PTs [Katoen et al., 2014], where ↾ denotes restriction.

Definition 5. Let Ti = (Wi, Li, Pi) for i=1, 2 with T1 ∈ T∗ and T2 ∈ Tω . T1 is a prefix of T2, denoted T1 ⪯ T2, iff W1 ⊆ W2 and L2 ↾ W1 = L1 and P2 ↾ (W1 ×W1) = P1. Let Prefin(T) denote the set of all prefixes of T ∈ Tω .

It is not hard to see each MC D can be unfolded into a total PT, denote T (D). Conversely, any PT can be seen as an MC with infinite many states. Therefore, the satisfaction relation between PCTL formulas and total PTs can be defined directly. Such satisfaction relation can also be lifted to finite-depth PTs in T∗ in a natural way: Let Φ be a PCTL formula and T1 ∈ T∗ . T1 satisfies Φ, denoted T1 |= Φ, iff T2 |= Φ for any T2 ∈ Tω such that T1 ∈ Prefin(T2). Intuitively, the finite-depth PT T1 suffices to conclude that Φ is satisfied regardless of the remaining execution. We say that Φ always has finite-depth witnesses iff for any MC D such that D |= Φ, there exists T1 ∈ Prefin(T(D)) such that T1 |= Φ.

3 Safety and Co-safety Properties

The distinction of safety and liveness properties is pivotal for verifying reactive systems. As Lamport introduced in 1977 [Lamport, 1977; Alford et al., 1985], safety properties assert that something "bad" never happens, while liveness properties require that something "good" will happen eventually. For stochastic properties, PCTL formulas have been classified into safety and liveness in [Katoen et al., 2014]. In this paper, we are mainly interested in co-safe PCTL, i.e., formulas whose negations are safe PCTL.

Definition 6. The safe and co-safe fragments of PCTL, denoted PCTLs and PCTLcs respectively, are defined by the following grammar, where n ∈ N, φ, φ1, . . . and Φ, Φ1, . . . range over formulas in PCTLs and PCTLcs , respectively.

We note that for bounded until and weak until, ▷◁ can be any operator in {<,>,⩽,⩾}. Since ¬[Xφ]⩾q ≡ [Xφ]<q ≡

1 For technical reasons, ϵ is excluded from the tree.

[X¬φ]>1-q, together with Eq. (2), it is easy to check that the negation of each formula in PCTLs has an equivalent representation in PCTLcs and vice versa. Also note the membership of PCTLs and PCTLcs can be determined pure syntactically. For instance, F and T are both safe and co-safe; [□φ]⩾q = [φWF]⩾q is safe, provided φ ∈ PCTLs , while [♦Φ]>q = [TUΦ]>q is co-safe, provided Φ ∈ PCTLcs . In this way, PCTLcs subsumes reachability properties with strict lower bounds. Note the formula in Eq. (1) also belongs to PCTLcs , provided that we have atomic propositions such as c ⩾ 20 and c = 0. Below is a theorem from [Katoen et al., 2014] showing that the definitions of PCTLs and PCTLcs are both sound and complete.

Theorem 1 ([Katoen et al., 2014, Thm. 4 and 5]). All formulas in PCTLs (PCTLcs resp.) are safe (co-safe resp.), while each safe (co-safe resp.) property expressible in PCTL has an equivalent formula in PCTLs (PCTLcs resp.).

Expressiveness of co-safe PCTL We mention that many patterned properties classified in [Grunske, 2008] can be expressed in PCTLcs . For instance,

• Probabilistic Invariance. The probability of no error occurring in the next n steps is at least 0.99: [□⩽n (no error)]⩾0.99.
• Probabilistic Existence. If an error occurs, it will be solved eventually with probability greater than 0.95: error =⇒ [♦solved]>0.95.
• Probabilistic Until. With probability greater than 0.95, the alarm should be on until the problem is solved: [alarmOnU(alarmOff ∧ solved)]>0.95.
• Probabilistic Response. With probability greater than 0.99, during the lifetime (m) of a robot, whenever it is out of battery (A), it will be fully recharged (B) in the next n steps: [□⩽m(A =⇒ [♦⩽nB]⩾1)]⩾0.99.

Particularly, since PCTLcs is closed under conjunction, multi-objective properties [Wakuta and Togawa, 1998; Refanidis and Vlahavas, 2003; Wiering and De Jong, 2007; Khouadjia et al., 2013; Wray et al., 2015] can be directly expressed in PCTLcs by properly choosing atomic propositions. If given more than one objective, we can put them together in conjunction and find a strategy fulfilling all of them at the same time.

Remark 1. According to Definition 6, [♦solved]>0.95 is cosafe, while [♦solved]⩾0.95 is not. Such a subtle difference between > and ⩾ is of theoretic importance, as the probability of reaching "solved" may converge to 0.95 in infinite steps, but the probability of reaching "solved" is strictly less than 0.95 in any finite steps. However, as shown in [Chatterjee and Henzinger, 2008], in a finite MDP where all transition probabilities are rational, reachability probabilities can be computed precisely in finite steps. Therefore, in practice, the algorithms we shall introduce later can also be applied to properties with non-strict bounds, i.e., those definable by the PCTLcs grammar in Definition 6 with additional operators [XΦ]⩾q, [φ1Wφ2]⩽q, and [Φ1UΦ2]⩾q.

4 Stochastic Games with Perfect Recall

In this section we introduce stochastic games [Baier et al., 2004; Kucera and Strazovsk´y, 2008; Br´azdil et al., 2006] formally. If general PCTL objectives are considered, stochastic games with perfect recall turn out to be highly undecidable [Br´azdil et al., 2006] even for finite models. Therefore, we mainly focus on games whose objectives are restricted to PCTLcs . Even though DP ⊊ RP, these two sets of strategies are usually studied separately, as winning strategies with or without randomization make differences for PCTL objectives [Baier et al., 2004]. We show in this section that stochastic games with PCTLcs objectives are decidable even if strategies in DP are considered. Below defines stochastic games formally:

Definition 7. Let M be an MDP as in Definition 2 and Φ ∈ PCTLcs . Let XX range over the set {RP, RM, DP, DM}. The stochastic game over M has a winning strategy in XX for the given objective Φ iff there exists a XX-strategy σ such that Mσ |= Φ. A XX stochastic game answers whether or not a winning strategy in XX exists for a given objective.

We shall fix an MDP M throughout the remaining part of this paper. As we mentioned, DP stochastic games are undecidable in general for objectives specified by PCTL. This is mainly due to the fact that some objectives only have winning strategies using infinite memories. By restricting to PCTLcs objectives, however, finite memories suffice as shown in the following lemma [Katoen et al., 2014].

Lemma 1. Formulas in PCTLcs have finite-depth witnesses.

Lemma 1 ensures that a winning strategy only requires finite memories for objectives in PCTLcs . However, it does not give us an upper bound for the size of the memory. Fortunately, such bounds can be established. For this, we first introduce some notations. In the following, we assume all probabilities are expressed as irreducible fractions.

Definition 8. Let m be the number of transitions of M; d the largest denominator among all transition probabilities appearing in M; θ the least common multiple of all denominators; p the largest numerator of all transition probabilities; and γ = d4m · θ · p.

It was shown in [Chatterjee and Henzinger, 2008] that maximal and minimal reachability probabilities can be computed precisely in at most O(γ 2 ) iterations. We show in the following lemma that such bound also holds for the size of memory used by a winning strategy, if exists, in a DP stochastic game.

Lemma 2. Given an objective Φ ∈ PCTLcs , whenever the DP stochastic game has a winning strategy σ, there exists T1 ∈ Prefin(Mσ) with depth O(|Φ| · γ 2 ) such that T1 |= Φ, where |Φ| denotes the length of Φ.

Proof. The proof is by structural induction on Φ. Let depth(Φ) denote the least depth of finite-depth witnesses of Φ in M. We only show proofs of several non-trivial cases:

• Φ = [Φ1UΦ2]>q. Then we show that depth(Φ) = depth(Φ1) + c + depth(Φ2), where c ∈ O(γ 2 ). Essentially, the result in [Chatterjee and Henzinger, 2008] ensures that reachability probabilities in an MC D can

be computed precisely by considering a prefix of T (D) of depth c ∈ O(γ 2 ). By induction hypothesis, a tree of depth depth(Φ1) suffices to witness all states satisfying Φ1. According to [Chatterjee and Henzinger, 2008], by extending all prefixes for c steps, we make sure all strategies which can reach states satisfying Φ2 with probability > q can be found. To ensure that all states satisfying Φ2 will be found, further extensions up to depth(Φ2) would be enough by induction hypothesis.

• Φ = [φ1Wφ2]<q. By duality law, Φ ≡ [(φ1 ∧ ¬φ2)U(¬φ1 ∧ ¬φ2)]>1-q. We show that depth(Φ) = depth(¬φ2) + c + depth(¬φ1 ∧ ¬φ2). Note ¬φ1 and ¬φ2 are co-safe formulas. Therefore, prefixes of depth depth(¬φ2) suffice to find all states satisfying ¬φ2 by induction hypothesis. Consequently, all states satisfying φ1 ∧ ¬φ2 can be found, which is a subset of states satisfying ¬φ2. The remaining proof is then similar as the above case.

This completes the proof.

Due to Lemma 2, the decidability of DP stochastic games with PCTLcs objectives is easy to establish.

Theorem 2. DP stochastic games with PCTLcs objectives are decidable and in 3-EXPTIME.

Proof. Let M and Φ ∈ PCTLcs be given. First, we unfold M to a PT up to a certain step. Let Mi denote the resultant model at the i-th step of unfolding. In Mi , it suffices to enumerate all possible DM strategies, which are finitely many. We continue unfolding M until either a winning strategy is found, or for each state s ∈ S and path formula ϕ in Φ, the change of the probability of s satisfying ϕ is less than 1 2γ [Chatterjee and Henzinger, 2008], comparing to the previous valuation. As Φ ∈ PCTLcs , the termination of this process is guaranteed by Lemma 2.

The above procedure will cause a triply exponential blowup: Since we may need to unfold M up to an exponential number i of steps and hence may result in an MDP Mi doubly exponentially larger than the original model. Furthermore, the number of DM strategies of Mi is exponentially many with respect to the size of Mi . Therefore, the whole algorithm is in 3-EXPTIME.

It is not surprising that the problem is of high complexity, since even DM stochastic games are NP-complete, and DP stochastic games with linear time objectives are elementary [Baier et al., 2004].

5 Stochastic Games with Perfect Recall and Randomization

In this section we focus on RP stochastic games with PCTLcs objectives. Unfortunately, Theorem 2 does not hold if RP strategies are considered. This is because randomized strategies can assign arbitrary probabilities to successor states, hence parameters d, θ, and p in Definition 8 cannot be defined directly. On the other hand, robustness of strategies has been argued by many authors to be a natural requirement in probabilistic systems, see for instance [Nilim and Ghaoui, 2005; Kucera and Strazovsk´y, 2008]. In the remaining of this section we will define robustness of strategies along the line of [Kucera and Strazovsk´y, 2008] and then show that it is decidable to determine whether or not a robust winning strategy exists. Finally, we show that as special cases of robust RP stochastic games (when tolerance is equal to 0), RP stochastic games are decidable too. As we shall show, this also implies that satisfiability of PCTLcs is decidable.

We follow definitions in [Kucera and Strazovsk´y, 2008] and define strategy robustness for RP stochastic games.

Definition 9. Let σ, σ′ be two RP strategies of a stochastic game with respect to an objective Φ ∈ PCTLcs . We say that

1. σ′ is a δ-perturbation of σ if for all π ∈ S ∗ with π↓∈ S□ and t ∈ S: a) |σ(π)(t) - σ′ (π)(t)| ⩽ δ and b) σ(π)(t) = 0 iff σ′ (π)(t) = 0, where δ ∈ (0, 1) ∩ Q;
2. σ is a δ-robust winning strategy iff for any RP strategy σ′ , whenever σ′ is a δ-perturbation of σ, it is a winning strategy of the stochastic game too.

Intuitively, a strategy σ′ is a δ-perturbation of σ iff at each step the probability of σ′ choosing a state is within [q-δ, q+δ], where q is the probability of σ choosing the same state. Moreover, for technical reasons, an extra condition is imposed, which essentially guarantees that all states chosen by σ with positive probabilities should also be chosen by σ′ with positive probabilities. This condition is necessary to preserve qualitative structures, i.e., topologies of MCs [Courcoubetis and Yannakakis, 1995] induced by strategies which are δ-perturbations of each other.

In the sequel we focus on robust RP stochastic games with PCTLcs objectives: Given a δ ∈ (0, 1) ∩ Q and an objective Φ ∈ PCTLcs , decide whether or not a δ-robust RP winning strategy exists for the stochastic game. We show that robust RP stochastic games can be solved by using the algorithm in [Kucera and Strazovsk´y, 2008], denoted MRGame, as an oracle. MRGame solves RM stochastic games with PCTL objectives by reducing them to the decidable problem - first order theory of reals (R, +, ∗, ⩽) [Tarski, 1951]. For similar reasons as in Section 4, MRGame cannot be extended to deal with RP strategies directly. Below is a theorem showing another main result of this paper:

Theorem 3. For a given δ ∈ (0, 1) ∩ Q, robust RP stochastic games with PCTLcs objectives are decidable.

So far, we require δ > 0. In the sequel we discuss the special case when δ = 0, i.e., RP stochastic games. It is easy to see that arguments used in Theorem 3 do not apply when δ = 0, as in principle a strategy can assign arbitrarily small probabilities to some states. However, we can prove a lemma showing that if there is a winning strategy for an RP stochastic game, then we can always find a winning strategy where the largest denominator of all probabilities assigned by the strategy to all states is bounded.

Lemma 3. Let Φ ∈ PCTLcs be an objective. There is an RP winning strategy for Φ, iff there exists D ∈ N+ and a winning strategy σ such that for any π ∈ S ∗ with π↓∈ S□ and t ∈ S, σ(π)(t) = kD , where k ∈ [0,D] is an integer.

Proof. The sufficiency is trivial. To prove the necessity part, let σ be a winning strategy for Φ and T1 ∈ Prefin(T(Mσ)) such that T1 |= Φ. For each node π in T1, we denote PrT1 π (ϕ) the probability of π satisfying ϕ in T1, where ϕ is a path formula in Φ. Let dσ be the greatest denominator of all PrT1 π (ϕ) including all bounds in Φ and odM the greatest outdegree of states in M. For k ∈ N and q ∈ [0, 1], we denote ⌊q⌋k = k′ k , where k′ is the greatest integer such that k′ k ⩽ q. Let σ′ be a strategy such that σ′ (π)(t) = ⌊σ(π)(t)⌋D and σ′ (π)(dummy) = 1 - ∑t∈S σ′ (π)(t), where D is any integer greater than 2 · odM · dσ and dummy denotes a deadlock state. The reason to introduce dummy is that by letting σ′ (π)(t) = ⌊σ(π)(t)⌋D for each π and t, the sum of probabilities assigned by σ′ to all successors may be less than 1. Therefore, we have to add an extra transition to the dummy state with the remaining probability to make sure that σ′ gives rise to a distribution at each step. Let T ′1 be the prefix of Mσ′ of the same depth as T1. It shall be easy to see that for each node π and path formula ϕ in Φ,

As dσ is the greatest denominator of all Prπ(ϕ) including all bounds in Φ, T1 |= Φ implies T ′1 |= Φ, hence σ′ is also a winning strategy.

Let D ∈ N+ be a positive integer. We call a strategy σ a D-strategy if all probabilities assigned by σ to states are in form kD with k ∈ [0, D] being an integer. Given a D and i, it is easy to see that the number of D-strategies of Mi in DM is finite. Below is a theorem showing that RP stochastic games with PCTLcs objectives are decidable, which can be proved in a similar way as Theorem 3.

Theorem 4. RP stochastic games with PCTLcs objectives are decidable.

As a byproduct of Theorem 4, the satisfiability of PCTLcs is decidable.

Theorem 5. Let Φ be a formula in PCTLcs . The following problem is decidable: Checking whether Φ is satisfiable, i.e., whether there exists an MC D such that D |= Φ.

To the best of our knowledge, until now, the problem of deciding whether or not a given PCTL formula is satisfiable is still open and only partial results are known [Br´azdil et al., 2008; Bertrand et al., 2012].

6 Conclusion and FutureWork

We have considered stochastic games with branching-time objectives, where strategies are deterministic or randomized, and always with perfect recall. While undecidable in general, we showed that the problem can be solved if restricted to PCTLcs objectives, which cover many interesting properties in practice as we have shown. Robust stochastic games were also studied. Our result indicates that satisfiability of PCTLcs is decidable.

There are several directions for future work, e.g., the complexity of these problems and other fragments of PCTL which make stochastic games with perfect recall decidable.

Acknowledgments

The authors are supported by Australian Research Council under Grant DP130102764, the National Natural Science Foundation of China (Grant Nos. 61428208, 61472473 and 61361136002), AMSS-UTS Joint Research Laboratory for Quantum Computation, Chinese Academy of Sciences, and the CAS/SAFEA International Partnership Program for Creative Research Team.