A Simple Probabilistic Extension of Modal Mu-calculus

1 Introduction

Temporal logics are heavily used in theoretical computer science and AI-related fields. Among those, modal �-calculus receives a lot of attraction ever since Kozen's seminal work [Kozen, 1983]. See for example, [Banieqbal and Barringer, 1987; Katoen, 1998; Walukiewicz, 2000; Berezin, 2002]. Moreover, various temporal logics including LTL [Pnueli, 1977], CTL [Emerson and Clarke, 1980], CTL* [Emerson and Halpern, 1986] are extensively studied. It is known that their expressiveness is strictly less [Dam, 1995] 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 PSPACEcomplete [Sistla and Clarke, 1985].

Probabilistic systems, such as Markov chains and Markov decision processes, are an important theme in AI domain. To reason about properties for probabilistic systems, the logic CTL was first extended with probabilistic quantifiers in [Hansson and Jonsson, 1994] , resulting in the logic PCTL. Intuitively, (aU �0:9 b) means that the probability of reaching

Lei Song

University of Technology, Sydney, Australia

Lijun Zhang

State Key Lab. of Computer Science, Institute of Software, CAS, Beijing, P. R. China

b-states along a-states is at least 0:9. At the same time, probabilistic LTL and its extension PCTL* have 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 [Couvreur et al., 2003]. 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 non-trivial in terms of the complexity of the corresponding model checking and satisfiability problems, or hindered from the restriction of fixpoint nesting.

We propose a natural and succinct extension of �TL in this paper, and name it P�TL. The logic is acquired by equipping the next operator with probability quantifiers, and keeping other parts as standard �TL. We have for instance the formula �Z:(a ^ X �0:8 Z). We investigate the model checking, expressiveness, and satisfiability problems of P�TL.

In detail, we first investigate the model checking problem of P�TL upon Markov chains. It turns out to be a straightforward adaptation of the classical algorithms for �TL, and the complexity remains in UP \ co-UP. We then give a comprehensive study on the expressiveness of P�TL by comparing with PCTL, and prove that P�TL is orthogonal with PCTL in expressiveness. However, for the qualitative fragments (i.e., probabilities may appear in a formula are only 0 and 1), we show that qualitative P�TL is strictly more expressive (w.r.t. finite Markov chains). 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, and it is shown that both of these two problems are in 2EXPTIME. This is in contrast to PCTL as well, whose Satisfiability checking is still an open problem (cf. [Br´azdil et al., ; Bertrand et al., 2012]).

An illustrating example We introduce a running example to motivate our work: Suppose there is a hacker trying 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; otherwise he tries with another one. However, 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 - assuming 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 s1, 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, as such system is considered to be safe if l is big enough. However, as we will show later, all PCTL formulae are not capable of expressing this property. 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 di�erent from s5.

Motivation from AI perspective The presented logic has the following potential application in AI domain:

• � First of all, Markov chains and Markov decision processes are the basic models in several areas of AI. As a logic with semantics defined w.r.t. such models, it 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 [Bhatia et al., 2011], because of its powerful expressiveness and the decidability of its Satisfiability problem. Thus, we expect that P�TL could be used in stochastic motion planning - since, P�TL is a decidability-preserving extension of �TL.
• � Fixpoints play an important role in mathematics and computer science. In AI area, it is used to designate non-terminating behaviors of intelligent systems, such as maintenance goals [Singh, 1998]. Fixpoints act as the elementary ingredients in P�TL, 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 [Morgan and McIver, 1997; Huth and Kwiatkowska, 1997; de Alfaro and Majumdar, 2001; McIver and Morgan, 2002; 2007; Mio, 2012b] interpret a formula as a function from states to real values in [0; 1], whose semantics is di�erent from P�TL. A further extension of �-calculus was proposed in [Mio, 2012a], which is able to encode the full PCTL. However, the model checking and Satisfiability algorithms are still unknown for these calculi and are "far from trivial" [Mio, 2012b]. The other probabilistic �-calculus was introduced in [Cleaveland et al., 2005] along with a model checking algorithm for it. Moreover, it is able to encode PCTL formulae as well. However, that calculus only allows alternation-free formulae (cf. [Emerson and Lei, 1986]).

