{'fraction_non_alphanumeric': 0.06941789422392143, 'fraction_numerical': 0.01394355110761273, 'mean_word_length': 3.440745672436751, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 20, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Simple Probabilistic Extension of Modal Mu-calculus

Probabilistic systems are an important theme in AI domain. As the specification language, the logic PCTL is now the default logic for reasoning about probabilistic properties. In this paper, we present a natural and succinct probabilistic extension of mu-calculus, another prominent logic in the concurrency theory. We study the relationship with PCTL. Interestingly, the expressiveness is highly orthogonal with PCTL. The proposed logic captures some useful properties which cannot be expressed in PCTL. We investigate the model checking and satisfiability problem, and show that the model checking problem is in UP and co-UP, and the satisfiability checking can be decided via reducing into solving parity games. This is in contrast to PCTL as well, whose satisfiability checking is still an open problem.


Introduction
Modal µ-calculus receives a lot of attraction in classical model checking and temporal logic theory, ever since Kozen's seminal work [20]. See for example, [2,19,32,3]. Moreover, various temporal logics including LTL [27], CTL [12], CTL* [13] are extensively studied. It is known that their expressiveness is strictly less [10] than µ-calculus (aka. µTL), and their model checking algorithm has been proposed: for CTL the problem can be solved in polynomial time, whereas for LTL the problem is PSPACE-complete [30].
Probabilistic systems, such as Markov chains and Markov decision procedures, are always an important AI domain. To reason about properties for probabilistic systems, the logic CTL was first extended with probabilistic quantifiers in [16] , resulting in the logic PCTL. Intuitively, (aU ≥0.9 b) means that the probability of reaching b-states along a-states is at least 0.9. At the same time, probabilistic LTL and its extension PCTL* has all been studied. As in the classical setting, model checking problem for PCTL can be solved in polynomial time, whereas only exponential algorithms are known for LTL [9]. There have also been several attempts to extend µTL with probabilities in the literature. As we shall discuss in the related work, the extensions are either highly nontrivial in terms of the complexity of the corresponding model checking and satisfiability problems, or hindered from the restriction of fixpoint nestings. This paper proposes a natural and succinct extension of µTL. We equip the next operator with probability quantifiers, and keep other parts of the logic. We have for instance the formula νZ.(a ∧ X ≥0.8 Z). As we will see in the later, this property cannot be expressed by any PCTL formula.
We then study the relationship with PCTL, and prove that the expressiveness is orthogonal with PCTL. However, for the qualitative fragments (i.e., probabilities may appear in a formula are only 0 and 1), we prove that qualitative PCTL is a proper subset of qualitative PµTL (upon finite Markov chains). Then, we investigate the model checking and satisfiability decision of PµTL upon Markov chains. The model checking problem turns out to be a straightforward adaptation of the classical algorithms, and the complexity remains in UP ∩ co-UP. On the other side, the satisfiability checking is quite challenging: we exploit the notion of probabilistic alternating parity automata (PAPA, for short), and reduce the satisfiability problem into the Emptiness problem of PAPA. Further, this is reduced to solving parity games. This is in contrast to PCTL as well, whose satisfiability checking is still an open problem [6,4].
An illustrating example We introduce a running example to motivate our work: Suppose there is a hacker tries to attack a remote server. The hacker has a supercomputer at hand and is trying to guess the password in a brute-force manner. For simplicity, we assume the password is a sequence of l letters, each of which is from '0'-'9', 'a'-'z', and 'A'-'Z'. Therefore, the total number of possible passwords is n = 62 l . The hacker let the supercomputer randomly generate a password, and see whether the decryption succeeds. If yes, the hacker wins and stops; otherwise he tries with another one. However, due to security reasons, if the supercomputer generates three wrong passwords in a row, it will be blocked for a certain amount of time until it can start another round of attacking -note that the password may be changed during the blocked moment, hence it does not make sense for the supercomputer to store all generated passwords. The whole process is illustrated in Fig. 1. Starting from s 1 , we can see that the probability of eventually reaching attacked, i.e., the hacker decrypts successfully, equal 1, no matter how big l is (hence, the PCTL formula F ≥1 attacked holds), and we may conclude that the system is unsafe -this is of course against our intuition, and such system is considered to be safe if l is big enough. However, as we will show later, all existing specification languages are not capable of expressing this fact. By making use of PµTL, such property of security can be characterized easily as follows: νZ.(¬attacked ∧X ≥p Z)) with p = n−3 /n−2, where ¬attacked denotes all other states in Fig. 1 different from s 5 .
Motivation from AI perspective The presented logic has the following potential application in AI domain: -First of all, Markov chains and Markov decision procedures are the basic models in several areas of AI. As a logic whose semantics is defined w.r.t. such models, the presented logic could definitely be used in designating probability-relevant properties upon them. Particularly, the properties that could not be expressed by PCTL. -Motion planing is an important topic in AI area, where standard µTL has once been adopted [5], because of its powerful expressiveness and the decidability of its Satisfiability problem. Then, it is no wonder that PµTL could be used in stochastic motion planning -because, PµTL is a decidability-preserving extension of µTL. -Fixpoints act an important role in mathematics and computer science. For AI areas, fixpoints are useful to specify non-terminating behaviors of intelligent systems, for instance, maintenance goals [29]. In PµTL, fixpoints act as the core ingredients, hence such logic can also be used in such a situation.
Related work Probabilistic extensions of µTL have been studied by many authors: e.g., µ-calculi proposed in [26,17,11,22,23,25] interpret each formula as a function from states to real values in [0, 1], whose semantics is different from PµTL. A further extension of µ-calculus was proposed in [24], which is able to encode the full PCTL. However, model checking and satisfiability algorithms are still unknown for these calculi and are "far from trivial" [25]. The other probabilistic µ-calculus was introduced in [8] along with a model checking algorithm for it. Moreover, it is able to encode PCTL formulae as well. However, the calculus in [8] only allows alternation-free formulae (cf. [14]), hence its expressiveness is limited and incomparable with PµTL. Very Recently, Castro, Kilmurray, and Piterman present another extension by investigating fixpoints to full PCTL [7]. To some extent, that is a proper super logic of PµTL. They show the model checking problem is in NP ∩co-NP. However, since that logic subsumes PCTL, its Satisfiability problem is also left open.

