Modal Logics And Bisimulation Invariance

The modal logic restricted to formulas of modal depth N is denoted by ML .De nition 2.5 (Standard translation to FO). The standard translation of a ML-formulaϕ to rst order logic, denoted [ϕ] , is as follows:[P (x)] P (x),[ ψ] [ψ] ,[ψ θ] [ψ] [θ] ,[ψ θ] [ψ] [θ] ,[ψ θ] [ψ] [θ] ,[ ψ] (x) y(Exy [ψ] (y/x)), and[ ψ] (x) y(Exy [ψ] (y/x)).Since this translation uses only two variables, which can be cycled repeatedly in nestedmodal quanti ers, this de nition essentially embeds modal logic into FO2 . The remainderof this chapter is used to nd the precise fragment of FO that corresponds to modal logic.De nition 2.6 ( -neighbourhood). Suppose M is a Kripke structure with a distinguishedelement m. Given a natural number , the -neighbourhood of m is the set U (m) of allnodes reachable from m on E -paths of length at most .De nition 2.7 (Tree structures). A Kripke structure with a distinguished element, M, m,is called a tree structure if E M is acyclic and every other world can be reached from mby a unique path. A branch of the tree is a path, which cannot be expanded further andthe worlds at the end of branches are called leaves. The depth of a tree structure is theE -length of its longest branch. A Kripke structure M, m is said to be -locally a treestructure if the restriction M U (m), m is a tree structure.De nition 2.8 (Property of Kripke structures). A property of pointed Kripke structuresis a class of Kripke structures closed under isomorphisms.The following concept expresses the idea that whether a structure has a property canbe deduced from a restriction of the structure.De nition 2.9 ( -locality). A property K of Kripke structures is said to be -local, for N, if for every Kripke structure M, m(M, m) K (M U (m), m) K.If the property K is de ned by a formula ϕ, -locality can be expressed as the equivalenceM, m ϕ M U (m), m ϕ.6

2.2Equivalences and BisimulationIn order to better grasp the upcoming concepts, we will go through some more familiar relations from rst order logic. The upcoming bisimulation relations are similar toequivalence, but more limited in range, giving them some unique features.In the following de nitions and lemmas we assume that M (W, E M , PM ) and00M0 (W 0 , E M , PM ) are Kripke structures.De nition 2.10 (Quanti er depth). The quanti er depth of a FO-formula ϕ, denotedqd(ϕ), is de ned recursively as follows:1. if ϕ P x, or ϕ P x, for some variable x, qd(ϕ) 0;2. if ϕ ψ θ, ϕ ψ θ, or ϕ ψ θ for some FO-formulae ψ and θ, qd(ϕ) max(qd(ϕ), qd(θ));3. if ϕ ψ , or ϕ ψ , for some FO-formula ψ , qd(ϕ) qd(ψ) 1.De nition 2.11 (FO-equivalence). Two structures M, m and M0 , m0 are FO-equivalent,denoted M, m FO M0 , m0 , if M [m/x] ϕ if and only if M0 [m0 /x] ϕ, for all FO-formulaeϕ(x). The two structures are FO-equivalent to depth n, for some n N if M [m/x] ϕ ifand only if M0 [m0 /x] ϕ, for all FO-formulas ϕ such that qd(ϕ) n. This is denoted by00M, m FOn M ,m .De nition 2.12 (Partial isomorphism). A partial function f : M M0 is a partialisomorphism if the function g : M Dom(f ) M0 Rng(f ) de ned by g(a) f (a) isan isomorphism.De nition 2.13 (Partially isomorphic structures). Let k be a natural number. TwoKripke structures M, m and M0 , m0 are k partially isomorphic, written M, m k M0 , m0 ,if there exists a sequence (In )n k of non-empty sets of partial isomorphisms f , for which(m, m0 ) f , between M and M0 , such that it has the following properties:1. For every partial isomorphism f In 1 and w W there is a partial isomorphismg In , such that f g and w Dom(g),2. For every partial isomorphism f In 1 and w0 W 0 there exists a partial isomorphism g In , such that f g and w0 Rng(g).A classic result in model theory states that for two structures M and M0 , M, m nM0 , m0 if and only if M, m n M0 , m0 and, furthermore, both claims are equivalent withthe duplicator having a winning strategy in the n-round Ehrenfeucht-Fraïsse game. Formore details on this topic see for example [5].7