Very recently - and independently -, Castro, Kilmurray, and Piterman present another extension by adding fixpoints to full PCTL [Castro et al., 2015]. The calculus they introduced is more expressive than logics PCTL and PCTL*. Moreover, it is also easy to see that it is a proper super logic of our logic P�TL as well. They show the model checking problem is in NP \co-NP. We note that some examples in our paper are similarly investigated in [Castro et al., 2015]. Since the logic in [Castro et al., 2015] subsumes PCTL, its Satisfiability problem is also left open. However in this paper we show Satisfiability of P�TL could be reduced to solving parity games, which makes this problem solvable in 2EXPTIME.

2 Preliminaries

In this paper, we fix a countable set A of atomic propositions, ranging over a; b; a1 etc, and fix a countable set Z of formula variables, ranging over Z; Z1 etc.

A Markov chain is a tuple M = (S ; T; L), where S is a finite set of states; T : S � S ! [0; 1] is the matrix of transitionprobabilities, fulfilling P s 0 2S T(s; s 0 ) = 1 for every s 2 S ; and L : S ! 2 A is the labeling function. A pointed Markov chain is a pair (M; s) where M is a Markov chain (S ; T; L) and s 2 S is the initial state.

An (infinite) path � of M is an infinite sequence of states s0; s1; : : :, such that si 2 S and T(si; si+1) > 0 for each i. A basic cylinder cyl(s0; s1; : : : ; sn) of M is the set of infinite paths having s0; s1; : : : ; sn as the prefix.