Preliminaries
In this paper, we fix a countable set A of atomic propositions, ranging over a, b, a 1 etc, and fix a countable set Z of formula variables, ranging over Z, Z 1 etc. . . , s n )) equals 0 if s s 0 , and equals i<n T(s i , s i+1 ) otherwise. We say a set P ⊆ Π M,s is measurable if P ∈ ∆ M,s . [31] shows that the intersection of Π M,s and an omega-regular set must be measurable.
The syntax of PCTL formulae is described by the following abstract grammar: where ∼∈ {>, ≥} and p ∈ [0, 1]. We also abbreviate ⊤U ∼p f and ⊥R ∼p f as F ∼p f and G ∼p f , respectively. Semantics of a PCTL formula is given w.r.t. a Markov chain. For each PCTL formula f and a Markov chain M = (S , T, L), we will use f M to denote the subset of S satisfying f , inductively defined as follows.
In addition, for an infinite path π = s 0 ,

PµTL, Syntax and Semantics
In this section we present a simple probabilistic extension of modal µ-calculus, called PµTL. The syntax of PµTL formulae is depicted as follows: Semantics of a PµTL formula is given w.r.t. a Markov chain M = (S , T, L) and an assignment e : Z → 2 S . Similarly, for each PµTL formula f , we denote by f M (e) the state set satisfying f under e. Inductively: and Indeed, µZ. f M (e) (resp. νZ. f M (e)) could be computed as in the classical setting via the following iteration: Note that the algorithm obtains a monotonic chain with such an iteration, and hence it must terminate within finite steps. Actually, µZ. f M (e) (resp. νZ. f M (e)) captures the least (resp. greatest) solution of Semantical definition of PµTL formulae also yields the model checking algorithm.