Now we shall de ne similar concepts for modal logic and show an equivalence result ofa similar nature. This requires us to de ne rstly equivalence in modal logic, secondly thebisimulation relation, and thirdly a game that encapsulates the essence of this relation.De nition 2.14 (ML-equivalence). Two Kripke structures M, m and M0 , m0 are ML-equivalent, denoted M, m ML M0 , m0 , if M, m ϕ if and only if M0 , m0 ϕ, for allML-formulas ϕ. The two Kripke structures are ML-equivalent to depth n, for some n Nif M, m ϕ if and only if M0 , m0 ϕ, for all ML-formulas ϕ such that md(ϕ) n. This00is denoted by M, m MLn M ,m .De nition 2.15 (Atomic correspondence). Two worlds w W and w0 W 0 are said tobe in atomic correspondence if they satisfy the same atomic formulae, i.e.M, w P x M 0 , w0 P xfor all P P.De nition 2.16 (Bisimulation). A bisimulation between M and M0 is a binary relation W W 0 such that, for w W and w0 W 0 , if w w0 , then the following hold:1. w and w0 are in atomic correspondence,2. if (w, v) E M for some world v W , then there exists a world v 0 W 0 such that0v v 0 and (w0 , v 0 ) E M ,3. if (w0 , v 0 ) E M for some world v 0 W 0 , then there exists a world v W such thatv 0 v and (w, v) E M .0When a bisimulation exists between M, w and M0 , w0 they are said to be bisimilar.We de ne the bounded variant of the bisimulation by recursion. The resulting relationis similar, despite the di erences in their de nition.De nition 2.17 (k-bisimulation). Let w W and w0 W 0 be worlds and k N.k-bisimulations between M and M0 are de ned recursively as follows:M, w 0 M0 , w0 if and only if w and w0 are in atomic correspondence,M, w k 1 M0 , w0 if and only if the following hold:M, w 0 M0 , w0 ,0Mfor every v E [{w}] there exists v 0 E M [{w0 }] such that v k v 0 , andfor every v 0 E M [{w0 }] there exists v E M [{w}] such that v k v 0 .If M, m k M0 , m0 they are said to be k-bisimilar.8

2.3Bisimulation as a GameBisimulation can alternatively be de ned by a zero-sum game of perfect information playedby two players, denoted I and II in this text. During each round of the game eachplayer moves a pebble in one of the two Kripke structures starting from either of thedistinguished elements. Player I moves the pebble of his choice forward along an E -edge,thereby challenging player II, who responds by moving the other pebble forward alongan E -edge in the other model. The victory condition for player II is that she maintainsatomic equivalence; she loses if the played worlds of a given turn do not agree on monadicpredicates or she runs out of worlds connected by E .De nition 2.18 (Bisimulation game). Assume M and M0 are two Kripke structures,with the same vocabulary P and distinguished elements m and m0 respectively. Thebisimulation game BG(M, m, M0 , m) over M and M0 is a game, where the winningcondition consists of plays x0 , y0 , x1 , y1 , . such that player II has adhered to the followingrules:1. If x0 m, then y0 m0 , and if x0 m0 , then y0 m. In either case, m and m0have atomic correspondence.2. If xn mn , where mn W and (mn 1 , mn ) E M for mn 1 from the previous round,0then yn m0n , where m0n W 0 and (m0n 1 , m0n ) E M . Otherwise, if xn m0n ,0where m0n W 0 and (m0n 1 , m0n ) E M for m0n 1 from the previous round, thenyn mn , where mn W and (mn 1 , mn ) E M . Additionally m0n and mn haveatomic correspondence.Both players continue playing worlds as long as there are E -edges from previously playedworlds.In a similar vein, k-bisimulations can be de ned through a k-round bisimulation game.De nition 2.19 (Winning strategy). A strategy for player II of a bisimulation gameBG(M, m, M0 , m0 ) is an in nite sequenceσ (σ0 , σ1 , .)of functions σi : (W W 0 )i W W 0 such that σn (v0 , ., vn 1 , w) W 0 for all w Wand σ(v0 , ., vn 1 , w0 ) W for all w0 W 0 , where v0 , ., vn 1 W W 0 and n N. Astrategy is said to be a winning strategy if all possible plays x0 , σ0 (x0 ), x1 , σ1 (x0 , x1 ), .are contained in the winning condition of the game. In other words, a winning strategyis a way for player II to decide what to play that maintains atomic correspondence andan unbroken path to the distinguished worlds.9