According to the standard theory of Markov process, the pointed Markov chain (M; s) uniquely derives a measure space (�M;s; �M;s; prob M;s ) where �M;s consists of all infinite paths of M; �M;s is the minimal Borel field containing all basic cylinder of M (i.e., �(M;s) is closed under complementation and countable intersection); and the measuring function prob M;s fulfills: prob M;s (cyl(s0; s1; : : : ; sn)) equals 0 if s , s0, and equals Q i<n T(si; si+1) otherwise. We say a set P � �M;s is measurable if P 2 �M;s. [Vardi, 1985] 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 �2 f>; �g and p 2 [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.

• � ~>�M = S ; ~?�M = ;.
• � ~a�M = fs 2 S j a 2 L(s)g; ~:a�M = fs 2 S j a < L(s)g.
• � ~X �p f �M = fs 2 S j P s 0 2~ f �M T(s; s 0 ) � pg.
• � ~ f1 ^ f2�M = ~ f1�M \ ~ f2�M; ~ f1 _ f2�M = ~ f1�M [ ~ f2�M.
• � ~ f1U �p f2�M = fs 2 S j prob M;s f� 2 cyl(s) j � j= f1Uf2g � pg and ~ f1R �p f2�M = fs 2 S j prob M;s f� 2 cyl(s) j � j= f1Rf2g � pg.

In addition, for an infinite path � = s0; s1; : : : of M, the notation � j= f1Uf2 stands for that there is some i � 0 such that si 2 ~ f2�M and s j 2 ~ f1�M for each j < i. Meanwhile, � j= f1Rf2 holds if either � j= f2U( f1 ^ f2) or s j 2 ~ f2�M for each j. To simplify notations, in what follows we denote by M; s j= f whenever s 2 ~ f �M holds.

3 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:

• � ~>�M(e) = S and ~?�M(e) = ;.
• � ~a�M(e) = fs 2 S j a 2 L(s)g and ~:a�M(e) = fs 2 S j a < L(s)g.
• � ~Z�M(e) = e(Z).
• � ~X �p f �M(e) = fs 2 S j P s 0 2~ f �M(e) T(s; s 0 ) � pg.
• � ~ f1 ^ f2�M(e) = ~ f1�M(e) \ ~ f2�M(e) and ~ f1 _ f2�M(e) = ~ f1�M(e) [ ~ f2�M(e).
• � ~ �Z: f �M(e) = T fS 0 � S j ~ f �M(e[Z 7 ! S 0 ]) � S 0 g and ~ �Z: f �M(e) = S fS 0 � S j ~ f �M(e[Z 7 ! S 0 ]) � S 0 g.

Indeed, ~ �Z: f �M(e) (resp. ~ �Z: f �M(e)) could be computed as in the classical setting via the following iteration:

1. let S 0 = ; (resp. S 0 = S );
2. subsequently, let S i+1 = ~ f �M(e[Z 7 ! S i]);
3. stops if S ' +1 = S ', and returns S '.

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 X = ~ f �M(e[Z 7 ! X]) within 2 S .

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 [Jurdzi ´nski, 1998; Wilke, 2002] and the only noteworthy di�erence lies from handling X �p - subformulae, 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 M; s j= f if s 2 ~ f �M.

Below we give some example properties:

1. The formula �Z:(a^X >0:8 Z) describes that there exists an a-region, where each state has less than 0:2 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.
3. M; s j= �Z:(a _ X �0:6 Z) 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 �Z1:(a _ �Z2:(a _ X >0 Z2) ^ X �1 Z1) 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 Df (Z) to denote the subformula which binds Z in f . For example, let f = �Z1(a ^ �Z2:(b ^ X > =0:3 Z2)_X >0:6 Z1), then we have Df (Z1) = f and Df (Z2) = �Z2:(b ^ X �0:3 Z2).

We say that a P�TL formula f is guarded, if the occurrence of each bound variable Z in Df (Z) is in the scope of some Xoperator. The following theorem could be proven in a same manner as that in [Walukiewicz, 2000].

Theorem 2. For each P�TL formula f , there is a guarded formula f 0 such that ~ f 0 �M(e) = ~ f �M(e) for every M and e.

Thus, in what follows, we always assume that each P�TL formula is guarded.

4 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 everyMarkov 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.

Theorem 3. Let f = �Z:(a ^ X �0:5 Z), then g . f for every PCTL formula g.

Proof. To show this, we need first construct two families of Markov chains, namely, M0; M1; : : : ; and M 0 0 ; M 0 1 ; M 0 2 ; : : :.

For the first group, let Mn = (fs0; s1; : : : ; sng; Tn; Ln), where: Tn(s0; s0) = 1 and Tn(si+1; si) = 1 for each i < n (hence Tn(si; s j) = 0 for any other si, s j). In addition, Ln(s0) = ; and Ln(si) = fag for each 0 < i � n.

For the second ones, let M 0 n = (fs 0 0 ; s 0 1 ; : : : ; s 0 n g; T 0 n ; L 0 n ) where: T 0 n (s 0 n ; s 0 n ) = T 0 n (s 0 n ; s 0 n�1 ) = 0:5, T 0 n (s0; s0) = 1, and T 0 n (s 0 i+1 ; s 0 i ) = 1 for every i < n � 1. In addition, L 0 n (s 0 0 ) = ; and L 0 n (s 0 i ) = fag for each 0 < i � n.

Given a PCTL formula g, let N(g) be the maximal nesting depth of temporal-operators of g. According to [Baier and Katoen, 2008, Thm. 10.45], we have that M 0 n ; s 0 n j= g if and only if Mn; sn j= g whenever n � N(g).

Observe the fact that M 0 n ; s 0 n j= f and Mn; sn 6 j= 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.

�

Conversely, the following theorem reveals that there also exists some PCTL formula that could not be equivalently expressed by any P�TL formula.

Theorem 4. Let f = F �0:5 a, then g . f for every (closed) P�TL formula g.

Proof. Let M = (fs1; s2; s3g; T; L) be the (family of) Markov chain(s) where: L(s1) = L(s2) = ;, L(s3) = fag, T(s1; s1) = x; T(s1; s2) = y; T(s1; s3) = z, and T(s2; s2) = T(s3; s3) = 1, with x; y; z 2 (0; 1) and x + y + z = 1.

For every PCTL and/or closed P�TL formula g, we let Px(g) be the proposition that "for the fixed x, there are infinitely many y making M; s1 j= g and there are infinitely many y making M; s1 6 j= g". We now show that if g is a closed P�TL formula, then there exists some xg < 1 such that Px(g) does not hold whenever x 2 (xg; 1).

• � Such xg can be arbitrarily chosen if g = ?, g = >, g = a or g = :a.
• � In the case that g = g1 ^ g2, assume by contradiction that such xg does not exist, then it implies that for every x 2 (0; 1), there exists some x 0 > x such that Px 0 (g) holds. Observe that M; s1 j= g implies both M; s1 j= g1 and M; s1 j= g2; and M; s1 6 j= g implies either M; s1 6 j= g1 or M; s1 6 j= g2. Thus, we can infer that either xg1 or xg2 does not exist, which violates the induction hypothesis.
• � Proof for the case of g = g1 _ g2 is similar to the above.
• � If g = X �p g 0 and p 2 (0; 1), whenever x 2 (maxfp; 1 � pg; 1), since �2 f>; �g, then M; s1 j= g i� M; s1 j= g 0 because y + z < p in such situation. In this case, we may just let xg = maxfxg 0 ; p; 1 � pg.
• � If g = X �1 g 0 , then we need to distinguish two cases: 1) There exist x; y 2 (0; 1) such that M; s1 j= g holds, then we can immediately infer that both M; s2 j= g 0 and M; s3 j= g 0 . In addition, observe that truth values of g 0 on s2 and s3 are irrelevant to x and y. It implies that in such case M; s1 j= g i� M; s1 j= g 0 , and hence, we may just let xg = xg 0 . 2) There is no such x and y having M; s1 j= g holds, in such situation, xg can be any number in (0; 1).
• � If g = X >0 g 0 , then the proof is similar to the above.
• � When g = X �0 g 0 (or g = X >1 g 0 ), things would be trivial, because g could be reduced to > (resp. ?) in such case.
• � If g = �Z:g 0 , we let g0 = ? and gi+1 = g 0 [Z=gi]. Since that M is a 3-state Markov chain, then g and W i�3 gi 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 0 , the preprocessing is almost similar, but we just replace g with V i�3 gi where g0 = >.

Now, for the PCTL formula f = F �0:5 a, such xf does not exist, because, for every x 2 (0; 1) we have: M; s1 j= f provided that y 2 [(1 � x)=2; 1); and M; s1 6 j= f if y 2 (0; (1 � x)=2). This implies that Px( f ) holds for every x 2 (0; 1), and hence f cannot be equally expressed by any P�TL formula. �

Note that the value 0:5 in the previous two theorems can be generalized to any other probability p 2 (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 formulaeg. Inductively:

1. eg = ? if g = ?, or its root operator is X >1 , U >1 or R >1 ; eg = > if g = >, or its root operator is X �0 , U �0 or R �0 .
2. eg = e g1 ^ e g2 if g = g1 ^g2; andeg = e g1 _ e g2 if g = g1 _g2.
3. eg = X >0e g 0 if g = X >0 g 0 ; andeg = X �1e g 0 if g = X �1 g 0 .
4. eg = �Z:( e g2 _ (e g1 ^ X >0 Z)) if g = g1U >0 g2; and eg = �Z:( e g2 ^ (e g1 _ X �1 Z)) if g = g1R �1 g2.
5. eg = �Z:( e g2 _ (e g1 ^ ] F >0 g2 ^ X �1 Z)) = �Z:( e g2 _ (e g1 ^ �Z 0 :( e g2 _ X >0 Z 0 ) ^ X �1 Z)) if g = g1U �1 g2; and eg = �Z:( e g2 ^ (e g1 _ ] G �1 g2 _ X >0 Z)) = �Z:( e g2 ^ (e g1 _ �Z 0 :( e g2 ^ X �1 Z 0 ) _ X >0 Z)) if g = g1R >0 g2.