Theorem 1. The model checking problem of PµTL is in UP ∩co-UP.
Indeed, the proof is analogous to the non-probabilistic version [18,33] and the only noteworthy difference lies from handling X ∼p -subformae, opposing to -and -subformulae, which could be proceeded in (deterministic) polynomial time.
In what follows, we directly denote by f M in the case that f is a closed formula (i.e., each variable of f is bound), and we also denote by Below we give some example properties (some of them are also mentioned in [7]): (1) The formula νZ.(a∧X >0.5 Z) describes that there exists an a-region, where each state has less than 0.5 probability to escape from it immediately (i.e., in one step). (2) νZ.(a ∧ X >0 X >0 Z) says that there is a cycle in the Markov chain, such that a holds at least in every even step.
if some a-state is reachable from s, but at each step, one just has some probability (not less than 0.6) to go on with the right direction. (4) The PµTL formula µZ.(b ∨ (a ∧ X ≥1 Z)) holds if aUb holds along each path. It is stronger than the property described by the PCTL formula aU ≥1 b. For the latter allows the existence of a-cycles. (5) As a more complicated example, the formula νZ 1 .(a ∨ µZ 2 .(a ∨ X >0 Z 2 ) ∧ X ≥1 Z 1 ) just tells the story that "a will be surely encountered", as described by F ≥1 a with PCTL.
Given a PµTL formula f and a bound variable Z, we use D f (Z) to denote the sub- We say that a PµTL formula f is guarded, if the occurrence of each bound variable Z in D f (Z) is in the scope of some X-operator. The following theorem could be proven in a same manner as that in [32]. Thus, in what follows, we always assume that each PµTL formula is guarded.

Expressiveness
In this section, we will give a comparison between PµTL and PCTL, and we are only concerned about closed PµTL formulae. For a PµTL formula f and a PCTL formula g, we say that f and g are equivalent if f M = g M for every Markov chain M, denoted as f ≡ g.
First of all, we will show that some PµTL formula could not be equivalently expressed by any PCTL formula.
, then g f for every PCTL formula g.
Proof. To show this, we need first construct two families of Markov chains, namely, For the second ones, let Given a PCTL formula g, let N(g) be the maximal nesting depth of temporaloperators of g. According to [1,Thm. 10.45], we have that M ′ n , s ′ n | = g if and only if M n , s n | = g whenever n ≥ N(g).
Observe the fact that M ′ n , s ′ n | = f and M n , s n | = f for every n ≥ 1. Assume that there exists some PCTL formula g fulfilling f ≡ g, then we have and hence it results in a contradiction! In [7], a proof for f = νZ.(a ∧ X >0 Z) is also provided. Conversely, the following theorem reveals that there also exists some PCTL formula that could not be equivalently expressed by any PµTL formula. For every PCTL and/or closed PµTL formula g, we let P x (g) be the proposition that "for the fixed x, there are infinitely many y making M, s 1 | = g and there are infinitely many y making M, s 1 | = g". We now show that if g is a closed PµTL formula, then there exists some x g < 1 such that P x (g) does not hold whenever x ∈ (x g , 1).
-Such x g can be arbitrarily chosen if g = ⊥, g = ⊤, g = a or g = ¬a.
-In the case that g = g 1 ∧g 2 , assume by contradiction that such x g does not exist, then it implies that for every x ∈ (0, 1), there exists some x ′ > x such that P x ′ (g) holds.
Observe that M, s 1 | = g implies both M, s 1 | = g 1 and M, s 1 | = g 2 ; and M, s 1 | = g implies either M, s 1 | = g 1 or M, s 1 | = g 2 . Thus, we can infer that either x g 1 or x g 2 does not exist, which violates the induction hypothesis. -Proof for the case of g = g 1 ∨ g 2 is similar to the above.
-If g = X ∼p g ′ and p ∈ (0, 1), whenever x ∈ (max{p, 1 − p}, 1) note that ∼∈ {>, ≥}, then M, s 1 | = g iff M, s 1 | = g ′ because y + z < p in such situation. In this case, we may just let x g = max{x g ′ , p, 1 − p}. -If g = X ≥1 g ′ , then we need to distinguish two cases: 1) There exist x, y ∈ (0, 1) such that M, s 1 | = g holds, then we can immediately infer that both M, s 2 | = g ′ and M, s 3 | = g ′ . In addition, observe that truth values of g ′ on s 2 and s 3 are irrelevant to x and y. It implies that in such case M, s 1 | = g iff M, s 1 | = g ′ , and hence, we may just let x g = x g ′ . 2) There is no such x and y having M, s 1 | = g holds, in such situation, x g can be any number in (0, 1). -If g = X >0 g ′ , then the proof is similar to the above.
-When g = X ≥0 g ′ (or g = X >1 g ′ ), things would be trivial, because g could be reduced to ⊤ (resp. ⊥) in such case.
Since that M is a 3-state Markov chain, then g and i≤3 g i share the same truth value at every state of M. This indicates that all least fix-points could be eliminated w.r.t. such Markov chain. -When g = νZ.g ′ , the preprocessing is almost similar, but we just replace g with Note that the value 0.5 in the previous two theorems can be generalized to any other probability p ∈ (0, 1).
We also provide a comparison on the qualitative fragments of PCTL and PµTL. Probabilities occurring in such fragments can only be 0 or 1.

