Proving the decidability of the PDLtimesPDL product logic

STUDIA UNIV. BABES¸–BOLYAI, INFORMATICA, Volume LIV, Number 1, 2009 PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI Abstract. The propositional dynamic logic (PDL) is an adequate tool to write down programs. In a previous article we used PDL to formulate cryptographic protocols as parallel programs. In these protocols at least two agents/individuals exchange messages, so we needed to use product logic to formulate the parallel actions. ´ Agnes Kurucz proved that S5×S5×S5 — which is the simplest triple product logic — is undecidable, hence it follows that PDL×PDL×PDL is undecidable, too. It is easy to show that the PDL logic (without the star operator) is decidable, so it is an interesting problem, that the PDL×PDL product logic is decidable or not. 1. Introduction Authentication protocols emerged from numerous works of computer scientists and their use has become common in the science and study of methods of exchanging keys. They are basically sequences of message exchanges, whose purpose is to assure users that communications do not leak confidential data. Indeed, there is a wide variety of protocols that have been specified and implemented, from protocols with trusted third party, to protocols with public key and, even more generally, hybrid protocols. The one drawback is that many of them have been shown to be flawed, from which one may explain the great deal of attention devoted to the formal verification of security properties of protocols. Examples of protocols can be found in [4]. Received by the editors: December 6, 2008. 2000 Mathematics Subject Classification. 03B45, 94A60. 1998 CR Categories and Descriptors. F.4.1 [Mathematical logic]: model logic – product of propositional dynamic logics; D.4.6 [Security and protection]: Authentication – formal verification of authentication protocols . Key words and phrases. Mathematical logic, Decidability, PDL×PDL product logic, Formal verification. This paper has been presented at the 7th Joint Conference on Mathematics and Computer Science (7th MaCS), Cluj-Napoca, Romania, July 3-6, 2008. 3 4 L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI In the literature, the most popular logic-based formal approach to the analysis of authentication protocols is perhaps the modal BAN calculus introduced by Burrows, Abadi and Needham [3]. From the point of view of computer science, a virtue of BAN is that it allows static characterization of epistemic concepts. In spite of its success in finding flaws or redundancies in some well-known protocols, the effectiveness of BAN as a formal method for the analysis of authentication protocols has been a source of debate, see [9] for details. The problem with the BAN logic is that it explicitly excludes time. On the other hand there is no way to represent actions performed by users. Communication, by its nature, refers to time, and its properties are naturally expressed in terms of actions like sending and receiving messages. When devising a protocol, we usually think of some property that we want the protocol to satisfy. We are mainly interested in the correctness of a protocol with respect to epistemic properties between two users like the arranging of a secret key known only to them. Therefore, our emphasis is on the interplay between knowledge and action. This leads us to consider a language that allows to express notions of knowledge and actions in a straightforward way: the language of modal logic. We can treat protocols as programs, so we used the propositional dynamic logic (PDL) [7] as a starting point. It allows for us to examine properties of the protocol using logic. Protocols are not just sole programs, but a set of programs. Usually two or three programs run parallel when a protocol executed: the program of Alice, of Bob and maybe program of Charlie, if we use the the traditional names of the cryptography. To handle the parallel execution of programs, we developed the product logic PDL×PDL, using the construction of Gabbay and Shehtman [5, 6]. We would use the logic PDL×PDL to examine real protocols, so the decidability of the logic is very important. From [8] we know that S5×S5×S5 — which is the simplest triple product logic — is undecidable, so the examination of PDL×PDL×PDL unnecessary. The original PDL logic is decidable. What is the status of our construction which is between in PDL and PDL×PDL×PDL? We will prove in this article that PDL×PDL is decidable. In the following section we introduce the logic, PDL×PDL, and after we show the method of quasimodels developed by Wolter and Zakharyaschev and explained in [5]. 2. PDL×PDL logic The PDL logic is a logic of actions, so at first we define the set of actions. We have a finite set of atomic actions, its elements are denoted with πi. Two PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC 5 atomic actions are special: the sending and receiving messages. They are denoted with send and rec. For our proofs the structure of messages are indifferent. In our previous papers [1, 2] we discussed the structure of messages in detail. To construct complicated actions we can use the operators of test, sequence and selections, denoted by ?, semicolon and ∪, respectively. α®λ|πk|A?|α;β|α∪β|send(m)|rec(m) We can define the formulae based on the set of atomic formulae, by using the usual logical connectives and the modalities constructed from a pair of actions: A®pk| ¬A|A∨B| hα1kα2iA For the semantics, we use a variant of the Kripke model. We have two agents, so the global state is build up from local states. The model Mis a (W1, W2, r, R, V ) tuple where W1and W2are the set of local states (possible worlds), rand Ris a family of relations on Wi(ri,Ri⊆Wi×Wi), and V is a valuation on W1×W2(V(pj)⊆W1×W2). Given a model Mwe define the relation Rαkβand the (s, t, c)|= MAtruth-relation by a parallel induction for any states s, s0∈W1,t, t0∈W2, actions α,βand formula Aas follows: •(s, t, c)Rλkλ(s0, t0, c0) iff s=s0, t =t0, c =c0; •(s, t, c)Rπikλ(s0, t0, c0) iff sris0, t =t0, c =c0; •(s, t, c)Rλkπi(s0, t0, c0) iff s=s0, tRit0, c =c0; •(s, t, c)RA?kλ(s0, t0, c0) iff s=s0, t =t0, c =c0,(s, t, c)|= MA; •(s, t, c)RλkA?(s0, t0, c0) iff s=s0, t =t0, c =c0,(s, t, c)|= MA; •(s, t, c)Rsend(m)kλ(s0, t0, c0) iff s=s0, t =t0, and if c= (c1, c2), then c0= (c1, c2? m); •(s, t, c)Rλksend(m)(s0, t0, c0) iff s=s0, t =t0, and if c= (c1, c2), then c0= (c1? m, c2); •(s, t, c)Rrec(m)kλ(s0, t0, c0) iff s=s0, t =t0, and if c0= (c1, c2), then c= (m?c1, c2); •(s, t, c)Rλkrec(m)(s0, t0, c0) iff s=s0, t =t0, and if c0= (c1, c2), then c= (c1, m ? c2); •Rϕ;αkψ;β®(Rϕkλ◦Rαkψ;β)∪(Rλkψ◦Rϕ;αkβ) where ϕiand ψjare atomic action, test, send or receive actions; •Rα(α1∪α2)kβ®Rα(α1)kβ∪Rα(α2)kβ; •Rαkβ(β1∪β2)®Rαkβ(β1)∪Rαkβ(β2). •(s, t, c)|= Mpiiff (s, t)∈V(pi) •(s, t, c)|= M¬Aiff (s, t, c)6|= MA. •(s, t, c)|= MA∨Biff (s, t, c)|= MAor (s, t, c)|= MB. 6 L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI •(s, t, c)|= MhαkβiA, if there exists a triple (s0, t0, c0) such that (s, t, c) Rα1kα2(s0, t0, c0) and (s0, t0, c0)|= MA We say that formula Ais satisfiable in model Mif there is exists s∈W1and t∈W2such that (s, t, (ε, ε)) |= MA; and we say that formula Ais valid in model Mif for all s∈W1and t∈W2, (s, t, (ε, ε)) |= MA. 3. Quasimodel To prove the decidability of the PDL×PDL logic, we follow the method described in [5]. At first we need the concept of the subformula. The standard definition is not suitable for us, so we use a variant. The Fischer-Ladner closure of ϕ(flc(ϕ)) defined as •if ψ∨χ∈flc(ϕ) then ψ∈flc(ϕ), χ∈flc(ϕ); •if ¬ψ∈flc(ϕ) then ψ∈flc(ϕ); •if hαkβiψ∈flc(ϕ) then ψ∈flc(ϕ); •if hα(α1∪α2)kβiψ∈flc(ϕ) then hα(α1)kβiψ∈flc(ϕ), hα(α2)k βiψ∈flc(ϕ); •if hαkβ(β1∪β2)iψ∈flc(ϕ) then hαkβ(β1)iψ∈flc(ϕ), hαkβ(β2)iψ∈ flc(ϕ); •if hπ;αkβiψ∈flc(ϕ) then hπkλihαkβiψ∈flc(ϕ), where πis an atomic action or a test; •if hαkπ;βiψ∈flc(ϕ) then hλkπihαkβiψ∈flc(ϕ), where πis an atomic action or a test; •if hψ?kλiχ∈flc(ϕ) or hλkψ?iχ∈flc(ϕ) then ψ∈flc(ϕ), and χ∈flc(ϕ). Type tfor ϕis a Boolean saturated subset tof flc(ϕ), satisfying the following conditions: (t1)hλkλiψ∈tiff ψ∈tfor all hλkλiψ∈flc(ϕ); (t2)hπ;αkλiψ∈tiff hπkλihαkλiψ∈tfor all hπ;αkλiψ∈flc(ϕ); (t3)hλkπ;βiψ∈tiff hλkπihλkβiψ∈tfor all hλkπ;βiψ∈flc(ϕ); (t4)hπ;αkπ0;βiψ∈tiff eitherhπkλihαkπ0;βiψ∈tor hλkπ0ihπ;αkβiψ∈ tfor all hπ;αkπ0;βiψ∈flc(ϕ); (t5)hα(α1∪α2)kβiψ∈tiff eitherhα(α1)kβiψ∈tor hα(α2)kβiψ∈tfor all hα(α1∪α2)kβiψ∈flc(ϕ); (t6)hαkβ(β1∪β2)iψ∈tiff eitherhαkβ(β1)iψ∈tor hαkβ(β2)iψ∈tfor all hαkβ(β1∪β2)iψ∈flc(ϕ); (t7)hψ?kλiχ∈tiff ψ∈tand χ∈tfor all hψ?kλiχ∈flc(ϕ); (t8)hλkψ?iχ∈tiff ψ∈tand χ∈tfor all hλkψ?iχ∈flc(ϕ). Modal depth of a formula ϕ(md(ϕ))is defined as usual: PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC 7 •md(pi) = md(>) = 0; •md(¬ϕ) = md(ϕ); •md(ϕ∨ψ) = max(md(ϕ), md(ψ)); •md([αkβ]ϕ) = md(hαkβiϕ); •md(hλkλiϕ) = md(ϕ); •md(hα(α1∪α2)kβiϕ) = max(md(hα(α1)kβiϕ), md(hα(α2)kβiϕ)); •md(hαkβ(β1∪β2)iϕ) = max(md(hαkβ(β1)iϕ), md(hαkβ(β2)iϕ)); •md(hπ;αkβiϕ) = md(hαkπ;βiϕ) = 1 + md(hαkβiϕ). An n-frame F= (W, R1, . . . , Rn) is called rooted, if there is a w0∈Wsuch that W={w∈W|w0R∗w}, where R=S1≤j≤nRj. Such a w0is called a root of F. A rooted frame F= (W, R1, . . . , Rn) is said to be a tree if all the Rjare pairwise disjoint and for every x∈W, the set Wx={y∈W|yR∗x}is finite and linearly ordered by the reflexive and transitive closure R∗of the relation R(its restriction to Wx, to be more precise). Fis called intransitive if for any Rj,Rk(1 ≤j, k ≤n) we have ∀x, y, z ∈W(xRjy∧yRkz→ ¬xRkz∧ ¬xRjz). A path of length lfrom xto yin Fis a sequence (x0, . . . , xl) such that x0=x, xl=yand xkRjxk+1 for each k < l and some j, 1 ≤j≤n. The length of the path from the root of Fto xis called the co-depth of x. The depth of Fis the maximum of co-depth of x(x∈W), if this maximum exists. By the depth of x in Fwe understand the depth of the subtree of Fwith root x. The Quasistate candidate for ϕis a pair ((T, R1, . . . , Rk), t), where (T, R1, . . . , Rk) is a finite intransitive tree of depth md(ϕ), and tis a labeling function associating with each x∈Ta type t(x) for ϕ. ((T, R1, . . . , Rk), t) is a quasistate for ϕif (qm1) for all x∈Tand hλkπiiψ∈flc(ϕ): hλkπiiψ∈t(x) iff there exists a y∈Tsuch that xRiyand ψ∈t(y). (qm1’) for all x0,x1,x2∈Tsuch that x0Rix1,x0Rix1, and x16=x2the structures ((Tx1, Rx1 1, . . . , Rx1 k), tx1) and ((Tx2, Rx2 1, . . . , Rx2 k), tx2) are not isomorphic. (Two quasistate candidates ((T, <1, . . . , <n), t) and ((T0, <0 1, . . . , <0 n), t0) are called isomorphic if there is an isomorphism fbetween the trees (T, <1, . . . , <n) and (T0, <0 1, . . . , <0 n) such that t(x) = t0(f(x)), for all x∈T.) Abasic structure for ϕof depth mis a pair (F, q), such that F= (W, r1, . . . , rk) and qis a function associating with each world w∈Wand each message c= (c1, c2) a quasistate q(w, c) = ((Tc w, Rc w,1, . . . , Rc w,k), tc w) for ϕsuch that the depth of each (Tc w, Rc w,i) is m. Let (F, q) be a basic structure for ϕof depth mand let l≤m. An l-run through (F, q) is a function ρgiving for each w∈Wand the list of messages ca point ρ(w, c)∈Tc wof co-depth l. Given a set Rof runs we denote by Rlthe set of all l-runs from R. A run ρis called 8 L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI coherent, if for all lists of messages c, for all possible worlds w∈Wand for all formulae the following conditions are satisfied: • hπikλiψ∈flc(ϕ): if there exists a world v∈Wsuch that wrivand ψ∈tc v(ρ(v, c)) then hπikλiψ∈tc w(ρ(w, c)); • hsend(m)kλiψ∈flc(ϕ): if c0= (c1, c2? m) where c= (c1, c2) and ψ∈tc0 w(ρ(w, c0)) then hsend(m)kλiψ∈tc w(ρ(w, c)); • hλksend(m)iψ∈flc(ϕ): if c0= (c1? m, c2) where c= (c1, c2) and ψ∈tc0 w(ρ(w, c0)) then hλksend(m)iψ∈tc w(ρ(w, c)); • hrec(m)kλiψ∈flc(ϕ): if c0= (c1, c2) where c= (m?c1, c2) and ψ∈tc0 w(ρ(w, c0)) then hrec(m)kλiψ∈tc w(ρ(w, c)); • hλkrec(m)iψ∈flc(ϕ): if c0= (c1, c2) where c= (c1, m ? c2) and ψ∈tc0 w(ρ(w, c0)) then hλkrec(m)iψ∈tc w(ρ(w, c)). In the previous definition the sign ?denotes the concatenation of messages. A run ρis called w-saturated for w∈W, if for all lists of messages cand for all formulae the following conditions are satisfied: • hπikλiψ∈flc(ϕ): if hπikλiψ∈tc w(ρ(w, c)) then there exists a world v∈Wsuch that wrivand ψ∈tc v(ρ(v, c)); • hsend(m)kλiψ∈flc(ϕ): if hsend(m)kλiψ∈tc w(ρ(w, c)) then ψ∈ tc0 w(ρ(w, c0)) where if c= (c1, c2) then c0= (c1, c2? m); • hλksend(m)iψ∈flc(ϕ): if hλksend(m)iψ∈tc w(ρ(w, c)) then ψ∈ tc0 w(ρ(w, c0)) where if c= (c1, c2) then c0= (c1? m, c2); • hrec(m)kλiψ∈flc(ϕ): if hrec(m)kλiψ∈tc w(ρ(w, c)) then ψ∈ tc0 w(ρ(w, c0)) where if c= (m?c1, c2) then c0= (c1, c2); • hλkrec(m)iψ∈flc(ϕ): if hλkrec(m)iψ∈tc w(ρ(w, c)) then ψ∈ tc0 w(ρ(w, c0)) where if c= (c1, m ? c2) then c0= (c1, c2). A run is saturted, if it is w-saturated for all w∈W.Q= (F, q, R,C) is aPDL×PDL-quasimodel for ϕif (F, q) is a basic structure for ϕof depth m≤md(ϕ) such that (qm2) there exists a world w0∈Wand ϕ∈t(ε,ε) w0(x0), where x0is the root of ³T(ε,ε) w0, R(ε,ε) w0,1, . . . , R(ε,ε) w0,k´. Ris a set of coherent and saturated runs through (F, q) and Cis a set of binary relation on Rsatisfying the following conditions: (qm3) for all ρ, ρ0∈ R, if ρCiρ0then ρ(w, c)Rc w,iρ0(w, c) for all w∈Wand lists of messages c. (qm4) R06=εand for all l < m,ρ∈ Rl,w∈W, for all lists of messages c, x∈Tc w, for all 1 ≤i≤k, if ρ(w, c)Rc w,ixthen there is ρ0∈ Rl+1 such that ρ0(w, c) = xand ρCiρ0. PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC 9 Lemma 1. An ML2formula ϕsatisfiable in a product frame F × G iff there is a PDL×PDL-quasimodel for ϕbased on F. Proof. Let (F, q, R,C) be a PDL×PDL-quasimodel for ϕbased on F, where F= (W, r1, . . . , rk). Take the product frame F × (R,C), and define a valuation Vin it as follows: V(pi) = {(w, ρ, c)|p∈tc w(ρ(w, c))}for every propositional variable pi. Let Mbe (F × (R,C),V). By induction on the construction of ψ∈flc(ϕ) we need to show that for every (w, ρ, c)∈ M we have (w, ρ, c)|= Mψiff ψ∈tc w(ρ(w, c)). •For variables this follows from the definition. •For Booleans, types are Boolean saturated sets. •(w, ρ, c)|= Mhπikλiψ(based on the definition of the semantics) iff there exists a world w0∈Wsuch that wriw0and (w0, ρ, c)|= Mψ. Then by induction hypothesis (IH) ψ∈tc w0(ρ(w0, c)). ρis saturated and coherent, so the previous holds iff hπikλiψ∈tc w(ρ(w, c)). •(w, ρ, c)|= Mhλkπiiψ(based on the definition of the semantics) iff there exists a run ρ0∈ R such that ρCiρ0and (w, ρ0, c)|= Mψ. Then by IH ψ∈tc w(ρ0(w, c)). According to (qm3), from ρCiρ0we get ρ(w, c)Rc w,iρ0(w, c). Finally based on (qm1) we get that hλkπiiψ∈ tc w(ρ(w, c)). In other direction let assume, that hλkπiiψ∈tc w(ρ(w, c)) Then by (qm1) there exists a x∈Tc wsuch that ρ(w, c)Rixand ψ∈tc w(x). According to (qm4) there exists ρ0∈ R such that ρCiρ0and ψ∈ tc w(ρ0(w, c)). By IH we get (w, ρ0, c)|= Mψand finally according to the definition of the semantics (w, ρ, c)|= Mhλkπiiψ. •(w, ρ, c)|= Mhsend(m)kλiψiff (w, ρ, c0)|= Mψwhere if c= (c1, c2) then c0= (c1, c2? m) (by def.). Then by IH ψ∈tc0 w(ρ(w, c0)). ρis saturated and coherent, so the previous holds iff hsend(m)kλiψ∈tc w(ρ(w, c)). •(w, ρ, c)| = Mhλksend(m)iψiff (w, ρ, c0)| = Mψwhere if c= (c1, c2) then c0= (c1? m, c2) (by def.). Then by IH ψ∈tc0 w(ρ(w, c0)). ρis saturated and coherent, so the previous holds iff hλksend(m)iψ∈tc w(ρ(w, c)). •(w, ρ, c)|= Mhrec(m)kλiψiff (w, ρ, c0)|= Mψwhere if c0= (c1, c2) then c= (m ? c1, c2) (by def.). Then by IH ψ∈tc0 w(ρ(w, c0)). ρis saturated and coherent, so the previous holds iff hrec(m)kλiψ∈tc w(ρ(w, c)). •(w, ρ, c)|= Mhλkrec(m)iψiff (w, ρ, c0)|= Mψwhere if c0= (c1, c2) then c= (c1, m ? c2) (by def.). Then by IH ψ∈tc0 w(ρ(w, c0)). ρis saturated and coherent, so the previous holds iff hλkrec(m)iψ∈tc w(ρ(w, c)). 10 L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI •(w, ρ, c)|= Mhψ?kλiχiff (w, ρ, c)|= Mψand (w, ρ, c)|= Mχ. By IH this is true iff ψ∈tc w(ρ(w, c)) and χ∈tc w(ρ(w, c)). But according to (t7) this is true iff hψ?kλiχ∈tc w(ρ(w, c)) •(w, ρ, c)|= Mhλkψ?iχiff (w, ρ, c)|= Mψand (w, ρ, c)|= Mχ. By IH this is true iff ψ∈tc w(ρ(w, c)) and χ∈tc w(ρ(w, c)). But according to (t8) this is true iff hλkψ?iχ∈tc w(ρ(w, c)) •(w, ρ, c)|= Mhα(α1∪α2)kβiψiff (w, ρ, c)|= Mhα(α1)kβiψor (w, ρ, c)|= Mhα(α2)kβiψ(by def.). By IH this is true iff hα(α1)kβiψ∈ tc w(ρ(w, c)) or hα(α2)kβiψ∈tc wρ(w, c)). But according to (t5) this is true iff hα(α1∪α2)kβiψ∈tc w(ρ(w, c)) •(w, ρ, c)|= Mhαkβ(β1∪β2)iψiff (w, ρ, c)|= Mhαkβ(β1)iψor (w, ρ, c)|= Mhαkβ(β2)iψ(by def.). By IH this is true iff hαkβ(β1)iψ∈tc w(ρ(w, c)) or hαkβ(β2)iψ∈tc w(ρ(w, c)). But according to (t6) this is true iff hαkβ(β1∪β2)iψ∈tc w(ρ(w, c)) •(w, ρ, c)|= Mhπi;αkλiψiff there exitst a world w0such that wriw0and (w0, ρ, c)|= Mhαkλiψ(by def.). Then by IH hαkλiψ∈tc w0(ρ(w0, c)). ρ is coherent and saturated, so hπikλihαkλiψ∈tc w(ρ(w, c)). According to (t2) this is true iff hπi;αkλiψ∈tc w(ρ(w, c)). •(w, ρ, c)|= Mhλkπi;βiψiff there exitst a run ρ0∈ R such that ρCiρ0 and (w, ρ0, c)|= Mhλkβiψ(by def.). Then by IH hλkβiψ∈tc w(ρ0(w, c)). According to (qm3) ρ(w, c)Rc w,iρ0(w, c), and by (qm1) hλkπiihλkβiψ∈ tc w(ρ(w, c)). According to (t3) this is true iff hλkπi;βiψ∈tc w(ρ(w, c)). •(w, ρ, c)|= Mhπi;αkπj;βiψiff (w, ρ, c)|= Mhπikλihαkπj;βiψor (w, ρ, c)|= Mhλkπjihπi;αkβiψ. Based on previous points of this proof we get that hπikλihαkπj;βiψ∈tc w(ρ(w, c)) or hλkπjihπi;αk βiψ∈tc w(ρ(w, c)). According to (t4) this is true iff hπi;αkπj;βiψ∈ tc w(ρ(w, c)). Therefore by (qm2), ϕis satisfied in M. For the other direction, suppose that ϕis satisfied in a model Mbased on the product F × G of frames F= (W, r1, . . . , rk) and G= (∆, R1, . . . , Rk) By proposition 1.7 and 3.9 in [5] we may assume, that Gis an intransitive tree of depth m≤md(ϕ) and (w0, x0,(ε, ε)) |= Mϕfor some w0∈Wwith x0being the root of G. With every triple (w, x, c) where w∈W,x∈∆ and cis a lists of messages we associate the type t(w, x, c) = {ψ∈flc(ϕ)|(w, x, c)|= Mψ}. Fix wand cand define a binary relation ∼c won ∆ as follows: •if x,y∈∆ of depth 0 then x∼c wyiff t(w, x, c) = t(w, y, c). •if x,y∈∆ of depth l < md(ϕ) then x∼c wyiff t(w, x, c) = t(w, y, c) and for all z∈∆ and for all 1 ≤i≤k PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC 11 –if xRizthen there exists a z0∈∆ such that yRiz0and z∼c wz0 –if yRizthen there exists a z0∈∆ such that xRiz0and z∼c wz0. Clearly ∼c wis an equivalence relation on ∆. Denote by [x]c wthe ∼c w-equivalence class of x, and put ∆c w®{[x]c w|x∈∆},sc w([x]c w)®t(w, x, c) and [x]c wRc w,i[y]c wif there exists a y0∈∆c wsuch that xRiy0. Then by the definition of ∼c w,rc wis well-defined, and the structure ((∆c w, rc w), sc w) clearly satisfies (qm1’). The map x7→ [x]c wis a p-morphism from (∆, r2) to (∆c w, rc w), so it also satisfies (qm1). However (∆c w, rc w) is not necessarily a tree. The tree (Tc w, <c w) we need can be obtained from this structure: Tc w=n([x0]c w, . . . , [xl]c w)¯¯¯l≤m, [x0]c wrc wi1[x1]c w· · · [xl−1]c wrc w,il−1[xl]c wo If u,v∈Tc wthen u <c w,i viff u= ([x0]c w, . . . , [xl]c w), v= ([x0]c w, . . . , [xl]c w,[xl+1]c w) and xlRixl+1.tc w([x0]c w,...,[xl]c w)®t(w, x, c). It is easy to show that ((Tc w, <c w), tc w) is a quasistate for ϕfor any w∈Wand messages c. Moreover ϕ∈t(ε,ε) w0³[x0](ε,ε) w0´. So by taking q(w, c)®((Tc w, <c w,1, . . . , <c w,k), tc w) for each w∈Wand each message cwe obtain a basic structure (F, q) for ϕ statisfying (qm2). We need to define runs trough (F, q). To do this for each l≤mand each sequence (x0, . . . , xl) in ∆ such that x0Ri1· · · Rilxl, take the map ρ: (w, c)7→ ([x0]c w, . . . [x0]c w). It is easy to check that ρis a coherent and a saturated l-run. Let Rbe the set of all such runs. For ρ,ρ0∈ R let ρCiρ0iff ρ(w, c)<c wρ0(w, c) for all w∈Wand for all messages c. Then (qm3) holds by definition. It remains to prove (qm4). Let ρ∈ Rl,v∈W, cany messages and z∈Tc vbe such that ρ(v, c)<c vz. We have to show that there is ρ0∈ Rl+1 such that ρCiρ0, and ρ0(v, c) = z. Since ρ(v, c)<c v,i z, we have ρ(v, c) = ([x0]c v, . . . , [xl]c v) and z= ([x0]c v, . . . , [xl]c v,[xl+1]c v) for some x1, . . . , xl, xl+1 with x0Rc j1x1· · · Rc jlxland [xl]c vrc v,i[xl+1]c v. By the definition of Rc v,i there is y∈[xl+1]c vsuch that xlRiy. But then the map ρ0: (w, c)7→ ([x0]c w, . . . , [xl]c w,[y]c w) is in R. Thus (F, q, R,C) is a quasimodel for ϕ. 4. Blocks A block for ϕwith root wis quadruple B= (F, q, R,C) such that • F = (∆, <) is a tree of depth less equal 1 with root w •(F, q) is a basic structure for ϕof depth mfor some m < md(ϕ) • R is a set of coherent and saturated runs through (F, q) •Cis a set of binary relation on Rsatisfying (qm3) and (qm4) A set Sof blocks for ϕis called satisfying, if •all blocks in Sare of the same depth mfor some m < md(ϕ)