Before showing how these concepts are related to each other we shall de ne Hintikkaformulae, which are modal logic formulae that crystallise the information about a worldin a Kripke structure.De nition 2.20 (Hintikka formula). Assume P {Pi i I} for some nite indexset I and let J I be index sets such that M, m Pi x if and only if i J . TheHintikka formula for M, m of depth n, χn[M,m] , for some n N, is de ned recursively inthe following manner:χ0[M,m] i Jχn 1[M,m] χ0[M,m] Pi x Pi x;i I\J χn[M,u] u E M [m]χn[M,u] .u E M [m]An immediate result from this de nition is that, for every Kripke structure M, m,M, m χn[M,m] , for all n N.Lemma 2.21. There are a nite number of Hintikka formulae of depth k up to equiva-lence, for every k N.Proof. We will prove the claim by induction on the depth of the Hintikka formula. Bysimple combinatorics there are 2 P possible combinations of the predicates in P, which isnite since P is nite. Hence the number of Hintikka formulae of depth 0 is nite.Suppose there are a nite number of Hintikka formulae of depth k up to equivalence.Now consider a Hintikka formula of depth k 1. As we already showed, there are anite number of Hintikka formulae of depth 0. For the conjunction and disjunction wehave a selection of Hintikka formulae of depth k, of which there is a nite number by theinduction hypothesis. Multiplying these numbers together gives the amount of Hintikkaformulae of depth k 1 which is nite.By the induction principle, a Hintikka formula of any depth is equivalent to a niteformula and there are a nite number of Hintikka formulae of that depth.Now we are ready to connect these concepts together: that the game actually is analternative de nition for the bisimulation relation and that they are equivalent with claimsregarding modal logic equivalence and Hintikka formulae.Lemma 2.22. Suppose M, m and M0 , m0 are Kripke structures, and let N. Thefollowing are equivalent:1. M, m M0 , m0 ;10