Theorem 5. Every qualitative PCTL formula can be equally expressed by a qualitative PµTL formula.
Proof. We will give a constructive translation procedure, which takes a qualitative PCTL formula g and outputs an equivalent qualitative PµTL formula g. Inductively: 1. g = ⊥ if g = ⊥, or its root operator is X >1 , U >1 or R >1 ; g = ⊤ if g = ⊤, or its root operator is X ≥0 , U ≥0 or R ≥0 . 2. g = g 1 ∧ g 2 if g = g 1 ∧ g 2 ; and g = g 1 ∨ g 2 if g = g 1 ∨ g 2 .
The proof of equivalence could be done by induction on the structure of the formula.
Note that Thm. 5 only works for finite models. Interested readers may show that it is not true for infinite Markov chains. , s ′′ i ) = 1 for each i < n. In addition, L ′′ n (s ′′ i ) = {a} for each i 1, and L ′′ n (s ′′ 1 ) = ∅. For a given PCTL formula g, letĝ be the LTL formula obtained from g by discarding all probability quantifiers, e.g., we haveĝ = aU(b ∨ G¬a) if g = aU ≥0.3 (b ∨ G >0.6 ¬a). Since that from s ′′ n the Markov chain M ′′ n has exactly one infinite path π n = s ′′ n , . . . , s ′′ 1 , (s ′′ 0 ) ω , then for each n ≥ 2 we have M ′′ n , s ′′ n | = g if and only if π n | =ĝ. It is shown in [34] where N ′ (g) and N ′ (ĝ) are the nesting depth of X-operator of g andĝ, respectively. Thus, we have M ′′ n , s ′′ n | = g iff M ′′ n+1 , s ′′ n+1 | = g in such situation. This implies that νZ.(a ∧ X >0 X >0 Z) has no equivalent qualitative PCTL expression, because we cannot simultaneously have M ′′ n , s ′′ n | = f and M ′′ n+1 , s ′′ n+1 | = f for each n ≥ 2.
Indeed, the proof of Thm. 6 also works for general PCTL formulae, and hence the property νZ.(a ∧ X >0 X >0 Z) even cannot be expressed by any PCTL formula.

