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(ϕ)