2. Player II has a winning strategy in the -round bisimulation game over M, m andM0 , m0 ;M0 , m0 ;3. M, m ML 4. M0 , m0 χ [M,m] .Proof. 1. 2.: Assume M, m M0 , m0 . Consider the -round bisimulation gameover M, m and M0 , m0 . We will show by induction on the rounds of the game that thebisimulation relation de nes a winning strategy for player II. Basis case: in the rst roundplayer I plays either m or m0 , and player II plays the other one. Since the models at thoseworlds are bisimilar, the worlds have atomic correspondence. Hence player II has upheldthe winning conditions.Induction case: assume player II has adhered to the winning conditions for the previousn rounds. Now we can assume that on round n 1 player I can play either a worldfrom W or one from W 0 , since otherwise the game is over and player II is victorious.Suppose player I plays a world mn 1 W , such that (mn , mn 1 ) E M , for a worldmn played in the previous round. Since player II has been playing according to thebisimulation relation the other world played during the previous round m0n W 0 is suchthat M, mn (n 1) M0 , m0n . Now, as n 1 , the bisimulation relation states there0exists a world m0n 1 W 0 such that (m0n , m0n 1 ) E M and the worlds mn 1 and m0n 1have atomic correspondence. Hence player II can play m0n 1 and uphold the winningcondition. An analogous argument holds for when player I plays a world from W 0 , due tothe third condition of the -bisimulation. Therefore by the induction principle if M, m M0 , m0 , then player II has a winning strategy in the -round BG(M, m, M0 , m0 ).2. 3.: Assume player II has a winning strategy in the -round bisimulation gameover M, m and M0 , m0 . Let ϕ be a ML -formula. We will show by induction on thestructure of ϕ that if player II has a winning strategy in the -round bisimulation gameover M, w and M0 , w0 , then M, w ϕ if and only if M0 , w0 ϕ, for all worlds w Wand w0 W 0 . Assume then w and w0 are such that player II has her winning strategy.Base step: Suppose ϕ P x or ϕ P x, for some P P. Now M, w ϕ if and onlyif M0 , w0 ϕ, as the winning condition of player II ensures that the initial worlds haveatomic correspondence.Induction step: This step breaks down into several cases.1. ϕ ψ for some ML -formula ψ . Assume as the induction hypothesis that M, w ψ M0 , w0 ψ if player II has a winning strategy. Now the induction hypothesisis equivalent with M, w 2 ψ M0 , w0 2 ψ if player II has a winning strategy, andhence M, w ψ if and only if M0 , w0 ψ .11

2. ϕ ψ θ for some ML -formulae ψ and θ. For the induction hypothesis supposethat M, w ψ M0 , w0 ψ and M, w θ M0 , w0 θ, if player II has awinning strategy. Seeing as this is the case, by the de nition of a ML-formula itfollows that M, w ψ θ if and only if M0 , w0 ψ θ.3. ϕ ψ θ for some ML -formulae ψ and θ. Assume for the induction hypothesisthat M, w ψ M0 , w0 ψ and M, w θ M0 , w0 θ, when player II has awinning strategy in the bisimulation game. Since we assumed so, by the de nitionof the disjunction it also holds that M, w ψ θ if and only if M0 , w0 ψ θ.4. ϕ ψ θ for some ML -formulae ψ and θ. The induction hypothesis is thatM, w ψ M0 , w0 ψ and M, w θ M0 , w0 θ, if player II has awinning strategy. Once again, since we assumed the winning strategy to exist, bythe de nition of the semantics of ML-formulae it holds that M, w ψ θ if andonly if M0 , w0 ψ θ.5. ϕ ψ for some ML 1 -formula ψ . As the induction hypothesis assume that ifplayer II has a winning strategy in the 1-round bisimulation game over M, vand M0 , v 0 , then M, v ψ M0 , v 0 ψ , for all v W and v 0 W 0 . Nowassume M, w ψ . By the de nition of the possibility quanti er, there exists aworld v E M [w], such that M, v ψ . Since player II has a winning strategy in0the -round bisimulation game over M, w and M0 , w0 , we let v 0 E M [w0 ] be theworld given by the winning strategy. Now player II has a winning strategy in the 1-round bisimulation game over M, v and M0 , v 0 , and therefore it follows fromthe induction hypothesis that M0 , v 0 ψ . Hence M0 , w0 ψ , by de nition. Theother direction is analogous.6. ϕ ψ for some ML 1 -formula ψ . Suppose player II has a winning strategy in the 1-round bisimulation game over M, v and M0 , v 0 , then M, v ψ M0 , v 0 ψ .0Suppose M, w ψ . If E M [w] is empty we are nished, since then E M [w0 ] isalso empty, or otherwise player II would lose on the second round of the game.Therefore we assume E M [w] is not empty. Suppose v E M [w] is an arbitraryelement. Now M, v ψ , and due to player II's winning strategy there also exists0a world v 0 E M [w0 ]. Since v and v 0 can be played on the second round of theBG(M, w, M0 , w0 ), player II has a winning strategy in the 1-round bisimulationgame over M, v and M0 , v 0 . By the induction hypothesis then M0 , v 0 ψ . Thisargument holds for all v E M [w] and hence M0 , w0 ψ . Analogously for theother direction.By the induction principle M, w ϕ M0 , w0 ϕ for all w W , w0 W 0 , andϕ ML (P), if player II has a winning strategy in the -round bisimulation game over12