Automata Characterization
In this section, we will define a new type of automata recognizing (pointed) Markov chains, called probabilistic alternating parity automata (PAPA, for short), and such automata could be viewed as the probabilistic extension of those defined in [33].
A PAPA A is a tuple (Q, q 0 , δ, Ω) where: Q is a finite set of states. q 0 ∈ Q is the initial state. δ is the transition function, to be defined later. Ω : Q N, is a partial function of coloring; in what follows, we say a state is colored if Ω is defined for the state.
The notion of transition conditions over Q is inductively defined as follows: 1. ⊥ and ⊤ are transition conditions over Q.
2. For every a ∈ A, the literals a and ¬a are transition conditions over Q.
3. If q ∈ Q, then q is a transition condition over Q. 4. If q ∈ Q and p ∈ [0, 1], then ∼p q is a transition condition over Q, where ∼∈ {≥, >}. 5. If q 1 , q 2 ∈ Q then both q 1 ∨ q 2 and q 1 ∧ q 2 are transition conditions over Q.
The transition function δ assigns each state q ∈ Q a transition condition over Q. We denote by R A the derived graph of A, its vertex set is just Q, and there is an edge from q 1 to q 2 iff q 2 appears in δ(q 1 ). We say that A is well-structured, if for every path q 1 , q 2 , . . . , q n that forms a cycle (i.e., q 1 = q n ) in R A , we have that: 1). there exists some 1 ≤ i < n such that δ(q i ) = ∼p q i+1 with some p ∈ [0, 1]; 2). there exists some 1 ≤ j < n such that q j is colored. In what follows, we are only concerned about well-structured PAPA.

Proof. We just let
: = a and δ f (q ¬a ) = ¬a; • δ f (q g 1 ∧g 2 ) = q g 1 ∧ q g 2 and δ f (q g 1 ∨g 2 ) = q g 1 ∨ q g 2 ; • δ f (q X ∼p g ) = ∼p q g ; • δ f (q µZ.g ) = q g and δ f (q νZ.g ) = q g ; -Ω f is defined at every state q Z with Z ∈ Z fulfilling: If Z is a µ-variable (resp. ν-variable), then Ω f (q Z ) is the minimal odd (resp. even) number which is greater It could be directly examined that A f is well-structured since f is guarded. The proof of equivalence can be similarly done as that in [33] -the only different induction step is to deal with transitions being of ∼p q (in that paper, the corresponding cases are q and q). Actually, we can see that if a PAPA (Q, q, δ, Ω) corresponds to the PµTL formula g, then the PAPA (Q ∪ {q ′ }, q ′ , δ[q ′ → ∼p q], Ω) must correspond to X ∼p g.

