index.md (5950B)
1 +++ 2 title = 'Bisimulations' 3 template = 'page-math.html' 4 +++ 5 6 # Bisimulations 7 A non-empty relation Z ⊆ W × W' is bisimulation ($Z : M \underline{\leftrightarrow} M'$) if for all pairs (w, w') ∈ Z we have: 8 - w ∈ V(p) iff w' ∈ V'(p) 9 - if Rwv then for some v' ∈ W' we have R'w'v' and vZv' 10 - if R'w'v' then for some v ∈ W we have Rwv and vZv' 11 12 Two models are bisimilar ($M \underline{\leftrightarrow} M'$) if there exists a bisimulation Z ∈ W × W'. 13 14 Basically, models are bisimilar if they are, in essence, the same (there may be extra states or relations in one of the models but those states/relations do not add any new information compared to the other model). A bisimulation then is the set of pairs of states that are bisimilar between two models. 15 16 Two pointed models are bisimilar if there exists a bisimulation Z such that (w,w') ∈ Z 17 18 Two states are modally equivalent if they satisfy exactly the same formulas. 19 So if M,w and M',w' are bisimilar, then they are modally equivalent. 20 21 If two states are modally equivalent, then they are bisimilar. 22 23 ## Example of a bisimulation 24 It's a bit hard to describe this in words, but intuitive if you see it. 25 Here's an example with two models: 26 27  28 29 You see that from the top state, you can get to a terminal state in one or two steps, in both models. 30 Therefore, the top states of both models are _bisimilar_. 31 Since all of the states in the models are bisimilar, _the two models are bisimilar_. 32 The dotted lines connect the pairs that make up the _bisimulation_. 33 34 ## Example: finding bisimulations 35 36 Take two example models: 37 38 <table> 39 <thead> 40 <th>A</th> <th>B</th> 41 </thead> 42 43 <tbody> 44 <tr> 45 46 <td> 47 48  49 50 <details> 51 <summary>Graphviz code</summary> 52 53 <!-- :Tangle(dot) model-a.dot --> 54 ```dot 55 digraph g { 56 1 -> 2 57 2 -> 3 58 3 -> 4 59 3 -> 5 60 1 [xlabel="p"] 61 2 [xlabel="q"] 62 3 [xlabel="q"] 63 4 [xlabel="q"] 64 5 [xlabel="q"] 65 } 66 ``` 67 68 </details> 69 </td> 70 71 <td> 72 73  74 75 <details> 76 <summary>Graphviz code</summary> 77 78 <!-- :Tangle(dot) model-b.dot --> 79 ```dot 80 digraph g { 81 a -> b 82 a -> c 83 c -> d 84 b -> d 85 d -> e 86 a [xlabel="p"] 87 b [xlabel="q"] 88 c [xlabel="q"] 89 d [xlabel="q"] 90 e [xlabel="q"] 91 } 92 ``` 93 94 </details> 95 </td> 96 97 </tr> 98 </table> 99 100 The claim is that states (A,1) and (B,a) are bisimilar. 101 How do you prove or refute the claim? 102 103 Well, we need to find a bisimulation with the pair (1, a). 104 1. Start with pair (1, a) 105 2. In A, move from 1 to 2. Have to mimic the move in B, can do so by moving from a to b or from a to c. 106 Yields the pairs (2, b) and (2, c). 107 3. In A, move from 2 to 3. Have to mimic the move in B, can move from both b and c to d. 108 Yields the pair (3, d). 109 4. In A, two options: 110 - move from 3 to 4. Have to mimic the move in B, can move from d to e. 111 Yields the pair (4, e). 112 - move from 3 to 5. Have to mimic the move in B, can move from d to e. 113 Yields the pair (5, e). 114 115 Since for any move in the first model, we can mimic it in the second model, we have a bisimulation. 116 The bisimulation contains exactly the pairs we just listed. 117 So there is a bisimulation Z = {(1, a), (2, b), (2, c), (3, d), (4, e), (5, e)}. 118 Since (1, a) ∈ Z, we can say that states (A, 1) and (B, a) are bisimilar. 119 120 If two states are bisimilar, then they are modally equivalent. 121 Prove by induction on definition of formulas. 122 123 For finitely branching models, if two states are modally equivalent, then they are bisimilar. 124 Prove by taking modal equivalence as bisimulation. 125 126 <details> 127 <summary>Proof of modal equivalence implying bisimilar</summary> 128 129 Let Z := {(x, x') | for all φ: x ⊨ φ iff x' ⊨ φ}. 130 Z is a bisimulation. 131 - Local harmony is satisfied. 132 - zig: suppose (x, x') ∈ Z and x → y. 133 Because x ⊨ ◇ T also x' ⊨ ◇ T. 134 So x' has finitely many successors y'₁...y'n with n ≥ 1. 135 Suppose for all i: y is not modally equivalent to y'ᵢ. 136 There are φ₁...φn such that y ⊨ φᵢ and y'ᵢ ⊭ φᵢ. 137 x ⊨ ◇(φ₁ ∧ ... ∧ φn) so also x' ⊨ ◇ (φ₁ ∧ ... ∧ φn). 138 Contradiction. 139 140 </details> 141 142 Asymmetry is not modally definable. 143 To deal with only frames, we can use surjective bounded morphisms. 144 145 Function f : W → W' is bounded morphism from (W,R) to (W',R') if: 146 - for all w,v ∈ W: if Rwv then Rf(w)f(v) 147 - for all w ∈ W and for all v' ∈ W': if R'f(w)v' then there exists v ∈ W such that f(v) = v' and Rwv 148 149 A bounded morphism f is surjective if for every w' ∈ W' there exists w ∈ W such that f(w) = w' 150 151 If f: W → W' is surjective bounded morphism from (W,R) to (W',R'), then if (W,R) ⊨ φ then (W', R') ⊨ φ 152 153 ## Modal depth of formulas 154 Modal formulas are 'nearsighted': 155 - md(p) = md(⊥) = md(T) = 0 156 - md(¬φ) = md(φ) 157 - md(φ ∨ ψ) = md(φ ∧ ψ) = max{md(φ), md(ψ)} 158 - md(□ φ) = md(◇ φ) = md(φ) + 1 159 160 ## A bisimulation game for two players 161 Spoiler S claims M,s an N,t to be different. 162 Duplicator D claims they are similar. 163 164 Play consists of sequence of links, starting with link s ~ t. 165 166 At current link m ~ n (with m in M and n in N): 167 - if m and n different in their atoms, then S wins 168 - if not, then S picks a successor x either of m or of n 169 - then D has to find a matching transition to y in the other model 170 - play continues with next link x ~ y (or y ~ x) 171 172 If player cannot make a move, he loses. 173 D wins infinite games. 174 175 There's an example of this [in exercise class 3](../exercise-3/#a). 176 177 We need a formula of model depth k to distinguish states x and y. 178 Spoiler can win bisimulation game in k rounds. 179 Every winning strategy for Spoiler corresponds to a distinguishing formula. 180 Games of less than k rounds can be won by Duplicator. 181 Formulas of modal depth less than k cannot distinguish between x and y. 182 183 M,s and N,t satisfy the same formulas up to modal depth k iff duplicator has winning strategy in the k-round game starting in s ~ t. 184 If Spoiler can win in k rounds, then there is a distinguishing formula of modal depth k.