M, w and M0 , w0 . In particular M, m ϕ if and only if M0 , m0 ϕ.3. 4.: Assume M, m M0 , m0 . Since md(χ [M,m] ) and M, m χ [M,m] , by thede nition of modal equivalence it follows that M0 , m0 χ [M,m] .4. 1.: Assume M0 , m0 χ [M,m] . We will show that if a world w0 W 0 is suchthat M0 , w0 χk[M,m] , then M, m k M0 , w0 , for all k . Basis case: supposeM0 , w0 χ0[M,m] . Now from the construction of the Hintikka formula it follows immediately that M0 , w0 satis es exactly the same predicates as M, m, and hence they haveatomic correspondence. In other words M, m 0 M0 , w0 .Induction case: k i 1 for some 0 i . For the induction hypothesis supposethat if M0 , v 0 χi[M,v] , then M, v i M0 , v 0 , for all v W and v 0 W 0 . Assume thati 10000M0 , w0 χi 1[M,m] . Now M , w χ[M,m] , since χ[M,m] is one of the conjuncts of χ[M,m] .As explained previously this means M0 , w0 and M, m have atomic correspondence. Thesecond conjunct of χi 1[M,m] is χi[M,u] ,u E M [m]a conjunction in its own right. Now M0 , w0 satis es this conjunction and thereby it alsosatis es each of the conjuncts, i.e. M0 , w0 χi[M,u] for all u E M [m]. This means by0the de nition of the semantics of modal logic that there exists a world u0 E M [w0 ] suchthat M0 , u0 χi[M,u] , for every u E M [m]. It follows now from the induction hypothesis0that for every u E M [m] there exists a world u0 E M [w0 ] such that M, u i M0 , u0 .The third and nal conjunct of χi 1[M,m] is a disjunction quanti ed by a necessity quanti er χi[M,u] .u E M [m]That model M, m satis es this formula is equivalent to M0 , u0 u E M [m] χi[M,u] for every0u0 E M [w0 ], by the de nition of the modal semantics. Since the disjunction runs thegamut of worlds attainable from M, m, the previous claim can be expressed as for every0u0 E M [w0 ] there exists a world u E M [m] such that M0 , u0 χi[M,u] . By the induction0hypothesis this implies that for every u0 E M [w0 ] there exists a world u E M [m]such that M, u i M0 , u0 . Now we have shown all three conditions for the boundedbisimulation M, m i 1 M0 , w0 , hence by the induction principle M, m k M0 , w0 holdsfor all integers 0 k , if M0 , w0 χk[M,m] . Since we assumed that M0 , m0 χ [M,m] , itnow follows that M, m M0 , m0 .WOne of the consequences of this result is that the two de nitions for the boundedbisimulation are equivalent. The game theoretical de nition will be used for the remainderof this chapter.13

This result has the following corollary when one considers the bounded bisimulation asan equivalence relation. That is an apt interpretation, since the identity function de nesa winning strategy for player II in the game BG(M, m, M, m), the game is symmetric by de nition BG(M, m, M0 , m0 ) BG(M0 , m0 , M, m), and if M, m M0 , m0 andM0 , m0 M00 , m00 then the compound function of the strategies for player II is a winningstrategy in the game BG(M, m

rst, a brief run-through of the basic concepts in modal logic. This rst chapter follows the outline of Martin Otto in [7], while expanding on the arguments presented. 2.1 The Fundamentals of Modal Logic The usual way to de ne modal logic in mathematical logic is as an extension of proposi-tional logic, with the de nition of structures in the .