Satisfiability Decision
It is known from Section 5 that the Satisfiability problem of PµTL could be reduced to the Emptiness problem of PAPA. In this section, we will further reduce it to parity game solving.
A parity game G is a tuple (V, E, C), where: V is a finite set of locations, and V could be partitioned into two disjoint sets V 0 and V 1 ; E ⊆ V × V is the set of moves, required to be total; and C : V N is a partial function of coloring, and we say a location v is colored, if C(v) is defined. In addition, for the game G, we require that each loop involves at least one colored location. Two players -player 0 and player 1, are respectively in charge of V 0 and V 1 when G is being played. A play of G starting from v 0 ∈ V is an infinite sequence of locations v 0 , v 1 , . . . made by player 0 and player 1 -for every i ∈ N, the location v i+1 is chosen by player 0 (resp. player 1) with Player 0 (resp. player 1) wins the play v 0 , v 1 , . . . if the maximal color occurring infinitely often in it is even (resp. odd) -and we say that a color c occurs in this play if there is some v i with C(v i ) = c.
A winning strategy for player i is a mapping H i : Theorem 8 ([15,35,18]). For a parity game G, from every location, there is exactly one player having a winning strategy. The problem of deciding the winner at a location is in UP ∩co-UP. In addition, if a player has a winning strategy then she also has a memoryless one from the same location.
We use W i (G) to denote the set consisting of all locations from which player i has a winning strategy.
For convenience, we sometimes directly write q ∈ D whenever D = (P, γ) and q ∈ P. We denote by D(A) the set consisting of all gadgets of A. Since we require that each PAPA A is well-structured, then D(A) must be a finite set.
We say that a gadget D = (P, γ) is incompatible if there exist q 1 , q 2 ∈ P and δ(q 1 ) = a, δ(q 2 ) = ¬a for some a ∈ A; or there is some q ∈ P with δ(q) = ⊥. Otherwise, we say that D is compatible.
Let D be a gadget and Γ = {D 1 , . . . , D k } be a set of gadgets, we denote by Γ D if there exist k positive numbers x 1 , . . . , x k such that: k i=1 x i ≤ 1, and for each q ∈ D with δ(q) = ∼p q ′ , we have q ′ ∈D i x i ∼ p. We in what follows call x 1 , . . . , x k the enabling condition. Note that the relation could be decided by solving a linear system of inequality.
According to automata theory, we may construct a deterministic (word) parity automaton A = ( Q, q, δ, Ω) were δ : Q × D(A) → Q and Ω is a total coloring function. It takes a gadget sequence as input, and accepts it if every gadget in it is compatible and every infinite path within it is even.
Then, we may create a parity game G A = (V A , E A , C A ) for the PAPA A, in detail: We say a vertex v of T is a modal vertex if δ(proj 1 (λ(v))) is of the form ∼p q ′ . We denote by ||v|| the modal depth of v, i.e., the number of modal vertices among the ancestors of v.
From each vertex v of T , we may obtain a set of vertices, denoted as cls(v), which involves v and all its descendants with the same modal depth. Since A is well-structured, then cls(v) must be a finite set. We also lift the notation by defining cls V = v∈V cls(v) for a finite vertex set V.
In addition, each finite vertex set V of T derives a gadget D( Let v 0 be the root vertex of T , then we have λ(v 0 ) = (q, s). We now let D = D 0 = D(cls(v 0 )), then for each play ∆ 0 , (D 0 , q 0 ), ∆ 1 , (D 1 , q 1 ), ∆ 2 , . . . with ∆ 0 = (D, δ( q, D)) and each D i = (P i , γ i ), player 0 can control it and make the play to fulfill the following property: (*) For each i, there exists a finite set of vertices V i having the same modal depth i, and there exists a state s i of M; and q ′ ∈ P i iff there is some v q ′ ∈ V i such that λ(v q ′ ) = (q ′ , s i ). In addition, (q 1 , q 2 ) ∈ γ i iff v q 2 is a child of v q 1 .
For i = 0, we have V 0 = cls(v 0 ) and s 0 = s. Assume that (*) holds at step i, then player 0 chooses the next location guided by the run as following: First, let V ′ i be all modal vertices among V i , and let V ′′ i be the set consisting of children of vertices in V ′ i . Then, V ′′ i can be partitioned into several sets V ′′ i,1 , . . . , V ′′ i,k according to the second component (assume proj 2 (λ(v ′ )) = s i, j for v ′ ∈ V ′′ i, j ) labeled on the vertices. Player 0 then chooses the set { (D i,1 , q i,1 ), . . . , (D i,k , q i,k )} as the next location, where D i, j = D(cls(V ′′ i, j )) and Then, according to the construction, for each (D i, j , δ( q i, j )) we have some state s i, j and the vertex set cls(V ′′ i, j ) making property (*) holds, no matter how player 1 chooses. Let x 1 = T(s i , s i,1 ), . . . , x k = T(s i , s i,k ), we definitely have k j=1 x j ≤ 1 and we also have q ′′ ∈D i, j x j ∼ p for each q ′ ∈ D i such that δ(q ′ ) = ∼p q ′′ because (T, λ) is an accepting run. Therefore, (D i,1 , . . . , D i,k ) D i holds.
We assert that each D i = (q 1 , . . . , q ℓ ) must be compatible -since (T, λ) is accepting, no such q ′ ∈ D i having δ(q ′ ) = ⊥, and if there exist q 1 , q 2 ∈ D i with δ(q 1 ) = a and δ(q 2 ) = ¬a, then we will both have a ∈ L(s i ) and a L(s i ). Also note that each infinite path within D 0 , D 1 , . . . corresponds to the first component of the labelings of an infinite branch of T , hence it must be even. According to A, we then conclude that this strategy is winning for player 0 form {(D 0 , δ( q))}.
⇐=) Let H 0 be the (memoryless) winning strategy of player 0 from {(D, δ( q))}, where D is some gadget involving q. We say that a location l = (D l , q l ) ∈ V 1 A is feasible if l may appear in some play under control of player 0 according to H 0 . We create a Markov chain M = (S , T, L) as follows. What left is to show that (M, s l 0 ) ∈ L (A), where l 0 is just (D, δ( q)). For each gadget D l such that l is feasible, we could obtain a forest (T l , λ l ), and in which each vertex q ′ is labeled with (q ′ , s l ). Then from T l 0 (which is an exact tree with (q, s l 0 ) labeled in the root), with a top-down manner, we connect the so far added tree T l with every T l ′ such that l ′ ∈ H 0 (l) -i.e., for each q ′ in T l with δ(q ′ ) = ∼p q ′′ , we add the vertex q ′′ in T l ′ as a child -it can be seen that it must be the case that some edges connecting some leaves of T l and the root(s) of T l ′ . We denote the labeled tree finally get as (T, λ), and it is indeed be an accepting run of A over (M, s l 0 ).
To make this paper not so dense, we have dropped off the proof of Thm. 9. Briefly, Player 0 could extract a winning strategy from an accepting run of A over any pointed Markov chain; and conversely, one can construct a Markov chain accepted by A according to the (memoryless) winning strategy of Player 0. Interested readers may find the detailed proof in the accompany report [21].
As a consequence of Thm. 7, Thm. 8 and Thm. 9 we have the following main conclusion of this section. Theorem 10. Both the Emptiness problem of PAPA and the Satisfiability problem of PµTL are decidable, and both of them are in 2EXPTIME.
Indeed, from Thm. 7 one can get a PAPA whose scale is linear in the size of the input formula, and an n-state PAPA could be converted to a parity game with scale 2 2 O(n) . From standard game theory (see [18,33], and see [28] for an improved bound), and with a similar analysis of [33] (see also the analysis of the coloring number in that paper), one can infer that this problem is in 2EXPTIME.

Discussion
In this paper, we present the logic PµTL, a simple and succinct probabilistic extension of µTL. We have compared the expressiveness of these two kinds of logics: In general, PµTL captures 'local' and 'stepwise' probabilities; whereas PCTL could describe 'global' probabilities in the system. Hence, these two logics are orthogonal and complementary, and one can obtain a more powerful and expressive logic by combing them together, as done in [7]. i.e., we may use formulae like (µZ.(a ∨ X ≥0.8 Z))U ≥0.6 (νZ ′ .(b ∧ F >0.3 Z ′ )). Model checking algorithm of such an extension can be acquired from those of the underlying logics.
In this paper, we have also investigated the decision problem of PµTL, the key issue and the most challenging part is to deal with probabilistic quantifiers when doing reduction to parity games, which is a highly nontrivial extension of the non-probabilistic case. As a cost, we have only now got an algorithm with double-exponential time complexity for solving it -in contrast, the Satisfiability problem for the standard µTL is in EXPTIME.