Proving the decidability of the PDLtimesPDL product logic

STUDIA UNIV. BABES¸–BOLYAI, INFORMATICA, Volume LIV, Numbe 1, 2009 PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI Abs ac . The p oposi ional dynamic logic (PDL) is an adequa e ool o w i e down p og ams. In a p e ious a icle we used PDL o o mula e c yp- og aphic p o ocols as pa allel p og ams. In hese p o ocols a leas wo agen s/indi iduals exchange messages, so we needed o use p oduc logic o o mula e he pa allel ac ions. ´ Agnes Ku ucz p o ed ha S5×S5×S5 — which is he simples iple p oduc logic — is undecidable, hence i ol- lows ha PDL×PDL×PDL is undecidable, oo. I is easy o show ha he PDL logic (wi hou he s a ope a o ) is decidable, so i is an in e es ing p oblem, ha he PDL×PDL p oduc logic is decidable o no . 1. In oduc ion Au hen ica ion p o ocols eme ged om nume ous wo ks o compu e sci- en is s and hei use has become common in he science and s udy o me hods o exchanging keys. They a e basically sequences o message exchanges, whose pu pose is o assu e use s ha communica ions do no leak con iden ial da a. Indeed, he e is a wide a ie y o p o ocols ha ha e been speci ied and imple- men ed, om p o ocols wi h us ed hi d pa y, o p o ocols wi h public key and, e en mo e gene ally, hyb id p o ocols. The one d awback is ha many o hem ha e been shown o be lawed, om which one may explain he g ea deal o a en ion de o ed o he o mal e i ica ion o secu i y p ope ies o p o ocols. Examples o p o ocols can be ound in [4]. Recei ed by he edi o s: Decembe 6, 2008. 2000 Ma hema ics Subjec Classi ica ion. 03B45, 94A60. 1998 CR Ca ego ies and Desc ip o s. F.4.1 [Ma hema ical logic]: model logic – p o- duc o p oposi ional dynamic logics; D.4.6 [Secu i y and p o ec ion]: Au hen ica ion – o mal e i ica ion o au hen ica ion p o ocols . Key wo ds and ph ases. Ma hema ical logic, Decidabili y, PDL×PDL p oduc logic, Fo - mal e i ica ion. This pape has been p esen ed a he 7 h Join Con e ence on Ma hema ics and Compu e Science (7 h MaCS), Cluj-Napoca, Romania, July 3-6, 2008. 3 4 L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI In he li e a u e, he mos popula logic-based o mal app oach o he analysis o au hen ica ion p o ocols is pe haps he modal BAN calculus in- oduced by Bu ows, Abadi and Needham [3]. F om he poin o iew o compu e science, a i ue o BAN is ha i allows s a ic cha ac e iza ion o epis emic concep s. In spi e o i s success in inding laws o edundancies in some well-known p o ocols, he e ec i eness o BAN as a o mal me hod o he analysis o au hen ica ion p o ocols has been a sou ce o deba e, see [9] o de ails. The p oblem wi h he BAN logic is ha i explici ly excludes ime. On he o he hand he e is no way o ep esen ac ions pe o med by use s. Communica ion, by i s na u e, e e s o ime, and i s p ope ies a e na u ally exp essed in e ms o ac ions like sending and ecei ing messages. When de ising a p o ocol, we usually hink o some p ope y ha we wan he p o ocol o sa is y. We a e mainly in e es ed in he co ec ness o a p o ocol wi h espec o epis emic p ope ies be ween wo use s like he a anging o a sec e key known only o hem. The e o e, ou emphasis is on he in e play be ween knowledge and ac ion. This leads us o conside a language ha al- lows o exp ess no ions o knowledge and ac ions in a s aigh o wa d way: he language o modal logic. We can ea p o ocols as p og ams, so we used he p oposi ional dynamic logic (PDL) [7] as a s a ing poin . I allows o us o examine p ope ies o he p o ocol using logic. P o ocols a e no jus sole p og ams, bu a se o p og ams. Usually wo o h ee p og ams un pa allel when a p o ocol execu ed: he p og am o Alice, o Bob and maybe p og am o Cha lie, i we use he he adi ional names o he c yp og aphy. To handle he pa allel execu ion o p og ams, we de eloped he p oduc logic PDL×PDL, using he cons uc ion o Gabbay and Sheh man [5, 6]. We would use he logic PDL×PDL o examine eal p o ocols, so he de- cidabili y o he logic is e y impo an . F om [8] we know ha S5×S5×S5 — which is he simples iple p oduc logic — is undecidable, so he exam- ina ion o PDL×PDL×PDL unnecessa y. The o iginal PDL logic is decid- able. Wha is he s a us o ou cons uc ion which is be ween in PDL and PDL×PDL×PDL? We will p o e in his a icle ha PDL×PDL is decidable. In he ollowing sec ion we in oduce he logic, PDL×PDL, and a e we show he me hod o quasimodels de eloped by Wol e and Zakha yasche and explained in [5]. 2. PDL×PDL logic The PDL logic is a logic o ac ions, so a i s we de ine he se o ac ions. We ha e a ini e se o a omic ac ions, i s elemen s a e deno ed wi h πi. Two PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC 5 a omic ac ions a e special: he sending and ecei ing messages. They a e deno ed wi h send and ec. Fo ou p oo s he s uc u e o messages a e indi e en . In ou p e ious pape s [1, 2] we discussed he s uc u e o messages in de ail. To cons uc complica ed ac ions we can use he ope a o s o es , sequence and selec ions, deno ed by ?, semicolon and ∪, espec i ely. α®λ|πk|A?|α;β|α∪β|send(m)| ec(m) We can de ine he o mulae based on he se o a omic o mulae, by using he usual logical connec i es and he modali ies cons uc ed om a pai o ac ions: A®pk| ¬A|A∨B| hα1kα2iA Fo he seman ics, we use a a ian o he K ipke model. We ha e wo agen s, so he global s a e is build up om local s a es. The model Mis a (W1, W2, , R, V ) uple whe e W1and W2a e he se o local s a es (possible wo lds), and Ris a amily o ela ions on Wi( i,Ri⊆Wi×Wi), and V is a alua ion on W1×W2(V(pj)⊆W1×W2). Gi en a model Mwe de ine he ela ion Rαkβand he (s, , c)|= MA u h- ela ion by a pa allel induc ion o any s a es s, s0∈W1, , 0∈W2, ac ions α,βand o mula Aas ollows: •(s, , c)Rλkλ(s0, 0, c0) i s=s0, = 0, c =c0; •(s, , c)Rπikλ(s0, 0, c0) i s is0, = 0, c =c0; •(s, , c)Rλkπi(s0, 0, c0) i s=s0, Ri 0, c =c0; •(s, , c)RA?kλ(s0, 0, c0) i s=s0, = 0, c =c0,(s, , c)|= MA; •(s, , c)RλkA?(s0, 0, c0) i s=s0, = 0, c =c0,(s, , c)|= MA; •(s, , c)Rsend(m)kλ(s0, 0, c0) i s=s0, = 0, and i c= (c1, c2), hen c0= (c1, c2? m); •(s, , c)Rλksend(m)(s0, 0, c0) i s=s0, = 0, and i c= (c1, c2), hen c0= (c1? m, c2); •(s, , c)R ec(m)kλ(s0, 0, c0) i s=s0, = 0, and i c0= (c1, c2), hen c= (m?c1, c2); •(s, , c)Rλk ec(m)(s0, 0, c0) i s=s0, = 0, and i c0= (c1, c2), hen c= (c1, m ? c2); •Rϕ;αkψ;β®(Rϕkλ◦Rαkψ;β)∪(Rλkψ◦Rϕ;αkβ) whe e ϕiand ψja e a omic ac ion, es , send o ecei e ac ions; •Rα(α1∪α2)kβ®Rα(α1)kβ∪Rα(α2)kβ; •Rαkβ(β1∪β2)®Rαkβ(β1)∪Rαkβ(β2). •(s, , c)|= Mpii (s, )∈V(pi) •(s, , c)|= M¬Ai (s, , c)6|= MA. •(s, , c)|= MA∨Bi (s, , c)|= MAo (s, , c)|= MB. 6 L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI •(s, , c)|= MhαkβiA, i he e exis s a iple (s0, 0, c0) such ha (s, , c) Rα1kα2(s0, 0, c0) and (s0, 0, c0)|= MA We say ha o mula Ais sa is iable in model Mi he e is exis s s∈W1and ∈W2such ha (s, , (ε, ε)) |= MA; and we say ha o mula Ais alid in model Mi o all s∈W1and ∈W2, (s, , (ε, ε)) |= MA. 3. Quasimodel To p o e he decidabili y o he PDL×PDL logic, we ollow he me hod desc ibed in [5]. A i s we need he concep o he sub o mula. The s anda d de ini ion is no sui able o us, so we use a a ian . The Fische -Ladne closu e o ϕ( lc(ϕ)) de ined as •i ψ∨χ∈ lc(ϕ) hen ψ∈ lc(ϕ), χ∈ lc(ϕ); •i ¬ψ∈ lc(ϕ) hen ψ∈ lc(ϕ); •i hαkβiψ∈ lc(ϕ) hen ψ∈ lc(ϕ); •i hα(α1∪α2)kβiψ∈ lc(ϕ) hen hα(α1)kβiψ∈ lc(ϕ), hα(α2)k βiψ∈ lc(ϕ); •i hαkβ(β1∪β2)iψ∈ lc(ϕ) hen hαkβ(β1)iψ∈ lc(ϕ), hαkβ(β2)iψ∈ lc(ϕ); •i hπ;αkβiψ∈ lc(ϕ) hen hπkλihαkβiψ∈ lc(ϕ), whe e πis an a omic ac ion o a es ; •i hαkπ;βiψ∈ lc(ϕ) hen hλkπihαkβiψ∈ lc(ϕ), whe e πis an a omic ac ion o a es ; •i hψ?kλiχ∈ lc(ϕ) o hλkψ?iχ∈ lc(ϕ) hen ψ∈ lc(ϕ), and χ∈ lc(ϕ). Type o ϕis a Boolean sa u a ed subse o lc(ϕ), sa is ying he ollowing condi ions: ( 1)hλkλiψ∈ i ψ∈ o all hλkλiψ∈ lc(ϕ); ( 2)hπ;αkλiψ∈ i hπkλihαkλiψ∈ o all hπ;αkλiψ∈ lc(ϕ); ( 3)hλkπ;βiψ∈ i hλkπihλkβiψ∈ o all hλkπ;βiψ∈ lc(ϕ); ( 4)hπ;αkπ0;βiψ∈ i ei he hπkλihαkπ0;βiψ∈ o hλkπ0ihπ;αkβiψ∈ o all hπ;αkπ0;βiψ∈ lc(ϕ); ( 5)hα(α1∪α2)kβiψ∈ i ei he hα(α1)kβiψ∈ o hα(α2)kβiψ∈ o all hα(α1∪α2)kβiψ∈ lc(ϕ); ( 6)hαkβ(β1∪β2)iψ∈ i ei he hαkβ(β1)iψ∈ o hαkβ(β2)iψ∈ o all hαkβ(β1∪β2)iψ∈ lc(ϕ); ( 7)hψ?kλiχ∈ i ψ∈ and χ∈ o all hψ?kλiχ∈ lc(ϕ); ( 8)hλkψ?iχ∈ i ψ∈ and χ∈ o all hλkψ?iχ∈ lc(ϕ). Modal dep h o a o mula ϕ(md(ϕ))is de ined 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- ame F= (W, R1, . . . , Rn) is called oo ed, i he e is a w0∈Wsuch ha W={w∈W|w0R∗w}, whe e R=S1≤j≤nRj. Such a w0is called a oo o F. A oo ed ame F= (W, R1, . . . , Rn) is said o be a ee i all he Rja e pai wise disjoin and o e e y x∈W, he se Wx={y∈W|yR∗x}is ini e and linea ly o de ed by he e lexi e and ansi i e closu e R∗o he ela ion R(i s es ic ion o Wx, o be mo e p ecise). Fis called in ansi i e i o any Rj,Rk(1 ≤j, k ≤n) we ha e ∀x, y, z ∈W(xRjy∧yRkz→ ¬xRkz∧ ¬xRjz). A pa h o leng h l om x o yin Fis a sequence (x0, . . . , xl) such ha x0=x, xl=yand xkRjxk+1 o each k < l and some j, 1 ≤j≤n. The leng h o he pa h om he oo o F o xis called he co-dep h o x. The dep h o Fis he maximum o co-dep h o x(x∈W), i his maximum exis s. By he dep h o x in Fwe unde s and he dep h o he sub ee o Fwi h oo x. The Quasis a e candida e o ϕis a pai ((T, R1, . . . , Rk), ), whe e (T, R1, . . . , Rk) is a ini e in ansi i e ee o dep h md(ϕ), and is a labeling unc ion associa ing wi h each x∈Ta ype (x) o ϕ. ((T, R1, . . . , Rk), ) is a quasis a e o ϕi (qm1) o all x∈Tand hλkπiiψ∈ lc(ϕ): hλkπiiψ∈ (x) i he e exis s a y∈Tsuch ha xRiyand ψ∈ (y). (qm1’) o all x0,x1,x2∈Tsuch ha x0Rix1,x0Rix1, and x16=x2 he s uc u es ((Tx1, Rx1 1, . . . , Rx1 k), x1) and ((Tx2, Rx2 1, . . . , Rx2 k), x2) a e no isomo phic. (Two quasis a e candida es ((T, <1, . . . , <n), ) and ((T0, <0 1, . . . , <0 n), 0) a e called isomo phic i he e is an isomo phism be ween he ees (T, <1, . . . , <n) and (T0, <0 1, . . . , <0 n) such ha (x) = 0( (x)), o all x∈T.) Abasic s uc u e o ϕo dep h mis a pai (F, q), such ha F= (W, 1, . . . , k) and qis a unc ion associa ing wi h each wo ld w∈Wand each message c= (c1, c2) a quasis a e q(w, c) = ((Tc w, Rc w,1, . . . , Rc w,k), c w) o ϕsuch ha he dep h o each (Tc w, Rc w,i) is m. Le (F, q) be a basic s uc u e o ϕo dep h mand le l≤m. An l- un h ough (F, q) is a unc ion ρgi ing o each w∈Wand he lis o messages ca poin ρ(w, c)∈Tc wo co-dep h l. Gi en a se Ro uns we deno e by Rl he se o all l- uns om R. A un ρis called 8 L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI cohe en , i o all lis s o messages c, o all possible wo lds w∈Wand o all o mulae he ollowing condi ions a e sa is ied: • hπikλiψ∈ lc(ϕ): i he e exis s a wo ld ∈Wsuch ha w i and ψ∈ c (ρ( , c)) hen hπikλiψ∈ c w(ρ(w, c)); • hsend(m)kλiψ∈ lc(ϕ): i c0= (c1, c2? m) whe e c= (c1, c2) and ψ∈ c0 w(ρ(w, c0)) hen hsend(m)kλiψ∈ c w(ρ(w, c)); • hλksend(m)iψ∈ lc(ϕ): i c0= (c1? m, c2) whe e c= (c1, c2) and ψ∈ c0 w(ρ(w, c0)) hen hλksend(m)iψ∈ c w(ρ(w, c)); • h ec(m)kλiψ∈ lc(ϕ): i c0= (c1, c2) whe e c= (m?c1, c2) and ψ∈ c0 w(ρ(w, c0)) hen h ec(m)kλiψ∈ c w(ρ(w, c)); • hλk ec(m)iψ∈ lc(ϕ): i c0= (c1, c2) whe e c= (c1, m ? c2) and ψ∈ c0 w(ρ(w, c0)) hen hλk ec(m)iψ∈ c w(ρ(w, c)). In he p e ious de ini ion he sign ?deno es he conca ena ion o messages. A un ρis called w-sa u a ed o w∈W, i o all lis s o messages cand o all o mulae he ollowing condi ions a e sa is ied: • hπikλiψ∈ lc(ϕ): i hπikλiψ∈ c w(ρ(w, c)) hen he e exis s a wo ld ∈Wsuch ha w i and ψ∈ c (ρ( , c)); • hsend(m)kλiψ∈ lc(ϕ): i hsend(m)kλiψ∈ c w(ρ(w, c)) hen ψ∈ c0 w(ρ(w, c0)) whe e i c= (c1, c2) hen c0= (c1, c2? m); • hλksend(m)iψ∈ lc(ϕ): i hλksend(m)iψ∈ c w(ρ(w, c)) hen ψ∈ c0 w(ρ(w, c0)) whe e i c= (c1, c2) hen c0= (c1? m, c2); • h ec(m)kλiψ∈ lc(ϕ): i h ec(m)kλiψ∈ c w(ρ(w, c)) hen ψ∈ c0 w(ρ(w, c0)) whe e i c= (m?c1, c2) hen c0= (c1, c2); • hλk ec(m)iψ∈ lc(ϕ): i hλk ec(m)iψ∈ c w(ρ(w, c)) hen ψ∈ c0 w(ρ(w, c0)) whe e i c= (c1, m ? c2) hen c0= (c1, c2). A un is sa u ed, i i is w-sa u a ed o all w∈W.Q= (F, q, R,C) is aPDL×PDL-quasimodel o ϕi (F, q) is a basic s uc u e o ϕo dep h m≤md(ϕ) such ha (qm2) he e exis s a wo ld w0∈Wand ϕ∈ (ε,ε) w0(x0), whe e x0is he oo o ³T(ε,ε) w0, R(ε,ε) w0,1, . . . , R(ε,ε) w0,k´. Ris a se o cohe en and sa u a ed uns h ough (F, q) and Cis a se o bina y ela ion on Rsa is ying he ollowing condi ions: (qm3) o all ρ, ρ0∈ R, i ρCiρ0 hen ρ(w, c)Rc w,iρ0(w, c) o all w∈Wand lis s o messages c. (qm4) R06=εand o all l < m,ρ∈ Rl,w∈W, o all lis s o messages c, x∈Tc w, o all 1 ≤i≤k, i ρ(w, c)Rc w,ix hen he e is ρ0∈ Rl+1 such ha ρ0(w, c) = xand ρCiρ0. PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC 9 Lemma 1. An ML2 o mula ϕsa is iable in a p oduc ame F × G i he e is a PDL×PDL-quasimodel o ϕbased on F. P oo . Le (F, q, R,C) be a PDL×PDL-quasimodel o ϕbased on F, whe e F= (W, 1, . . . , k). Take he p oduc ame F × (R,C), and de ine a alua ion Vin i as ollows: V(pi) = {(w, ρ, c)|p∈ c w(ρ(w, c))} o e e y p oposi ional a iable pi. Le Mbe (F × (R,C),V). By induc ion on he cons uc ion o ψ∈ lc(ϕ) we need o show ha o e e y (w, ρ, c)∈ M we ha e (w, ρ, c)|= Mψi ψ∈ c w(ρ(w, c)). •Fo a iables his ollows om he de ini ion. •Fo Booleans, ypes a e Boolean sa u a ed se s. •(w, ρ, c)|= Mhπikλiψ(based on he de ini ion o he seman ics) i he e exis s a wo ld w0∈Wsuch ha w iw0and (w0, ρ, c)|= Mψ. Then by induc ion hypo hesis (IH) ψ∈ c w0(ρ(w0, c)). ρis sa u a ed and cohe en , so he p e ious holds i hπikλiψ∈ c w(ρ(w, c)). •(w, ρ, c)|= Mhλkπiiψ(based on he de ini ion o he seman ics) i he e exis s a un ρ0∈ R such ha ρCiρ0and (w, ρ0, c)|= Mψ. Then by IH ψ∈ c w(ρ0(w, c)). Acco ding o (qm3), om ρCiρ0we ge ρ(w, c)Rc w,iρ0(w, c). Finally based on (qm1) we ge ha hλkπiiψ∈ c w(ρ(w, c)). In o he di ec ion le assume, ha hλkπiiψ∈ c w(ρ(w, c)) Then by (qm1) he e exis s a x∈Tc wsuch ha ρ(w, c)Rixand ψ∈ c w(x). Acco ding o (qm4) he e exis s ρ0∈ R such ha ρCiρ0and ψ∈ c w(ρ0(w, c)). By IH we ge (w, ρ0, c)|= Mψand inally acco ding o he de ini ion o he seman ics (w, ρ, c)|= Mhλkπiiψ. •(w, ρ, c)|= Mhsend(m)kλiψi (w, ρ, c0)|= Mψwhe e i c= (c1, c2) hen c0= (c1, c2? m) (by de .). Then by IH ψ∈ c0 w(ρ(w, c0)). ρis sa u a ed and cohe en , so he p e ious holds i hsend(m)kλiψ∈ c w(ρ(w, c)). •(w, ρ, c)| = Mhλksend(m)iψi (w, ρ, c0)| = Mψwhe e i c= (c1, c2) hen c0= (c1? m, c2) (by de .). Then by IH ψ∈ c0 w(ρ(w, c0)). ρis sa u a ed and cohe en , so he p e ious holds i hλksend(m)iψ∈ c w(ρ(w, c)). •(w, ρ, c)|= Mh ec(m)kλiψi (w, ρ, c0)|= Mψwhe e i c0= (c1, c2) hen c= (m ? c1, c2) (by de .). Then by IH ψ∈ c0 w(ρ(w, c0)). ρis sa u a ed and cohe en , so he p e ious holds i h ec(m)kλiψ∈ c w(ρ(w, c)). •(w, ρ, c)|= Mhλk ec(m)iψi (w, ρ, c0)|= Mψwhe e i c0= (c1, c2) hen c= (c1, m ? c2) (by de .). Then by IH ψ∈ c0 w(ρ(w, c0)). ρis sa u a ed and cohe en , so he p e ious holds i hλk ec(m)iψ∈ c w(ρ(w, c)). 10 L´ ASZL´ O ASZAL´ OS AND PHILIPPE BALBIANI •(w, ρ, c)|= Mhψ?kλiχi (w, ρ, c)|= Mψand (w, ρ, c)|= Mχ. By IH his is ue i ψ∈ c w(ρ(w, c)) and χ∈ c w(ρ(w, c)). Bu acco ding o ( 7) his is ue i hψ?kλiχ∈ c w(ρ(w, c)) •(w, ρ, c)|= Mhλkψ?iχi (w, ρ, c)|= Mψand (w, ρ, c)|= Mχ. By IH his is ue i ψ∈ c w(ρ(w, c)) and χ∈ c w(ρ(w, c)). Bu acco ding o ( 8) his is ue i hλkψ?iχ∈ c w(ρ(w, c)) •(w, ρ, c)|= Mhα(α1∪α2)kβiψi (w, ρ, c)|= Mhα(α1)kβiψo (w, ρ, c)|= Mhα(α2)kβiψ(by de .). By IH his is ue i hα(α1)kβiψ∈ c w(ρ(w, c)) o hα(α2)kβiψ∈ c wρ(w, c)). Bu acco ding o ( 5) his is ue i hα(α1∪α2)kβiψ∈ c w(ρ(w, c)) •(w, ρ, c)|= Mhαkβ(β1∪β2)iψi (w, ρ, c)|= Mhαkβ(β1)iψo (w, ρ, c)|= Mhαkβ(β2)iψ(by de .). By IH his is ue i hαkβ(β1)iψ∈ c w(ρ(w, c)) o hαkβ(β2)iψ∈ c w(ρ(w, c)). Bu acco ding o ( 6) his is ue i hαkβ(β1∪β2)iψ∈ c w(ρ(w, c)) •(w, ρ, c)|= Mhπi;αkλiψi he e exi s a wo ld w0such ha w iw0and (w0, ρ, c)|= Mhαkλiψ(by de .). Then by IH hαkλiψ∈ c w0(ρ(w0, c)). ρ is cohe en and sa u a ed, so hπikλihαkλiψ∈ c w(ρ(w, c)). Acco ding o ( 2) his is ue i hπi;αkλiψ∈ c w(ρ(w, c)). •(w, ρ, c)|= Mhλkπi;βiψi he e exi s a un ρ0∈ R such ha ρCiρ0 and (w, ρ0, c)|= Mhλkβiψ(by de .). Then by IH hλkβiψ∈ c w(ρ0(w, c)). Acco ding o (qm3) ρ(w, c)Rc w,iρ0(w, c), and by (qm1) hλkπiihλkβiψ∈ c w(ρ(w, c)). Acco ding o ( 3) his is ue i hλkπi;βiψ∈ c w(ρ(w, c)). •(w, ρ, c)|= Mhπi;αkπj;βiψi (w, ρ, c)|= Mhπikλihαkπj;βiψo (w, ρ, c)|= Mhλkπjihπi;αkβiψ. Based on p e ious poin s o his p oo we ge ha hπikλihαkπj;βiψ∈ c w(ρ(w, c)) o hλkπjihπi;αk βiψ∈ c w(ρ(w, c)). Acco ding o ( 4) his is ue i hπi;αkπj;βiψ∈ c w(ρ(w, c)). The e o e by (qm2), ϕis sa is ied in M. Fo he o he di ec ion, suppose ha ϕis sa is ied in a model Mbased on he p oduc F × G o ames F= (W, 1, . . . , k) and G= (∆, R1, . . . , Rk) By p oposi ion 1.7 and 3.9 in [5] we may assume, ha Gis an in ansi i e ee o dep h m≤md(ϕ) and (w0, x0,(ε, ε)) |= Mϕ o some w0∈Wwi h x0being he oo o G. Wi h e e y iple (w, x, c) whe e w∈W,x∈∆ and cis a lis s o messages we associa e he ype (w, x, c) = {ψ∈ lc(ϕ)|(w, x, c)|= Mψ}. Fix wand cand de ine a bina y ela ion ∼c won ∆ as ollows: •i x,y∈∆ o dep h 0 hen x∼c wyi (w, x, c) = (w, y, c). •i x,y∈∆ o dep h l < md(ϕ) hen x∼c wyi (w, x, c) = (w, y, c) and o all z∈∆ and o all 1 ≤i≤k PROVING THE DECIDABILITY OF THE PDL×PDL PRODUCT LOGIC 11 –i xRiz hen he e exis s a z0∈∆ such ha yRiz0and z∼c wz0 –i yRiz hen he e exis s a z0∈∆ such ha xRiz0and z∼c wz0. Clea ly ∼c wis an equi alence ela ion on ∆. Deno e by [x]c w he ∼c w-equi alence class o x, and pu ∆c w®{[x]c w|x∈∆},sc w([x]c w)® (w, x, c) and [x]c wRc w,i[y]c wi he e exis s a y0∈∆c wsuch ha xRiy0. Then by he de ini- ion o ∼c w, c wis well-de ined, and he s uc u e ((∆c w, c w), sc w) clea ly sa is ies (qm1’). The map x7→ [x]c wis a p-mo phism om (∆, 2) o (∆c w, c w), so i also sa is ies (qm1). Howe e (∆c w, c w) is no necessa ily a ee. The ee (Tc w, <c w) we need can be ob ained om his s uc u e: Tc w=n([x0]c w, . . . , [xl]c w)¯¯¯l≤m, [x0]c w c wi1[x1]c w· · · [xl−1]c w c w,il−1[xl]c wo I u, ∈Tc w hen u <c w,i i u= ([x0]c w, . . . , [xl]c w), = ([x0]c w, . . . , [xl]c w,[xl+1]c w) and xlRixl+1. c w([x0]c w,...,[xl]c w)® (w, x, c). I is easy o show ha ((Tc w, <c w), c w) is a quasis a e o ϕ o any w∈Wand messages c. Mo e- o e ϕ∈ (ε,ε) w0³[x0](ε,ε) w0´. So by aking q(w, c)®((Tc w, <c w,1, . . . , <c w,k), c w) o each w∈Wand each message cwe ob ain a basic s uc u e (F, q) o ϕ s a is ying (qm2). We need o de ine uns ough (F, q). To do his o each l≤mand each sequence (x0, . . . , xl) in ∆ such ha x0Ri1· · · Rilxl, ake he map ρ: (w, c)7→ ([x0]c w, . . . [x0]c w). I is easy o check ha ρis a cohe en and a sa u a ed l- un. Le Rbe he se o all such uns. Fo ρ,ρ0∈ R le ρCiρ0i ρ(w, c)<c wρ0(w, c) o all w∈Wand o all messages c. Then (qm3) holds by de ini ion. I emains o p o e (qm4). Le ρ∈ Rl, ∈W, cany messages and z∈Tc be such ha ρ( , c)<c z. We ha e o show ha he e is ρ0∈ Rl+1 such ha ρCiρ0, and ρ0( , c) = z. Since ρ( , c)<c ,i z, we ha e ρ( , c) = ([x0]c , . . . , [xl]c ) and z= ([x0]c , . . . , [xl]c ,[xl+1]c ) o some x1, . . . , xl, xl+1 wi h x0Rc j1x1· · · Rc jlxland [xl]c c ,i[xl+1]c . By he de ini ion o Rc ,i he e is y∈[xl+1]c such ha xlRiy. Bu hen he 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 o ϕ. 4. Blocks A block o ϕwi h oo wis quad uple B= (F, q, R,C) such ha • F = (∆, <) is a ee o dep h less equal 1 wi h oo w •(F, q) is a basic s uc u e o ϕo dep h m o some m < md(ϕ) • R is a se o cohe en and sa u a ed uns h ough (F, q) •Cis a se o bina y ela ion on Rsa is ying (qm3) and (qm4) A se So blocks o ϕis called sa is ying, i •all blocks in Sa e o he same dep h m o some m < md(ϕ)