The proof of equivalence could be done by induction on the structure of the formula. �

Note that Thm. 5 holds because we are only concerned about finite models in this paper. Interested readers may show that it is not true for infinite Markov chains.

Theorem 6. The qualitative P�TL formula f = �Z:(a ^ X >0 X >0 Z) cannot be expressed in qualitative PCTL.

Proof. Construct a series of Markov chains M 00 2 ; M 00 3 ; : : : such that each M 00 n is the Markov chain (fs 00 0 ; s 00 1 ; : : : ; s 00 n g; T 00 n ; L 00 n ), where T 00 n (s 00 0 ; s 00 0 ) = 1 and T 00 n (s 00 i+1 ; s 00 i ) = 1 for each i < n. In addition, L 00 n (s 00 i ) = fag for each i , 1, and L 00 n (s 00 1 ) = ;.

For a given PCTL formula g, let ˆg be the LTL formula obtained from g by discarding all probability quantifiers, e.g., we have ˆg = aU(b _ G:a) if g = aU �0:3 (b _ G >0:6 :a). Since that from s 00 n the Markov chain M 00 n has exactly one infinite path �n = s 00 n ; : : : ; s 00 1 ; (s 00 0 ) ! , then for each n � 2 we have M 00 n ; s 00 n j= g if and only if �n j= ˆg. It is shown in [Wolper, 1983] that M 00 n ; s 00 n j= ˆg i� M 00 n+1 ; s 00 n+1 j= ˆg in the case of n � N 0 (ˆg) = N 0 (g), where N 0 (g) and N 0 (ˆg) are the nesting depth of X-operator of g and ˆg, respectively. Thus, we have M 00 n ; s 00 n j= g i� M 00 n+1 ; s 00 n+1 j= 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 00 n ; s 00 n j= f and M 00 n+1 ; s 00 n+1 j= f for each n � 2. �

