A Logic of Probability with Decidable Model Checking

A logic of probability with decidable model-checking Beauquier, D. and Rabinovich, A. and Slissenko, A. Technical Report TR-2003-07 Laboratory of Algorithms, Complexity and Logic University of Paris XII, Val-de-Marne 61, avenue du Général de Gaulle F-94010 CRÉTEIL Cedex – France Tel: +33 (0)1 45 17 16 47 Fax: +33 (0)1 45 17 66 01 A logic of probability with decidable model-checking Danièle Beauquier1] Alexander Rabinovich2] University Paris 12, France beauquier@univ-paris12.fr Tel-Aviv University, Israel rabino@math.tau.ac.il Anatol Slissenko1 ] University Paris-12, France slissenko@univ-paris12.fr Abstract A predicate logic of probability, close to logics of probability of Halpern and al., is introduced. Our main result concerns the following model-checking problem: deciding whether a given formula holds on the structure defined by a given Finite Probabilistic Process. We show that this model-checking problem is decidable for a rather large subclass of formulas of a second-order monadic logic of probability. We discuss also the decidability of satisfiability and compare our logic of probability with the probabilistic temporal logic pCT L∗ . Keywords Predicate logics of probability, Model checking, Finite Probabilistic Process 1 Introduction Logics with probabilities were considered in different contexts; on the one hand in artificial intelligence for reasoning about uncertainty in expert systems, and on the other hand for specification and verification of systems which exhibit some uncertainty such as fault-tolerant or randomized systems. One can distinguish two families of logical approaches for reasoning about probabilities: (1) the first one extends the predicate logics (2) the second one extends temporal logics. A fundamental contribution to the study of predicate logics of probability was done in [FHM90, Hal90], mainly motivated by the problems of artificial intelligence. The paper [Hal90] contains a good survey and analysis of previous works on predicate logics of probability. There has been very interesting works on extensions of predicate logic by probability quantifiers in model-theory community (see survey [Kei85]). The models considered there are different from thus considered in this paper and these works seems to be unrelated to our. Most of the work related to the verification uses probabilistic extensions of temporal logics. The first applications of temporal logic to probabilistic systems were considered in studying which temporal properties are satisfied with probability 1 by systems modeled as finite Markov chains [LS82]. Later, papers [HJ94, ASB+ 95] introduced logics pCT L and pCT L∗ that can express quantitative bounds on the probability of system evolutions. This approach is surveyed, for example in [Han94] and [CY95]. In this paper we are interested in the verification of probabilistic systems. However, unlike previous works on verification we take as a specification formalism a probabilistic extension of predicate logic. Predicate logics offer some advantages (over modal and temporal logics) due to their expressiveness and convenience for formalization of complicated properties. We follow the general setting of [FHM90, Hal90, AH94] to introduce a rather expressive predicate logic of probability. ] 1 Address: LACL, Dept. of Informatics, University Paris-12, 61 Av. du Gén. de Gaulle, 94010, Créteil, France. Partially supported by French-Israeli Arc-en-ciel/Keshet project No 30. 2 Address: Department of Computer Science, Tel-Aviv University, Israel. 1 Our main result is a description of a fragment of a second-order monadic logic of probability with the following decidable model-checking problem. Model-checking problem: decide whether a given formula holds on the structure defined by a given finite Markov chain. The paper is organized as follows. In Section 2 we give a general description of the logic we use and emphasize how it deviates from [Hal90, FHM90]. In Section 3 we show that monadic predicate logic of probability is undecidable. Section 4 contains the statement of our main results about a fragment of probabilistic monadic logic of order with decidable model-checking. Section 5 is devoted to the proof of these results. In Section 6 we extend decidable model-checking to formulas with nested probabilistic operators. In the last section we give some open problems. Section 7 compares our logic with probabilistic temporal logic pCT L ∗ . We prove that the property “there is a moment at which Q holds with probability one” cannot be expressed in pCT L ∗ , but is directly formalized in our logic of probability. In the last section we state some open problems. 2 Logic of probability We follow Halpern’s presentation of logic of probability [Hal90]. There, arithmetic operations on probabilities are allowed, probabilities may be variables which are quantified. In our setting, we just compare probabilities with rational constants. However, we consider second order logics, when [Hal90] confines himself to first order ones. We consider a language that consists of a collection Σ of predicate symbols of various arities. We also have a collection of predicate variables of various arities. Given formulas ϕ and ψ in the logic, we allow formulas of the form Prob>q (ϕ) and Prob>q (ϕ|ψ), where q is a rational number which can be read as “the probability of ϕ is greater than q” and “the probability of ϕ under the condition ψ is greater than q” respectively. 2.1 Syntax More formally we define the syntax as follows. The vocabulary consists of a set of deterministic predicate symbols, a set of probabilistic predicate symbols, predicate variables and individual variables. We also assume that rational constants are in the vocabulary. Formulas: – Atomic formulas are of the form R(x1 , . . . , xk ), where R is a (deterministic or probabilistic) predicate symbol of arity k and x1 , . . . , xk are individual variables; or of the form Q(x1 , . . . , xk ), where Q is a deterministic predicate variable of arity k and x1 , . . . , xk are individual variables. – If ϕ1 and ϕ2 are formulas then (ϕ1 ∨ ϕ2 ) and ¬ϕ1 are formulas. – If ϕ is a formula then ∃ x ϕ and ∃ Q ϕ , where x is an individual variable and Q is a deterministic predicate variable, are formulas. – If ϕ, ψ are formulas, and q is a rational number then Prob>q (ϕ) and Prob>q (ϕ | ψ) are formulas. Conjunction (ϕ1 ∧ ϕ2 ), implication (ϕ1 → ϕ2 ), universal quantification ∀α ϕ are defined as usual, using disjunction, negation and existential quantifier. Expressions like Prob <q , Prob≤q , Prob≥q , Prob=q can be also defined in terms of Prob>p using negation and modified bounds on probability in a syntactical manner. For example, we define Prob<p (ϕ) as Prob>(1−p) (¬ϕ). 2.2 Semantics First we recall some basic notions from probability theory. 2 A measurable space is a pair (Ω, ∆) consisting of a non empty set Ω and a σ-algebra ∆ of its subsets that are called measurable sets and represent random events in probability context. A σ-algebra over Ω contains Ω and is closed under complementation and countable union. Adding to a measurable space a probability measure µ : ∆ → [0, 1] such that µ(Ω) = 1 and that is countably additive, we get a probability space (Ω, ∆, µ). Probabilistic predicates are interpreted as random predicates. Given a domain U and a probabilistic space (Ω, ∆, µ) a random (or stochastic) predicate P of arity k is a function from Ω × U k to Bool = {true, false} such that for any fixed u1 , . . . , uk ∈ U the set {ω ∈ Ω : P (ω, u1 , . . . , uk )} is measurable. A probabilistic structure for the language described above is a tuple (hU, δi, hΩ, ∆, µi, π), where – hU, δi is a first-order structure with universe U, and δ assigns a relation over U of the appropriate arity to each deterministic predicate symbol; – hΩ, ∆, µi is a probabilistic space; – π assigns to each probabilistic predicate symbol P of arity k a random predicate π(P ) : Ω × U k → Bool. Define a valuation ν to be a function which assigns to each individual variable an element of U, and to each deterministic predicate variable a finite relation over U of the appropriate arity (‘finite’ means that the set of tuples for which the deterministic predicate is true is finite). Given a probabilistic structure M = (hU, δi, hΩ, ∆, µi, π), an element ω ∈ Ω and a valuation ν, formally we define when a formula ϕ holds at ω in M under a valuation ν, written M, ν, ω |= ϕ , by the following inductive clauses: (S1) M, ν, ω |= R(x1 , . . . , xk ) for a deterministic predicate symbol R of arity k and individual variables x1 , . . . , xk iff δ(R)(ν(x1 ), . . . , ν(xk )) is true. (S2) M, ν, ω |= Q(x1 , . . . , xk ) for a deterministic predicate variable Q of arity k iff ν(Q)(ν(x1 ), . . . , ν(xk )) is true. (S3) M, ν, ω |= P (x1 , . . . , xk ) for a probabilistic predicate P of arity k iff π(P )(ω, ν(x1 ), . . . , ν(xk )) is true. (S4) Quantifiers over individual variables and Boolean connectors are treated as usually. (S5) Quantifiers over deterministic predicate variables are interpreted as quantifiers over deterministic predicate variables that range only over finite relations over U. (S6) M, ν, ω |= Prob>q (ϕ) iff µ({ω 0 ∈ Ω : M, ν, ω 0 |= ϕ}) > q, that is iff the set of all ω 0 for which M, ν, ω 0 |= ϕ holds has a measure greater than q. (S7) M, ν, ω |= Prob>q (ϕ | ψ) iff µ{ω 0 ∈ Ω : M, ν, ω 0 |= (ϕ ∧ ψ)} > q · µ{ω 0 ∈ Ω : M, ν, ω 0 |= ψ}, i. e. the conditional probability of ϕ under ψ is > q. Remark that (S6) is a particular case of (S7) when ψ = true. The semantics is well defined only if the sets that appear in (S6) and (S7) are measurable. From now on we assume that (Countability Assumption) The domain U of probabilistic structures is countable. Proposition 1 Under Countability Assumption the sets that appear in (S6) and (S7) are measurable, and the semantics is well defined. Proof. By induction on the structure of formulas. The only not quite straightforward step is quantification. For formula ∃ x ϕ we use that any σ-algebra is closed under countable union. For formula ∃ Q ϕ we use the fact that the set of finite predicates over a countable domain is countable and thus we can again use that any σ-algebra is closed under countable union. ¥ 3 Proposition 2 Suppose that two valuations ν1 and ν2 agree on the free variables of a formula ϕ. Then M, ν1 , ω |= ϕ iff M, ν2 , ω |= ϕ. Proposition 3 If all the occurrences of probabilistic predicates in a formula ϕ are in the scope of some operator Prob then M, ν, ω1 |= ϕ iff M, ν, ω2 |= ϕ for every ω1 , ω2 ∈ Ω. In particular, for any formula ψ we have M, ν, ω1 |= Prob>q (ψ) iff M, ν, ω2 |= Prob>q (ψ). 3 Undecidability of monadic logic of probability The decidability of the probabilistic propositional logic follows from [FH94] where the decidability of a more general logic was proved. For first-order logic it is well-known that the satisfiability problem is decidable if the language has only unary predicates (Monadic Logic) and the satisfiability problem is undecidable even with one binary predicate [Hod93]. Many undecidability results for probabilistic logics can be found in [AH94] where this question was investigated in detail. It was shown in [AH94] that the satisfiability problem of their probabilistic logic even with one unary predicate is Σ21 complete. However the logics considered there admit addition of probabilities or even multiplication of probabilities and quantifiers over reals and the methods of [AH94] are not applicable for our (much weaker) probabilistic logic. In this section we prove (Theorem 1) that the satisfiability/validity problem for first-order monadic logic of probability (that is a logic of probability where all predicates are monadic) is undecidable. We reduce the satisfiability problem for first-order predicate logic with one binary predicate to the satisfiability problem for monadic logic of probability. First, we define a translation from the first-order formulas over a binary predicate to formulas of probabilistic logic with two unary predicates. Let R be a binary predicate symbol and φ be a formula in the signature {R}. Replace in φ every occurrence of R(x, y) by Prob>0 (P (x) ∧ Q(y)), where P and Q are unary predicate symbols. The resulting formula ψ(P, Q) is called the translation of φ. Proposition 4 The formula φ(R) is satisfiable iff its translation ψ(P, Q) is satisfiable. Proof. It is clear that if the translation of φ is satisfiable in a probabilistic structure M then φ is satisfiable in the structure h|M |, R∗ i, where |M | is the universe of M and R∗ (a, b) holds iff M, a, b |= Prob>0 (P (x)∧Q(y)). Let M be a structure for a binary predicate name R where the interpretation of R is a relation R ∗ over a countable universe U = {a1 , a2 , . . . , an , . . .}. Let us define a probabilistic structure M as follows. Take as a probabilistic space Ω = U with a discrete distribution of probabilities µ({a n }) = 1/2n for every n if Ω is infinite, and µ is uniform if Ω is finite. For each an ∈ Ω, set π(P )(an , t) = true iff t = an and set π(Q)(an , t) = true iff R∗ (an , t). Observe that for every a, b ∈ U, R∗ (a, b) iff M, a, b |= Prob>0 (P (x) ∧ Q(y)). Hence for every sentence φ in the signature {R} and its translation ψ we have M |= φ iff M |= ψ In particular, if φ is satisfiable then its translation is satisfiable. ¥ From Proposition 4 we can deduce: Theorem 1 The satisfiability problem for monadic logic of probability is undecidable. We do not know the exact complexity for the satisfiability problem of monadic logic of probability, however we believe that it is much lower than Σ21 . We also have the following property: Proposition 5 There exists a satisfiable formula of monadic logic of probability with equality such that all its models have an infinite probabilistic space. 4 Proof. There is a closed predicate formula φ(R) over a binary predicate R which is satisfiable only in structures where the universe is infinite. For example take for φ(R) the conjunction of the three properties, R is transitive, irreflexive and ∀x ∃y R(x, y). Consider the formula ψ(P, Q) obtained as above, replacing in φ(R) every occurrence of R(x, y) by Prob>0 (P (x) ∧ Q(y)). Consider the probabilistic monadic formula Ψ(P, Q) = ψ(P, Q) ∧ Prob=1 (∃!x P (x)) ∧ ∀x Prob>0 (P (x)) We claim that : (1) Ψ(P, Q) is satisfiable, (2) Every model of Ψ(P, Q) has an infinite probabilistic space. In order to prove (1), consider the following model M . Take a countable infinite universe U = {a 1 , a2 , . . . , an , . . .}. Take as a probabilistic space Ω = U with a discrete distribution of probabilities µ({a n }) = 1/2n for every n. For each an ∈ Ω set π(P )(an , t) = true iff t = {an } and π(Q)(an , t) = true iff t ∈ {an+1 , an+2 , . . .}. Then it is clear from the construction that M satisfies Ψ(P, Q). Here is the proof of (2). Suppose there is a structure M that is a model of Ψ(P, Q) with a finite probabilistic space Ω = {ω1 , . . . , ωk }. We can suppose that µ(ωi ) > 0 for i = 1, . . . , k. Thus for i = 1, . . . , k there exists a unique ai ∈ U such that π(P )(ωi , ai ) because M satisfies Prob=1 (∃!x P (x)). Choose an element a in universe U different from all the ai . Since M satisfies ∀ x Prob>0 (P (x)), there exists an ω ∈ Ω such that π(P )(ω, a) = true. A contradiction. ¥ 4 Model-checking for fragments of logic of probabilities In this section we consider a logic of probability with one binary deterministic predicate, the order <, all other predicates are probabilistic monadic and all its second-order variables are monadic. This logic is denoted PMLO(Probabilistic Monadic Logic of Order). Formally the syntax of Probabilistic Monadic Logic of Order has in its vocabulary individual (first order) variables t0 , t1 , . . . , tk , monadic predicate variables (interpreted as finite sets), and unary predicate names (interpreted as probabilistic predicates) and one binary relation < (the order). We use lower case letters t, x, y to range over individual variables and upper case letters X, Y, Z to range over monadic variables and monadic predicate names. Atomic formulas are of the form X(t), t1 < t2 and t1 = t2 . Well formed formulas of the monadic logic PMLO are obtained from atomic formulas using Boolean connectives ¬, ∨, ∧, →, the (first order) quantifiers ∃t and ∀t, second order quantifiers ∃X and ∀X, and probabilistic constructs Prob>q (ϕ) and Prob>q (ϕ | ψ), where q is a rational number. The formulas without probabilistic constructs are formulas of the Weak Monadic Logic of Order (WMLO) - this logic plays an important role in automata theory. The probabilistic structures used in this section are defined by Finite Probabilistic Processes. We study the following model-checking problem: decide whether a given PMLO-formula ϕ holds on the structure defined by a given Finite Probabilistic Process. We introduce a rather large subclass C of formulas for which the model-checking problem is ‘almost always decidable’. Subsection 4.1 explains how Finite Probabilistic Processes define probabilistic structures. Subsection 4.2 introduces a class C of formulas with decidable model-checking problem and states the main results of the paper. 4.1 Probabilistic Structures defined by Finite Probabilistic Processes Definition 1 A Finite Probabilistic Process is a finite labeled Markov chain [KS60] M = (S, P, V, L), where S is a finite set of states, P is a transition probability matrix: S 2 → [0, 1] such that P (i, j) is a rational 5 P number for all (i, j) ∈ S 2 , j∈S P (i, j) = 1 for every i ∈ S, and V : S → 2L is a valuation function which assigns to each state a set of symbols from a finite set L. The pair (S, P ) is called a finite Markov chain. The following Lemma is a well known fact in the theory of matrices (see e. g. [Gan77],13.7.5, 13.7.1) Lemma 1 Let (S, P ) be a finite Markov chain. There exists a positive natural number d period of the Markov chain such that the limits lim P r+dm = Pr (r = 0, 1, . . . , d − 1) m→∞ exist. Moreover if the elements of P are rational, then these limits are computable from P and the convergence to the limits is geometric, i. e. |P r+dm (i, j) − Pr (i, j)| < a · bm when m ≥ m0 for some positive rationals a, b < 1 and natural m0 also computable from P . Given a Finite Probabilistic Process M = (S, P, V, L) and a state s, we define a probabilistic structure M s as follows: Signature: a deterministic binary predicate <, and monadic probabilistic predicates Q for every label Q ∈ L. Interpretation: • the universe of the structure Ms is the set N of natural numbers; • < is interpreted as the standard less relation over N; • probabilistic space (Ω, ∆, µ)(see [KSK66]) : Ω = sS ω is the set of all infinite sequences of states starting from s, ∆ is the σ-algebra generated by theQbasic cylindric sets Du = uS ω , for every u ∈ sS ∗ , and the probability measure µ is defined by µ(Du ) = i=0,...,n−1 P (si , si+1 ) where u = s0 s1 ...sn ; • interpretation of monadic probabilistic predicates: for each ω = s0 s1 ...sn ... ∈ Ω, for each n ∈ N we have π(Q)(ω, n) iff Q ∈ V (sn ) (i.e. Q belongs to the label of state sn ). At this point, notice that for every integer n, the set {ω ∈ Ω : π(Q)(ω, n)} is µ-measurable since it is a finite union of basic cylinders. Example. Let us consider a Call Establishment procedure in a simple telephone network where the capacity of simultaneous outgoing calls is less than the number of users. An abstraction of this procedure represents the behavior of a user where time is assumed to be discrete (Figure 1 ). 0.7 W 2/7 alloc 0.3 clear 5/7 Figure 1. C To simplify it is assumed that a user which is not connected is continuously attempting to get a connection (state W ait) and at each time moment he succeeds to be connected with probability 3/10. Moreover when the calling is established the duration of the call (state Call) follows a geometric distribution: at each time moment, the probability to finish the call has probability 5/7. The set of labels here is equal to the set of states, and the label of a state is the state itself. One can write a liveness property such that: ϕ =df ∀t Prob=1 (∃ t0 > t Call(t0 ) | W ait(t)) (1) which expresses that at every time, if the user is waiting for a connection, the probability that he will be served later is equal to one. One can also express some probabilistic property concerning the time the user has to wait before being served: ψ =df ∀t Prob≥0.9 (∃t0 (t < t0 ∧ t0 < t + 3 ∧ Call(t0 )) | W ait(t)) (2) One can prove that MW ait |= ϕ and MW ait 6|= ψ. 6 4.2 Statement of Main Results In this subsection we define some classes of formulas. Our main results (Theorems 3-5), roughly speaking, say that for these classes it is decidable whether a given formula in a class holds in the structure defined by a given Finite Probabilistic Process M . The proofs of these results will be provided in the next section. All our decidability results are only for formulas which do not contain conditional probability operators. From now on we will deal only with such formulas. Definition 2 A PMLO-formula ϕ belongs to the class C iff operators Prob >q are not nested, and for every subformula of ϕ of the form Prob>q ψ, the formula ψ does not contain free second order variables. If a PMLO-formula ϕ contains occurrences Prob>q only with q = 0 then ϕ is called a qualitative formula. If for every subformula of the form Prob>q ψ of a PMLO-formula ϕ , the formula ψ contains at most one free individual variable then ϕ is called a simple formula. For example ∃t∃t0 (t < t0 ∧ Prob>1/3 (P (t) ∧ P (t0 ) ∧ ∃Q∀t00 > t Q(t00 )) ∧ Prob>1/2 (¬P (t0 ))) (3) where P is a probabilistic predicate and Q a deterministic one, belongs to C. The properties expressed in (1) and (2) are simple formulas. As one more example that uses a weak second order quantification we can mention the following property: the probability that a given probabilistic predicate has an even number of elements is greater than 0.9. A PMLO-formula ϕ is called a sentence if it has no free variable and no probabilistic predicate is out of scope of an operator Prob. If ϕ is a sentence, M |= ϕ stands for M, ω |= ϕ, that is well-defined and is independent from ω and an interpretation of variables due to Proposition 3. The main results of this subsection are Theorems 3-5 which, roughly speaking, say that it is decidable whether a given formula ϕ ∈ C holds in the structure defined by a given Finite Probabilistic Process M . In order to express our decidability result about model-checking, we need to introduce the notion of parametrized formula of logic of probability. The set of parametrized formulas is defined similarly to the set of formulas except that operators Prob >q with q ∈ Q are replaced by Prob>p , where p is a parameter name. For example ∃t∃t0 (t < t0 ∧ Prob>p1 (P (t) ∧ P (t0 ) ∧ ∃Q∀t00 > t Q(t00 )) ∧ Prob>p2 (¬P (t0 ))) is a parametrized formula. Let ϕ be a parametrized formula with parameters p1 , . . . , pm and α1 , . . . , αm be a sequence of rational values. We denote by ϕα1 ,...,αm the formula obtained by replacing in ϕ each parameter pi by the value αi . The set of parametrized sentences is defined exactly like the set of sentences. By abuse of terminology, we say that a parametrized formula ϕ belongs to C if all (or, equivalently, any of) its instances ϕ α1 ,...,αm are in C. Below, for simplicity, we will write ProbMs (ϕ(n1 , . . . , nk )) instead of µ{ω : Ms , n1 , . . . , nk , ω |= ϕ(t1 , . . . , tk )} for a Finite Probabilistic Process M , state s of M and (n1 , . . . , nk ) ∈ Nk . Now, we are ready to state the main technical theorem. Theorem 2 Let M be a Finite Probabilistic Process, s0 be a state of M , and ϕ(t1 , . . . , tk ) be a parametrized formula ϕ(t1 , . . . , tk ) without free predicate variables and with m parameters. (1) If formula ϕ is in the class C and is simple, one can compute for each parameter p i in ϕ (i = 1, . . . , m) a finite set Hi of rational values not containing zero such that for each tuple of rationals α = (α 1 , . . . , αm ) where αi ∈ Q \ Hi , i = 1, . . . , m, one can compute a WMLO-formula ψ(t1 , . . . , tk ) such that for n1 , . . . , nk ∈ N 7 (M, s0 ) satisfies ϕα (n1 , . . . , nk ) iff (N, <) |= ψ(n1 , . . . , nk ). (2) If formula ϕ is in the class C, then for each rational number ² > 0, one can compute for each parameter p i in ϕ (i = 1, . . . , m) a set Hi union of a finite set of intervals not containing zero, with total length less than ², such that for each tuple of rationals α = (α1 , . . . , αm ) where αi ∈ Q \ Hi , i = 1, . . . , m, one can compute a WMLO-formula ψ(t1 , . . . , tk ) such that for n1 , . . . , nk ∈ N (M, s0 ) satisfies ϕα (n1 , . . . , nk ) iff (N, <) |= ψ(n1 , . . . , nk ). Remarks. 1. The complexity of our decision procedure is mainly determined by the complexity of decision procedure for MLO-formulas (that is non-elementary in the worst case). 2. The fact that we cannot treat some set of exceptional values seems to be essential from mathematical point of view. One cannot exclude that the model-checking problem is undecidable for these exceptional values. However, for practical properties the values of probabilities can always be slightly changed without loss of its essential significance, and this permits to eliminate these exceptional values of probabilities. From Theorem 2 and from the fact that the validity problem for WMLO is decidable, one deduces immediately the three following decidability results: Theorem 3 (Qualitative model-checking) Given a qualitative sentence ϕ in the class C, a Finite Probabilistic Process M , a state s of M , it is decidable whether ϕ holds in the probabilistic structure M s . Theorem 4 Given a Finite Probabilistic Process M , a state s of M and a parametrized simple sentence ϕ in the class C with m parameters, one can compute for each parameter p i in ϕ a finite set Hi (i = 1, . . . , m), such that for each tuple α = (α1 , . . . , αm ) where αi ∈ Q \ Hi , i = 1, . . . , m, it is decidable whether ϕ holds in the probabilistic structure Ms . Theorem 5 Given a Finite Probabilistic Process M , a state s of M , a parametrized sentence ϕ in the class C with m parameters, and a rational number ² > 0, one can compute for each parameter p i in ϕ (i = 1, . . . , m) a finite set Hi of intervals, not containing zero, with total length less than ², such that for each tuple α = (α1 , . . . , αm ) where αi ∈ Q \ Hi , i = 1, . . . , m, it is decidable whether ϕ holds in the probabilistic structure Ms . 5 Proof of Theorem 2 Before providing the proof of theorem 2 let us illustrate the model-checking procedure on a simple example. Assume that M is a finite state labelled Markov chain. Moreover assume that (1) its matrix P is regular, i.e. limn→∞ P n exists and (2) there is exactly one state s1 labelled by a predicate Q1 . Let ϕ(t) be the formula Prob>1/2 Q1 (t). In order to check whether ϕ is satisfiable in the structure Ms0 we can do the following. First observe that the probability that Q1 (t) holds at moment n in the structure Ms0 is (P n )0,1 . Second, compute Pb = limn→∞ P n ; and let λ = Pb0,1 . (This step is computable by Lemma 1). Now proceed by the following cases: Case λ > 1/2 In this case Prob>1/2 Q1 (n) holds in Ms0 for all n which are big. Therefore, Prob>1/2 Q1 (t) is satisfiable in Ms0 . 8 Case λ < 1/2 In this case by Lemma 1 we can compute n0 such that for all n > n0 the probability that Q1 (n) holds will be ∼ λ < 1/2. Therefore, Prob>1/2 Q1 (t) is satisfiable iff it is satisfiable for n ≤ n0 . The last condition can be checked by verifying if there is n < n0 such that (P n )0,1 > 1/2. Case λ = 1/2 In this case we have to verify that there is n such that (P n )0,1 > 1/2. We do not know how to treat this exceptional case. From the above description it is clear how to model-check the parametrized formula Prob >r Q1 (t) on Ms0 for all values of the parameter r except one value λ. Moreover, the above arguments show that for r 6= λ the set of n which satisfy Prob>r Q1 (t) is either finite (Case λ < r) or cofinite (case λ > r). The procedure for model-checking of arbitrary formulas is similar to the procedure described above. The above assumption that P is regular is not essential and can be easily removed. More difficult part of the proof is a reduction of arbitrary formulas to simpler formulas. This is done in the rest of this section. 5.1 Future and Past Formulas and Decomposition Lemma We introduce a notation: N≥a = {n ∈ N | n ≥ a} and recall what are future and past WMLO-formulas. Definition 3 A WMLO-formula ϕ(x0 , X1 , X2 , ..., Xm ) with only one free first-order variable x0 is a future formula if for every a ∈ N and every m subsets S1 , S2 , .., Sm of N, the following holds: (N, a, S1 , S2 , .., Sm ) |= ϕ(x0 , X1 , X2 , ..., Xm ) 0 ) |= ϕ(x0 , X1 , X2 , ..., Xm ) iff (N≥a , a, S10 , S20 , .., Sm where Si0 = Si ∩ N≥a for i = 1, 2, ..., m. Past WMLO-formulas are defined in a symmetric way. Note that this is a semantic notion. It is convenient to extend the system of monadic logic of order with the bounded existential quantifiers ≥t2 ≥t2 ∃t≤t1 , ∃t≤t , ∃t≥t1 . Semantically, ∃t≤t ϕ, where t1 and t2 are free in ϕ is a shorthand for ∃t t1 ≤ t ∧ t ≤ t2 ∧ ϕ. 1 1 Similarly,∃t≤t1 ϕ (resp. ∃t≥t1 ϕ), where t1 is free in ϕ is a shorthand for ∃t t ≤ t1 ∧ ϕ (resp. ∃t t ≥ t1 ∧ ϕ). There is a syntactic characterization of future and past formulas. Proposition 6 A WMLO-formula ϕ(x0 , X1 , X2 , ..., Xm ) with only one free first-order variable x0 is a future (resp. past) formula iff it is (semantically) equivalent to a formula where all first order quantifiers are relativized to ≤ x0 (resp. ≥ x0 , i.e. are of the form ∃t≤x0 (resp. ∃t≥x0 ). Similar to Lemma 9.3.2 in [GHR94] we have the following Decomposition Lemma for WMLO-logic: Lemma 2 (Decomposition Lemma) The formula t1 < t2 < . . . < tk ∧ψ(t1 , t2 , . . . , tk ) where ψ(t1 , t2 , . . . , tk ) is a WMLO-formula with only free variables t1 , . . . , tk is equivalent to a finite disjunction of formulas of the form: W i∈I ϕi,← (t1 ) ∧ ψi,1 (t1 , t2 ) ∧ . . . ∧ ψi,k−1 (tk−1 , tk ) ∧ ϕi,→ (tk ) where 1. ϕi,← (t1 ) is a past formula 2. ϕi,→ (tk ) is a future formula ≥t 3. in ψi,j (tj , tj+1 ) only tj and tj+1 are free and all first order quantifiers are of the form ∃t≤tjj+1 , for j = 1, . . . , k − 1. Moreover, formulas ϕi,← , ϕi,→ , ψi,j are computable from ψ and for i1 6= i2 , the disjuncts ϕi1 ,← (t1 ) ∧ ψi1 ,1 (t1 , t2 ) ∧ . . . ∧ ψi1 ,k−1 (tk−1 , tk ) ∧ ϕi1 ,→ (tk ) and ϕi2 ,← (t1 ) ∧ ψi2 ,1 (t1 , t2 ) ∧ . . . ∧ ψi2 ,k−1 (tk−1 , tk ) ∧ ϕi2 ,→ (tk ) are mutually exclusive. 9 5.2 Ultimately periodic sets We say that a set S ⊆ Nk is ultimately periodic with period d, dimension k and displacement h if for all n1 , . . . , nk ∈ N: if ni ≥ h then (n1 , . . . , ni . . . , nk ) ∈ S iff (n1 , . . . , ni + d . . . , nk ) ∈ S. Notice that in dimension one, an ultimately periodic set with period one is exactly a finite or cofinite set. It is not true in higher dimensions. A finite set J ⊆ Nk is a representation of S if (n1 , . . . , ni . . . , nk ) ∈ S iff there is (m1 , . . . , mi . . . , mk ) ∈ J such that: for all i ∈ {1, . . . , k} mi = ni < h or (mi , ni ≥ h and mi = ni mod d). Lemma 3 (Properties of ultimately periodic sets) 1. If a set is ultimately periodic then its complement is ultimately periodic. 2. If S1 , S2 ⊆ Nk are ultimately periodic then S1 ∪ S2 , S1 ∩ S2 are ultimately periodic. 3. Every ultimately periodic set has a finite representation. 4. If S ⊆ Nk is ultimately periodic then there exists a WMLO-formula θ(t1 , . . . , tk ) such that (N, <) |= θ(n1 , . . . , nk ) iff n1 < n2 < . . . < nk and (n1 , n2 − n1 , n3 − n2 , . . . , nk − nk−1 ) ∈ S. Proof. The first two properties are easy to prove. We prove the last ones. Proof of (3). If S ⊆ Nk is an ultimately periodic set with period d, dimension k and displacement h, then Vk the set {(n1 , . . . , nk ) : (n1 , . . . , nk ) ∈ S ∧ i=1 ni < h + d} is a finite representation of S. Proof of (4). For i < d ∈ N let Θi,d (t1 , t2 ) be the the conjunction of 1. t1 < t2 2. there are predicate variables Z0 , . . . Zd−1 such that (a) The sets Z0 , . . . Zd−1 partition interval [t0 , t1 ] Vd−1 (b) ∀t(t1 ≤ t < t2 ) → j=0 (t ∈ Zj ↔ t + 1 ∈ Zj+1 mod d ) (c) t1 ∈ Z0 and t2 ∈ Zi Observe that Θi,d (n1 , n2 ) holds iff n1 < n2 and n2 − n1 = i mod d. From Θi,d and the finite representation J of S given above one can construct the desirable formula, since (n1 , n2 − n1 , n3 − n2 , . . . , nk − nk−1 ) ∈ S is equivalent to: _ k ^ (ni − ni−1 = mi ∨ θmi −d (ni−1 , ni ) (m1 ,...,mk )∈J i=1 with n0 = 0. ¥ 10 5.3 A Lemma from Analysis The next lemma is a simple lemma from Analysis: Lemma 4 For 1 ≤ i ≤ k, 1 ≤ j ≤ m, let Pi,j be probabilistic rational matrices of size N × N , and Ii,j (resp. Fi,j ) be row (resp. column) of rational vectors of size N with all elements positive or equal to zero and n n cj ∈ Q+ . Suppose that matrices Pi,j have a limit when n → ∞. Let ai,j,n = Ii,j · Pi,j · Fi,j . Let Lp = {(n1 , . . . , nk ) ∈ N k : m X (cj · j=1 k Y ai,j,ni ) > p} i=1 1. if p = 0 then Lp is ultimately periodic with period one. 2. if p 6= 0 (a) if k = 1, then there is a computable finite set H such that for every rational p 6∈ H, the set L p is finite or cofinite, i.e. ultimately periodic with period one. (b) if k 6= 1 then for every rational ² > 0 there is a computable set H which is union of a finite set of intervals with total length at most ² such that for every rational p 6∈ H the set L p is ultimately periodic with period one In all cases a finite representation of Lp is computable. Proof. We study first the case when p = 0. In this case, (n1 , . . . , nk ) ∈ L0 iff there exists j ∈ {1, . . . m} such that for all i ∈ {1, . . . , k} ai,j,ni > 0. Let Gi,j be the graph with vertices 1, . . . , N and (s, s0 ) is an edge iff Pi,j (s, s0 ) > 0. Let S be the set of vertices s such that Ii,j (s) > 0 and S 0 be the set of vertices s0 such that Fi,j (s0 ) > 0. We have ai,j,ni > 0 iff there exists in the graph Gi,j a vertex s in S, a vertex s0 in S 0 and a path from s to s0 with length ni . It is well known that the set Cs,s0 of values n ∈ N such that there exists in a graph G a path of length n from a vertex s to another one s0 is ultimately periodic and has a computable finite representation since it is a regular language over a unary alphabet. Thus the set L 0 as a finite union of products of ultimately periodic subsets of N is an ultimately periodic set, and a finite representation of L 0 is computable. We study now the case when p > 0. Define: Pm Qk ∆(n1 , . . . , nk ) = j=1 (cj · i=1 ai,j,ni ). Pm Qk Let l = limn1 →∞,...,nk →∞ ∆(n1 , . . . , nk ) = j=1 (cj · i=1 limni →∞ ai,j,ni ) Qk Pm ni ) · Fi,j ). = j=1 (cj · i=1 Ii,j · (limni →∞ Pi,j From Lemma 1 the limit l is rational and computable. The proof of (2) is by induction on k. Case k = 1 and p > 0: – If l = 0 then limn1 →∞ ∆(n1 ) = 0 and so Lp = {n1 : ∆(n1 ) > p} is a finite set. – If l 6= 0, let H = {l}. If p > l, then Lp is finite. If p < l then Lp is cofinite so Lp is ultimately periodic with period one. In both cases, a finite representation of Lp is computable due to the exponential convergence of the matrices to the limit as stated in Lemma 1. 11 Case k > 1 and p > 0: For every rational ² there exists an integer N such that if n1 , . . . , nk ≥ N then |∆(n1 , . . . , nk ) − l| < ²/4 (4) Let: Nk<N = {(n1 , . . . , nk ) ∈ Nk | ni < N for i = 1, . . . , k}, and Nk≥N = {(n1 , . . . , nk ) ∈ Nk | ni ≥ N for i = 1, . . . , k}. For i ∈ {1, . . . , k} and ni ∈ {0, . . . , N − 1} let : Nki,ni = Ni−1 {ni }Nk−i . ni =N −1 k We have Nk = Nk≥N ∪ Nk<N ∪ (∪i=k Ni,ni ). i=1 ∪ni =0 We will prove that the intersection of Lp with each of the sets Nk<N , Nk≥N , and Nki,ni is ultimately periodic and a finite representation of the intersection is computable. Firstly from (4) we deduce that for each p such that |p − l| > ²/4, the set Nk≥N ∩ Lp = {(n1 , . . . , nk ) ∈ Nk≥N | ∆(n1 , . . . , nk ) > p} is ultimately periodic with period one and a finite representation of this set is computable. Secondly the set Nk<N ∩ Lp is finite and computable. Thirdly fix i0 ∈ {1, . . . , k} and ni0 ∈ {0, . . . , N − 1}. A tuple (n1 , . . . , nk ) ∈ Nki0 ,ni satisfies 0 ∆(n1 , . . . , nk ) > p m X (cj · ai0 ,j,ni0 iff Y · ai,j,ni ) > p). j=1 (5) i6=i0 Let Cj = cj · ai0 ,j,ni0 . Note that (5) can be rewritten as: m X j=1 (Cj · Y ai,j,ni ) > p). (6) i6=i0 Let ²0 = ²/2kN . Using induction hypothesis, there exists a computable set H i0 ,ni0 , union of a finite number of intervals with a sum of lengths at most ²0 such that if a rational p 6= 0 is not in Hi0 ,ni0 then the set of tuples (n1 , . . . , ni0 −1 ,ni0 +1 , . . . , nk ) solution of (6) is ultimately periodic with period one and with a computable finite representation. Thus for a fixed (i0 , ni0 ), if rational p is not in a finite number of intervals the sum of lengths of which is at most ²/2kN , the set of tuples in Nki,ni which satisfy the inequation (5) is ultimately periodic with period one and with a computable finite representation. Finally, the intervals of excluded values of p are computable, have a total length less than 2 × ²/4 + kN · ²/2kN = ², and the total number of intervals is finite. The proof is done. ¥ 5.4 Technical Lemmas Theorem 4.1.7 [CY95] gives the following corollary that we will use: Theorem 6 Let ϕ(t) be a future WMLO-formula, M be a Finite Probabilistic Process and s be a state of M . The probability fs that ϕ(0) holds in Ms is computable from M , s and ϕ. 12 Lemma 5 (Past formulas) Let ϕ(t) be a past WMLO-formula, M be a Finite Probabilistic Process and s 0 be a state of M . There is a probabilistic matrix Q and vectors u and v such that for every n ∈ N the probability that ϕ(n) holds in Ms0 is equal to uQn v. Moreover, Q, u and v are computable from M, s0 and ϕ. Proof. Let ϕ(t) be a past WMLO-formula. A structure S for such a formula ϕ is defined as an infinite word on the alphabet Σ = 2L where L is the set of monadic symbols of ϕ(t). The property defined by ϕ(t) depends only on the prefix of size t + 1 of a model. Thus from [Büc60], there exists a computable finite complete deterministic automaton A on the alphabet Σ accepting a language of finite words L(A) such that S, n |= ϕ(t) iff the prefix of S of size n + 1 belongs to L(A). Therefore, given the automaton A and the Finite Probabilistic Process M , we build a new Finite Probabilistic Process M 0 , “product” of M and A in the following way: States of M 0 are pairs (q, s) where q is a state of A and s is a state of M . There is a transition from (q, s) to (q 0 , s0 ) iff (q, σ, q 0 ) is a transition in A, where σ is the valuation of s in M and the probability of this transition is the same as the probability of (s, s0 ) in M . At last, the set of labels L0 of M 0 is reduced to one symbol F and the valuation of (q, s) is {F } if q is a final state in A, and ∅ otherwise. We have : 0 (F (n)) ProbMs0 (ϕ(n)) = ProbM(q ,s ) 0 0 where q0 is the initial state of A and F is the monadic probabilistic symbol defined by L 0 . Let Q be the transition probability matrix of the Markov chain M 0 , let u be the row vector with null components except u(q0 ,s0 ) which is equal to 1, and let v be the column vector with null components except v(q,s) which are equal to 1 if q ∈ F . We have: 0 (F (n)) = uQn v. So fs0 = uQn v is computable. ¥ ProbM(q ,s ) 0 0 2 Lemma 6 Let ϕ(t1 , t2 ) be a formula with all first order quantifiers of the form ∃t≤t l≥t1 , and ψ(t1 ) be a past formula. Let M be a Finite Probabilistic Process and si , sj be two of its states. For n1 , n2 ∈ N, ProbMsi (ψ(n1 ) ∧ Sj (n1 ) ∧ ϕ(n1 , n1 + n2 )) = ProbMsi (ψ(n1 ) ∧ Sj (n1 )) · ProbMsj (ϕ(0, n2 )), where Sj (t) is a predicate which is true exactly in state sj . Proof. The set of elements from the probabilistic space Ω = si S ω which satisfy ψ(n1 )∧Sj (n1 )∧ϕ(n1 , n1 +n2 ) can be written as a concatenation product Ω1 · Ω2 where Ω1 is the set of finite paths of length n1 starting in si ending in sj and satisfying ψ(n1 ), and Ω2 is the set of infinite paths starting in sj and satisfying ϕ(0, n2 ), ≤t2 this is due to the fact that all quantifiers of ϕ are of the form ∃tl≥t . Thus, 1 ProbMsi (ψ(n1 ) ∧ Sj (n1 ) ∧ ϕ(n1 , n1 + n2 )) = ProbMsi (Sj (n1 ) ∧ (ψ(n1 )) · ProbMsj (ϕ(0, n2 )). ¥ Lemma 7 Let k, m ∈ N. For 1 ≤ i ≤ k, 1 ≤ j ≤ m, let Mi,j be a Finite Probabilistic Process, si,j be a state of Mi,j , ϕi,j (ti ) be a past WMLO-formula with only one free variable ti , and cj ∈ Q+ . Let X Lp = {(n1 , . . . , nk ) ∈ Nk : cj · ProbM1,j ,s1,j (ϕ1,j (n1 )) · . . . · ProbMk,j ,sk,j (ϕk,j (nk )) > p} 1≤j≤m 1. if p = 0 then Lp is ultimately periodic. 2. if p 6= 0 13 (a) if k = 1, then there is a computable finite set H such that for every rational p 6∈ H, the set L p is finite or cofinite, i.e. ultimately periodic. (b) if k 6= 1 then for every rational ² > 0 there is a computable set H which is union of a finite set of intervals with total length at most ² such that for every rational p 6∈ H the set L p is ultimately periodic. In all cases a finite representation of Lp is computable. Proof. Using Lemma 5, one can compute for each 1 ≤ i ≤ k, and 1 ≤ j ≤ m, a probabilistic matrix Q i,j , and vectors ui,j , vi,j , such that the probability that (Mi,j,si,j , ni ) satisfies ϕi,j (ti ) is equal to ui,j · Qni,ji · vi,j . Let d be the least common multiple of the periods of the Markov chains with matrix Q i,j (for 1 ≤ i ≤ k and 1 ≤ j ≤ m). By Lemma 1 limn→∞ (Qdi,j )n exists. Let Q0 i,j be Qdi,j . If we write ni = ri + dn0i , with 0 ≤ ri < d, then n0 ui,j · Qni,ji · vi,j = ui,j · (Qdi,j )ni · (Qri,ji · vi,j ) = ui,j · Q0 i,ji · v 0 i,j = ai,j,n0 i . 0 n Using Lemma 1, limn→∞ Q0 i,j exists, so the hypothesis of Lemma 4 are satisfied. Therefore, Lp is an ultimately periodic set with period d and the present Lemma is proven. ¥ Lemma 8 Let M be a Finite Probabilistic Process, s be a state of M , and ϕ(t1 , . . . , tk ) be a WMLO-formula with only free variables t1 , . . . , tk . Let (Nk )ϕ,p =df {(n1 , . . . , nk ) ∈ Nk | Ms , n1 , n1 + n2 , . . . , nk−1 + nk |= Prob>p (ϕ(t1 , . . . , tk ))} 1. if p = 0 then (Nk )ϕ,p is ultimately periodic. 2. if p 6= 0 (a) if k = 1, then there is a computable finite set H such that for every rational p 6∈ H, the set (N k )ϕ,p is finite or cofinite, i.e. ultimately periodic. (b) if k 6= 1 then for every rational ² > 0 there is a computable set H which is union of a finite set of intervals with total length at most ² such that for every rational p 6∈ H the set (N k )ϕ,p is ultimately periodic. In all cases a finite representation of (Nk )ϕ,p is computable. Proof. Without loss of generality, one can reduce the proof to the case when ϕ(t1 , . . . , tk ) is of the form t1 < t2 < . . . < tk ∧ ϕ0 (t1 , t2 , . . . , tk ). Moreover using Lemma 2 the formula t1 < t2 < . . . < tk ∧ ϕ0 (t1 , t2 , . . . , tk ) is equivalent to a finite disjunction of formulas of the form: W ϕ (t1 ) ∧ ϕi,1 (t1 , t2 ) ∧ . . . ∧ ϕi,k−1 (tk−1 , tk ) ∧ ϕi,→ (tk ) i,← i∈I where 1. ϕi,← (t1 ) is a past formula 2. ϕi,→ (tk ) is a future formula 14 3. in ϕi,j (tj , tj+1 ) only tj and tj+1 are free and all quantifiers are relativized to between tj and tj+1 (i.e. ≥t of the form ∃t≤tjj+1 , for j = 1, . . . , k − 1). Moreover, formulas ϕi,← , ϕi,→ , ψi,j are computable from ψ and for i1 6= i2 , the disjuncts ϕi1 ,← (t1 ) ∧ ψi1 ,1 (t1 , t2 ) ∧ . . . ∧ ψi1 ,k−1 (tk−1 , tk ) ∧ ϕi1 ,→ (tk ) and ϕi2 ,← (t1 ) ∧ ψi2 ,1 (t1 , t2 ) ∧ . . . ∧ ψi2 ,k−1 (tk−1 , tk ) ∧ ϕi2 ,→ (tk ) are mutually exclusive. For each state j of M we introduce a new probabilistic predicate Sj , and add Sj in the valuation of state j. Let M 0 be the new Finite Probabilistic Process obtained in this way. The following equalities hold for every tuple of integers n01 , . . . , n0k , where Q is the set of states of M : ProbMs (n01 W < n02 < . . . < n0k ∧ ϕ0 (n01 , n02 , . . . , n0k )) 0 0 0 0 0 = Prob P Ms ( i ϕi,← (n1 ) ∧0 ψi,1 (n1 , n02 ) ∧0 . . . ∧ ψi,k−1 (nk−10, tk ) ∧ ϕi,→ (nk )) 0 = Pi∈I ProbMs (ϕi,← (n1 ) ∧ ψi,1 (n1 , n2 ) ∧ . . . ∧ ψi,k−1 (nk−1 , tk ) ∧ ϕi,→ (nk )) = i∈I,j1 ,...jk ∈Q ProbMs (ϕi,← (n01 )∧Sj1 (n01 )∧ψi,1 (n01 , n02 )∧Sj2 (n02 )∧. . .∧Sjk−1 (n0k−1 )∧ψi,k−1 (n0k−1 , n0k )∧ Sjk (0 nk ) ∧ ϕi,→ (n0k )) and Pusing Lemma 6 iteratively k times: = i∈I,j1 ,...jk ∈Q ProbMs (ϕi,← (n01 ) ∧ Sj1 (n01 )) · ProbMj1 (ψi,1 (0, n02 −0 n1 ) ∧ Sj2 (n02 −0 n1 )) · . . . . . . · ProbMjk−1 (ψi,k−1 (0, n0k − n0k−1 ) ∧ Sjk (n0k − n0k−1 )) · ProbMjk (ϕi,→ (0)). We can compute the rational constants ProbMjk (ϕi,→ (0)) using Theorem 6. Then we apply Lemma 7 with n1 = n01 and ni = n0i − n0i−1 for i = 2, . . . , k to finish the proof. ¥ Proof (of Theorem 2) For each i = 1, . . . , m, let ψi be the subformula of ϕ of the form Prob>pi ϕi (t1 . . . , tk ). One can compute using Lemma 8 a set of probabilities Hi not containing zero, such that for each value αi ∈ Q \ Hi , the set Rαi = {(n1 , . . . , nk ) : Ms0 , n1 , n1 + n2 , . . . , nk−1 + nk |= Prob>αi ϕi (t1 . . . , tk )}, is ultimately periodic with a computable finite representation. Moreover if k = 1, the sets Hi are finite. Using Lemma 3, there is a WMLO-formula θαi (t1 , . . . tk ) such that θαi (n1 , . . . nk ) holds iff (n1 , . . . , nk ) ∈ Rαi .Thus the PMLO subformula Prob>αi ϕi (t1 . . . , tk )} of ϕα can be replaced by the WMLO-formula θαi (t1 , . . . tk ). Consider now the WMLO-formula ψ(t1 , . . . , tk ) obtained from ϕα eliminating in the way just described all the probabilistic operators. We have: (M, s0 ) satisfies ϕα (n1 , . . . , nk ) iff (N, <) |= ψ(n1 , . . . , nk ). ¥ 6 Extension of decidable model-checking to nested formulas In class C we disallow nesting of Prob operators. Below we prove that the decidability results can be extended to formulas with nested Prob. Definition 4 A PMLO-formula ϕ belongs to the class C 0 iff in every subformula of the form Prob>q ψ, the formula ψ does not admit free second order deterministic variable. Definition 5 Let ² > 0 be a real number. The ²-thin subsets of Qn are defined by the induction on n as follows. 15 (1) S ⊂ Q is ²-thin if and only if S can be covered by a finite set of intervals of total length < ². (2) S ⊂ Qd+1 is ²-thin if there is an ²-thin set S1 ⊂ Q and i ≤ d + 1 such that for every qi 6∈ S1 the set {hq1 , . . . , qi−1 , qi+1 , . . . , , qd+1 i : hq1 , . . . qd , qd+1 i ∈ S} is ²-thin subset of Qd . Definition 6 Let the following recursive definition of a 0-thin subset of Q n : (1) S ⊂ Q is 0-thin if S is finite. (2)S ⊂ Qd+1 is 0-thin if there is an 0-thin set S1 ⊂ Q and i ≤ d + 1 such that for every qi 6∈ S1 the set {hq1 , . . . , qi−1 , qi+1 , . . . , , qd+1 i : hq1 , . . . qd , qd+1 i ∈ S} is 0-thin subset of Qd . Recall that if ϕ is a parametrized formula with parameters p1 , . . . , pm and α = (α1 , . . . , αm ) is a sequence of rational values then we denote by ϕα the formula obtained by replacing in ϕ each parameter pi by the value αi . Theorem 7 Let M be a Finite Probabilistic Process, s0 be a state of M , and ϕ(t1 , . . . , tk ) be a parametrized formula in the class C 0 with m parameters. 1. There exists a WMLO-formula ψ(t1 , . . . , tk ) such that for each (n1 , . . . , nk ) ∈ Nk (M, s0 ) satisfies ϕ(0,...,0) (n1 , . . . , nk ) iff (N, <) |= ψ(n1 , . . . , nk ). 2. For every rational ² > 0, there exists a computable ²-thin set H ⊂ (Q + )m such that for each tuple of (rational) values α = (α1 , . . . , αm ) 6∈ H there is a WMLO-formula ψα (t1 , . . . , tk ) such that (M, s0 ) satisfies ϕα (n1 , . . . , nk ) iff (N, <) |= ψα (n1 , . . . , nk ). 3. If ϕ is simple, there exists a computable 0-thin set H ⊂ (Q+ )m such that for each tuple of (rational) values α = (α1 , . . . , αm ) 6∈ H there is a WMLO-formula ψα (t1 , . . . , tk ) such that (M, s0 ) satisfies ϕα (n1 , . . . , nk ) iff (N, <) |= ψα (n1 , . . . , nk ). Proof. The proof is by induction on the depth l of the nesting. Case (1) is easy using Theorem 2. (2) The result is true for l = 1 (Theorem 2). Consider now a formula ϕ of depth l > 1. We have just to treat every subformula of ϕ of the form Prob>p1 (φ(t0 1 , . . . , t0 k0 )) where φ(t0 1 , . . . , t0 k0 ) is a parametrized formula of depth l − 1 in the class C 0 , with parameters p2 , . . . , pm . By induction hypothesis, for every rational ² > 0 there exists a set of bad values B² ⊂ Ql−1 which is ²-thin such that for a fixed good tuple (q2 , . . . , ql ) 6∈ B² , one can replace φ(t0 1 , . . . , t0 k0 ) by a WMLO-formula θ(t0 1 , . . . , t0 k0 ). For a fixed good tuple (q2 , . . . , ql ), after the replacement, we obtain an unnested formula ψ(t0 1 , . . . , t0 k0 ) of the form Prob>p1 (θ(t0 1 , . . . , t0 k0 )). Now we can proceed and find for ψ a set I(q2 ,...,ql ) of bad values of p1 which is ²-thin, and if q1 is a good value for the corresponding ψ (i.e. q1 6∈ I(q2 ,...,ql ) ) then using Theorem 5 one can compute a WMLO-formula ψ 0 (t0 1 , . . . , t0 k0 ) such that for (n1 , . . . , nk0 ) ∈ Nk (M, s0 ) satisfies ψ(n1 , . . . , nk0 ) iff (N, <) |= ψ 0 (n1 , . . . , nk0 ). It means that in ϕ, Prob>p1 (φ(t0 1 , . . . , t0 k0 )) can be replaced by ψ 0 (t0 1 , . . . , t0 k0 ) The set of bad values for parameters p1 , . . . , pl in Prob>p1 (φ(t1 , . . . , tk )) associated to ² is of the form Q · B² ∨ ∨(q2 ,...,ql )6∈B² I(q2 ,...,ql ) · {(q2 , . . . , ql )}. This set is clearly ²-thin, and the proof is done. Case(3) is similar to case (2). ¥ As a consequence of Theorem 7 we get the three following decidability results: 16 Theorem 8 (Qualitative model-checking) Given a qualitative sentence ϕ in the class C 0 , a Finite Probabilistic Process M , a state s of M , it is decidable whether ϕ holds in the probabilistic structure M s . Theorem 9 Given a Finite Probabilistic Process M , a state s of M and a parametrized simple sentence ϕ in the class C 0 with m parameters, there exists a computable 0-thin set H ⊂ (Q+ )m such that for each tuple of (rational) values α = (α1 , . . . , αm ) 6∈ H one can decide whether ϕα holds in the probabilistic structure Ms . Theorem 10 Given a Finite Probabilistic Process M , a state s of M and a parametrized sentence ϕ in the class C 0 with m parameters, for every rational ² > 0, there exists a computable ²-thin set H ⊂ (Q + )m such that for each tuple of (rational) values α = (α1 , . . . , αm ) 6∈ H one can decide whether ϕα holds in the probabilistic structure Ms . 7 Comparison with probabilistic temporal logic pCT L∗ The logic pCT L∗ is one of the most widespread among probabilistic temporal logics [ASB + 95]. The relationship between our logic and pCT L∗ is rather complex. The semantics for logic of probability is defined over arbitrary probabilistic structures, however pCT L∗ is defined only for Finite Probabilistic Processes. Moreover, unlike logic of probability, the truth value of pCT L∗ formula depends not only on the probabilistic structure defined by a Finite Probabilistic Process but also on the ‘branching structure’ of this process. Hence, there is no meaning preserving translation from pCT L∗ to monadic logic of probability. We also show below that even on the class of models restricted to Finite Probabilistic Processes no pCT L ∗ formula is equivalent to the probabilistic formula ∃t Prob≥1 Q(t), where Q is a probabilistic predicate symbol. Let us recall the syntax and the semantics of the logic pCT L∗ as defined in [ASB+ 95]. Formulas are evaluated on a Finite Probabilistic Process (S, P, V, L). There are two types of formulas in pCT L∗ : state formulas (which are true or false in a specific state) and path formulas (which are true or false along a specific path). Syntax. State formulas are defined by the following syntax: 1. each a in L is a state formula 2. If f1 and f2 are state formulas, then so are ¬f1 , f1 ∨ f2 3. If g is a path formula, then P r<q (g), P r>q (g) are state formulas for every rational number q. Path formulas are defined by the following syntax: 1. A state formula is a path formula 2. If g1 and g2 are path formulas, then so are ¬g1 , g1 ∨ g2 3. If g1 and g2 are path formulas, then so are Xg1 , g1 U g2 . (X and U are respectively the N ext and U ntil temporal operators). Semantics. Given a Finite Probabilistic Process M = (S, P, V, L) state formulas and path formulas are interpreted as defined below. Formulas f1 and f2 are state formulas and g1 and g2 are path formulas. Let s be a state, and Π be an arbitrary infinite path in M . Satisfaction of a state formula is defined with respect to s and satisfaction of a path formula with respect to Π. For each integer k ≥ 0, we denote by Π k the path obtained from Π when removing the first k states (thus Π0 = Π) and by [Π]k the kth state of Π. • M, s |= Q iff a ∈ V (Q), • M, s |= ¬f1 iff M, s 6|= f1 , M, s |= f1 ∨ f2 iff M, s |= f1 or M, s |= f2 , • M, s |= Prob>q (g1 ) iff µ{σ ∈ sS ω | M, σ |= g1 } > q, M, s |= Prob<q (g1 ) is defined in a similar way, • M, Π |= f1 iff [Π]0 |= f1 , 17 • M, Π |= ¬g1 iff M, Π 6|= g1 , M, Π |= g1 ∨ g2 iff M, Π |= g1 or M, Π |= g2 , • M, Π |= Xg1 iff M, Π1 |= g1 , • M, Π |= g1 U g2 iff there exists k ≥ 0 such that M, Πk |= g2 and for all 0 ≤ j < k, M, Πj |= g1 . Below we give an example that illustrate differences between the logic of probabilities and pCT L ∗ . Consider ∗ the Finite Probabilistic Processes K and L shown on ¢ Figure 2 below. Let ϕ be the following pCTL formula ¡ Prob=1 X(Prob= 21 (X P ) ∧ Prob= 12 (X Q)) . 1 1/2 1 s 1 1 1/2 P Note that K, s |= ϕ but L, s 6|= ϕ. However, the probabilistic structures Ks and Ls are the same. Hence, unlike the truth value of logic of probability, the truth value of pCT L∗ formula depends not only on the probabilistic structure defined by the Finite Probabilistic Process but also on the ‘branching structure’ of this process. Therefore there is no direct, meaning preserving translation from pCT L∗ to monadic logic of probability. P s 1 1/2 1 1/2 Q Q Process K 1 Process L Figure 2 In the rest of this section we show that even on the class of models restricted to Finite Probabilistic Processes no pCT L∗ formula is equivalent to the probabilistic formula ∃t Prob≥1 Q(t) where Q is a probabilistic predicate symbol. More precisely, Theorem 11 Let ϕ = ∃t Prob≥1 Q(t) where Q is a probabilistic predicate symbol. There is no pCT L∗ formula ψ such that for every Finite Probabilistic Process M and every state s of M one has M s |= ϕ iff M, s |= ψ. 1/2 s1 1 s2 Q sm 1 s'm 1 s 1/2 t1 1 t2 tn Q 1 s 1 Q s1 sm 1 s'm 1 t'n 1 Figure 3: Km,n and Km . Consider the Finite Probabilistic Processes Km,n and Km for m ≥ 1 and n ≥ 1 as shown in Figure 3. Edges (i, j) are labeled by probabilities P (i, j). Process Km contains only one state (state sm ) labeled by the probabilistic predicate Q, other states have empty labels and process K m,n contains only two states (states sm and tn ) labeled by the probabilistic predicate Q. Let us call Πm the unique infinite path starting in s in Km . Lemma 9 (1) For every pCT L∗ path formula g, there exists an integer r ≥ 1 such that for every m ≥ r, Km , Πm |= g iff Kr , Πr |= g. (2) For every pCT L∗ state formula f , there exists an integer r ≥ 1 such that for every m, n ≥ r, K m,n , s |= f iff Kr,r , s |= f . Proof. The proof is by induction on the complexity of g and f . (1) The key point is for a path formula of the form Xg. We have Km , Πm |= Xg iff m > 0 and Km−1 , Πm−1 |= g. By induction there exists an integer r such that for m − 1 ≥ r, Km−1 , Πm−1 |= g iff Kr , Πr |= g. At last Kr , Πr |= g iff Kr+1 , Πr+1 |= Xg. 18 Thus for m ≥ r + 1, Km , Πm |= Xg iff Kr+1 , Πr+1 |= Xg. (2) Here the key point is for a formula f of the form Prob>q (g). Notice that – for q ≥ 1/2, Km,n , s |= Prob>q (g) iff Km , Πm |= g and Kn , Πn |= g – for q < 1/2, Km,n , s |= Prob>q (g) iff Km , Πm |= g or Kn , Πn |= g. Then we use (1). ¥ Finally we are ready to prove Theorem 11. Proof of Theorem 11. Let us suppose that such a pCT L∗ formula ψ exists. Using Lemma 9, there exists an integer r ≥ 1 such that for every m, n ≥ r, Km,n , s |= ψ iff Kr,r , s |= ψ. That contradicts the fact that Km,n , s |= ϕ iff m = n. ¥ 8 Conclusion Our main result is a description of a fragment of a logic of probability with decidable model-checking. An important and difficult open question is whether one can prove the decidability of model-checking for all values of probabilistic parameters, without exceptions. Another open question is to extend the above results to formulas with conditional probabilities. Below we point to some difficulties which we have to face in order to extend model-checking results. 8.1 Extension to all values of parameters Recall that the central step in the model-checking problem is based on decidability of the following problem Problem A Instance: A probabilistic rational matrix P , its states s1 , s2 and a rational r. Task: Check whether there is n such that (P n )1,2 = r. In section 4 we explained that for given P , s1 and s2 it is easy to decide Problem A for all but finitely many values of A. These “bad”’ values are accumulating points of the sequence {(P n )1,2 }. It is an open question whether Problem A is decidable. It might be the case that there is a reduction between Problem A and the following Skolem problem. Skolem Problem Instance: An integer matrix P . Task: Check whether there is n such that (P n )1,1 = 0. Decidability of the Skolem Problem is open for more than sixty years. It would be interesting to investigate the relationship between Problem A and the Skolem problem. 8.2 Extension to formulas with Conditional Probabilities Let us illustrate here some obstacles that arise in the attempt to extend the model-checking results to the formulas with conditional probabilities. 19 Assume that M is a finite state labeled Markov chain. Moreover assume that (1) it is regular, i.e. its matrix P is such that limn→∞ P n exists and (2) there is exactly one state s1 labeled by a predicate Q1 and there is exactly one state s2 labeled by a predicate Q2 . Let ϕ(t) be the formula Prob>1/2 (Q1 (t) | Q1 (t) ∨ Q2 (t)). In order to check whether ϕ is satisfiable in the structure Ms0 we can do the following. First observe that the probability that Q1 (t) (respectively Q2 (t)) holds at moment n in the structure Ms0 is (P n )0,1 (respectively (P n )0,2 ). (P n )0,1 > 1/2. Therefore, Prob>1/2 (Q1 (t) | Q1 (t) ∨ Q2 (t)) holds at n in Ms0 iff (P n )0,1 +(P n) 0,2 n n Now if limn→∞ (P )0,1 +(P )0,2 > 0, then for all but finitely many r we can check whether Prob>r (Q1 (t) | Q1 (t)∨ Q2 (t)) is satisfiable in Ms0 . However, in the case when limn→∞ (P n )0,1 + (P n )0,2 = 0 we do not know how to verify the satisfiability in Ms0 . It is an open question whether the following conjecture holds: Conjecture Let (S, P ) be a finite Markov chain. There exists a positive natural number d such that the limits (P r+dm )0,1 lim m→∞ (P r+dm )0,1 + (P r+dm )0,2 exist for r = 0, 1, . . . , d − 1. References [AH94] M. Abadi and J. Halpern. Decidability and expressiveness for first-order logic of probability. Information and Computation, 112(1):1–36, 1994. [ASB+ 95] A. Aziz, V. Singhal, F. Balarin, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. It usually works: the temporal logic of stochastic systems. In Computer Aided Verification. Proceeding of CAV’95, pages 155–165. Springer Verlag, 1995. Lect. Notes in Comput. Sci., vol. 939. [Büc60] J.R. Büchi. Weak second-order arithmetic and finite automata. Z. Math. Logik u. Grundlag. Math., (6):66–92, 1960. [CY95] C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42:857–907, 1995. [FH94] R. Fagin and J. Halpern. Reasoning about knowledge and probability. J. of the Assoc. Comput. Mach., 41(2):340–367, 1994. [FHM90] R. Fagin, J.Y. Halpern, and N. Megiddo. A logic for reasoning about probabilities. Information and Computation, 87:1,2:78–128, 1990. [Gan77] F. R. (Feliks Ruvimovich) Gantmakher. The Theory of Matrices. Chelsea Pub. Co., New York, 1977. [GHR94] D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic. Clarendon Press, Oxford, 1994. [Hal90] J. Halpern. An analysis of first-order logics of probability. Artificial Intelligence, 46:311–350, 1990. [Han94] H. A. Hansson. Time and Probability in Formal Design of Distributed Systems. Elsevier, 1994. Series: “Real Time Safety Critical System”, vol. 1. 20 [HJ94] H. A. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6(5):512–535, 1994. [Hod93] W. A. Hodges . Model Theory. Cambridge University Press, Cambridge, 1993. [KS60] J. G. Kemeny and J. L. Snell. Finite Markov Chains. D Van Nostad Co., Inc., Princeton, N.J., 1960. [KSK66] J. G. Kemeny, J. L. Snell, and A.W. Knapp. Denumerable Markov Chains. D Van Nostad Co., Inc., Princeton, N.J., 1966. [Kei85] H. J. Keisler. Probability quantifiers. In J. Barwise and S. S.Feferman, editors, Model Theoretic Logics, pages 509–556. Springer, 1985. [LS82] D. Lehmann and S. Shelah. Reasoning about time and chance. Information and Control, 53(3):165– 198, 1982. [Tho90] W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 131–191. North-Holland, 1990. 21