Note that the conclusion of Thm. 6 is also pointed out in [Cleaveland et al., 2005], and we here provide a detailed proof. Indeed, this proof 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.

5 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 [Wilke, 2002].

A PAPA A is a tuple (Q; q0; �; �) where: Q is a finite set of states, q0 2 Q is the initial state, � is the transition function to be defined later, and � : 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 2 A, the literals a and :a are transition conditions over Q.
3. If q 2 Q, then q is a transition condition over Q.
4. If q 2 Q and p 2 [0; 1], then # �p q is a transition condition over Q, where �2 f�; >g.
5. If q1; q2 2 Q then both q1 _ q2 and q1 ^ q2 are transition conditions over Q.

The transition function � assigns each state q 2 Q a transition condition over Q.

We denote by RA the derived graph of A, its vertex set is just Q, and there is an edge from q1 to q2 i� q2 appears in �(q1). We say that A is well-structured, if for every path q1; q2; : : : ; qn that forms a cycle (i.e., q1 = qn) in RA, we have that: 1) there exists some 1 � i < n such that �(qi) = # �p qi+1 with some p 2 [0; 1]; 2) there exists some 1 � j < n such that qj is colored. In what follows, we are only concerned about well-structured PAPA.

Given a pointed Markov chain (M; s0) with M = (S; T; L) and s0 2 S , a run of A over (M; s0) is a Q � S -labeled tree (T; �) fulfilling: �(v0) = (q0; s0) for the root vertex v0; and for each internal vertex v of T with �(v) = (q; s) we require that

• � �(q) , ?, and if �(q) = > then v has no child;
• � a 2 L(s) if �(q) = a, and a < L(s) if �(q) = :a;
• � if �(q) = q1 ^ q2 then v has two children v1 and v2 respectively having �(v1) = (q1; s) and �(v2) = (q2; s);
• � if �(q) = q1 _ q2 then v has one child v 0 with �(v 0 ) 2 f(q1; s); (q2; s)g;
• � v has one child v 0 having �(v 0 ) = (q 0 ; s), if �(q) = q 0 ;
• � if �(q) = # �p q 0 then v has a set of children v1; : : : ; vn such that �(vi) = (q 0 ; si), where P n i=1 T(s; si) � p.

For an infinite branch � = v0; v1; : : : of T, let n� be the number

maxf n j there are infinitely many i s.t. �(proj 1 (�(vi))) = ng

where proj 1 (q; s) = q. A run (T; �) is accepting if n� is an even number, for every infinite branch � of T. A pointed Markov chain (M; s0) is accepted by A if A has an accepting run over it. We denote by L (A) the set consisting of pointed Markov chains accepted by A.

Theorem 7. Given a closed P�TL formula f , there is a PAPA Af such that: M; s j= f i� (M; s) 2 L(Af ), for each pointed Markov chain (M; s).

Proof. We just let Af = (Qf ; qf ; �f ; �f ), where:

• � Qf = fqg j g is a subformula of f g, and hence qf 2 Qf ;
• � �f is defined as follows:
• �f (q?) = ? and �f (q>) = >;
• �f (qa) = a and �f (q:a) = :a;
• � f (qg1^g2 ) = qg1 ^ qg2 and � f (qg1_g2 ) = qg1 _ qg2 ;
• �f (qX �p g) = # �p qg;
• �f (q�Z:g) = qg and �f (q�Z:g) = qg;
• �f (qZ) = qDf (Z).
• � �f is defined at every state qZ with Z 2 Z fulfilling: If Z is a �-variable (resp. �-variable), then �f (qZ) is the minimal odd (resp. even) number which is greater than every �f (qZ 0 ) such that Df (Z 0 ) is a subformula of Df (Z).

It could be directly examined that Af is well-structured since f is guarded. The proof of equivalence can be similarly done as that in [Wilke, 2002] - the only di�erent 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 [ fq 0 g; q 0 ; �[q 0 7 ! # �p q]; �) must correspond to X �p g. �

6 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 v0 2 V is an infinite sequence of locations v0; v1; : : : made by player 0 and player 1 - for every i 2 N, the location vi+1 is chosen by player 0 (resp. player 1) with (vi; vi+1) 2 E whenever vi 2 V 0 (resp. vi 2 V 1 ).

Player 0 (resp. player 1) wins the play v0; v1; : : : 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 vi with C(vi) = c.

A winning strategy for player i is a mapping Hi : V � � V i ! V, such that for every play v0; v1; : : :, player i always wins if vj+1 = Hi(v0; : : : ; vj) whenever vj 2 V i . In addition, Hi is memoryless if Hi(v0; : : : ; vj) agrees with Hi(vj) for every j.

Theorem 8 ([Gurevich and Harrington, 1982; Zielonka, 1998; Jurdzi ´nski, 1998]). 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 Wi(G) to denote the set consisting of all locations from which player i has a winning strategy.

Given a PAPA A = (Q; q; �; �), a gadget D of A is a finite directed acyclic digram (P; �) where P � Q, � � P � P, and for each q 2 P:

1. if �(q) = q 0 , then q 0 2 P and (q; q 0 ) 2 �;
2. if �(q) = q1 ^ q2 then q1; q2 2 P, and (q; q1); (q; q2) 2 �;
3. if �(q) = q1 _ q2 then there is some i 2 f1; 2g such that qi 2 P and (q; qi) 2 �,
4. q has no successor for the other cases.

For convenience, we sometimes directly write q 2 D whenever D = (P; �) and q 2 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.

Given a sequence of gadgets D1; D2; : : : such that Di = (Pi; �i), an infinite path within it is a sequence of states q1;1; : : : ; q1;'1 ; q2;1; : : : ; q2;'2 ; : : : such that each (qi; j; qi; j+1) 2 �i and �(qi;'i ) = # �pi qi+1;1 for some pi 2 [0; 1]. We say such an infinite path is even (resp. odd) if the maximal color (w.r.t. �) occurring infinitely often is even (resp. odd).

We say that a gadget D = (P; �) is incompatible if there exist q1; q2 2 P and �(q1) = a, �(q2) = :a for some a 2 A; or there is some q 2 P with �(q) = ?. Otherwise, we say that D is compatible.

Let D be a gadget and � = fD1; : : : ; Dkg be a set of gadgets, we denote by � � D if there exist k positive numbers x1; : : : ; xk such that: P k i=1 xi � 1, and for each q 2 D with �(q) = # �p q 0 , we have P q 0 2Di xi � p. We in what follows call x1; : : : ; xk 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 e A = (e Q;eq;e�; e�) were e� : e Q � D(A) ! e Q and e� 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 GA = (VA; EA;CA) for the PAPA A, in detail:

• � VA = V 0 A [V 1 A , where V 0 A = 2 D(A)�e Q and V 1 A = D(A) � e Q.
• � EA = f(f(D1; e q1); : : : ; (Dk; e qk)g; (Di; e qi)) j 1 � i � kg [ f((D;eq); f(D1; e q1); : : : ; (Dk; e qk)g) j (D1; : : : ; Dk) � D; and each e qi =e�(eq; Di)g.
• � CA(D;eq) = e�(eq), hence every location in V 1 A is colored.

Theorem 9. Let the PAPA A = (Q; q; �; �), then L(A) , ; if and only if there is some D 2 D(A) with q 2 D such that f(D;e�(eq; D))g 2 W0(GA).

Intuitively, player 0 could extract a winning strategy from an accepting run of A over any pointed Markov chain; and conversely, one can construct a pointed Markov chain accepted by A according to the (memoryless) winning strategy of player 0. Interested readers may find the detailed proof in the accompanied report [Liu et al., 2015].

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 [Jurdzi´nski, 1998; Wilke, 2002], and see [Schewe, 2008] for an improved bound), and with a similar analysis of [Wilke, 2002] (see also the analysis of the coloring number in that paper), one can infer that this problem is in 2EXPTIME.

7 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 [Castro et al., 2015]. i.e., we may use formulae like (�Z:(a _ X �0:8 Z))U �0:6 (�Z 0 :(b ^ F >0:3 Z 0 )). 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.

Acknowledgement

First and foremost, the authors would thank all the anonymous reviewers for the valuable and helpful comments on this paper. We would also thank Nir Piterman for his valuable comments on our work.

Wanwei Liu is supported by National Natural Science Foundation of China (Grant Nos. 61103012, 61379054 and 61272335). Lei Song is supported by Australian Research Council under Grant DP130102764. Ji Wang is supported by National Natural Science Foundation of China (Grant No. 61120106006). Lijun Zhang (corresponding author) is supported by National Natural Science Foundation of China (Grant Nos. 61428208, 61472473 and 61361136002), the CAS/SAFEA International Partnership Program for Creative Research Teams.