index.md (4732B)
1 +++ 2 title = 'Homework 1' 3 +++ 4 # Homework 1 5 ## 1 6 ### a 7 - We aim to show M,v ⊨ ◇ (q ∧ ◇ p). 8 - For the formula to hold, (q ∧ ◇ p) must hold in at least one successor of v. 9 - v has two R-successors: v and y. 10 - q ∧ ◇ p does not hold in v, because v ⊭ q. 11 - However, y ⊨ q ∧ ◇ p: y ⊨ q, and Ryz and z ⊨ p, thus y ⊨ ◇ p. 12 - Therefore, M,v ⊨ ◇ (q ∧ ◇ p). 13 14 ### b 15  16 17 If Verifier chooses the left branch (M, y ⊨ q ∧ ◇ p), he always wins. 18 19 <details> 20 <summary>Graphviz code</summary> 21 22 <!-- :Tangle(dot) game-tree.dot --> 23 ```dot 24 graph t { 25 t [label="M,v ⊨? ◇ (q ∧ ◇ p)", xlabel="V's turn"] 26 tl [label="M,y ⊨? q ∧ ◇ p", xlabel="F's turn"]; t -- tl 27 tll [label="{ M,y ⊨ q | Verifier wins }", shape="Mrecord"]; tl -- tll 28 tlr [label="M, y ⊨? ◇ p", xlabel="V's turn"]; tl -- tlr 29 tlrn [label="{ M, z ⊨ p | Verifier wins. }", shape="Mrecord"]; tlr -- tlrn 30 31 tr [label="M, v ⊨? q ∧ ◇ p", xlabel="F's turn"]; t -- tr 32 trl [label="{ M, v ⊭ q | Falsifier wins }", shape="Mrecord", xlabel="V's turn"]; tr -- trl 33 trr [label="M, v ⊨? ◇ p", xlabel="V's turn"]; tr -- trr 34 trrl [label="{ M, v ⊭ p | Falsifier wins. }", shape="Mrecord"]; trr -- trrl 35 trrr [label="{M, y ⊭ p | Falsifier wins.}", shape="Mrecord"]; trr -- trrr 36 } 37 38 ``` 39 40 </details> 41 42 ## 2 43 ### a 44 - Goal is to show ⊨ (◇ p → □ q) → (□ p → □ q). 45 - Take an arbitrary frame F = (W,R), V a valuation on F, and x ∈ W. Let M = (F, V). 46 - Assume M, x ⊨ (◇ p → □ q), where M = (F, V). 47 - Aim to show M, x ⊨ □ p → □ q. 48 - Assume M, x ⊨ □ p, aim to show M, x ⊨ □ q. 49 - If x has no successors, ◇ p does not hold, hence M, x ⊨ □ q ex falso (also by assumption). 50 - If x has successors, and p is valid in at least one of them, x ⊨ ◇ p, hence M, x ⊨ □ q by assumption. 51 - If x has successors, an p is not valid in any of them, x ⊨ □ q because ◇ p is not valid in x. 52 - Because the model and state are arbitrary, the formula is universally valid. 53 54 ### b 55 - Goal is to show ⊨ ¬ ◇ □ p → ◇ ◇ ¬ p. 56 - Consider the frame F = ({x}, ∅) and valuation V(p) = ∅. 57 - In state x, ◇ □ p is not valid, because x has no successors, hence x ⊨ ¬ ◇ □ p. 58 - However, since x has no successors, x ⊭ ◇ ◇ ¬ p. 59 - Therefore, the implication doesn't hold, and the formula is not universally valid. 60 61 ## 3 62 We aim to show that F ⊨ p → □ ◇ p iff F is symmetric: ∀ x, y ∈ W (Rxy → Ryx). 63 64 * Assume that in a frame F = (W,R), F ⊨ p → □ ◇ p. 65 - Assume towards a contradiction that F is not symmetric. 66 - Then there must be states x, y ∈ W such that Rxy but not Ryx. 67 - Take a model M = (F, V), with valuation V(p) = {x}. 68 - Then, M, x ⊨ p. 69 - x has successor y, but y does not have x as a successor, therefore M, y ⊭ p → □ ◇ p, so F ⊭ □ ◇ p. 70 - This contradicts the assumption. 71 72 * Assume that a frame F = (W, R) is symmetric. 73 - We aim to show that F ⊨ p → □ ◇ p. 74 - Take an arbitrary model M = (F, V) and an arbitrary state x ∈ M. 75 - Assume that M, x ⊨ p and aim to show M, x ⊨ □ ◇ p. 76 - If x has no successors, then x ⊨ □ ◇ p. 77 - If there is y ∈ W such that Rxy, then we must also have Ryx by the assumption that F is symmetric. 78 - Because x ⊨ p and y ⊨ p, x ⊨ □ ◇ p and y ⊨ □ ◇ p. 79 - Because the state x and the model M are arbitrary, F ⊨ □ ◇ p. 80 81 * We have therefore shown that the formula p → □ ◇ p characterizes the frame property "symmetry". 82 83 ## 4 84 ### a 85 86 <table> 87 <tr> <th>Model A</th> <th>Model B</th> <th>Model C</th> </tr> 88 <tr> 89 90 <td> 91 92  93 94 <details> 95 <summary>Graphviz code</summary> 96 97 <!-- :Tangle(dot) model-a.dot --> 98 ```dot 99 digraph g { 100 a -> b 101 b -> a 102 a -> c 103 b -> d 104 } 105 ``` 106 107 </details> 108 </td> 109 110 <td> 111 112  113 114 <details> 115 <summary>Graphviz code</summary> 116 117 <!-- :Tangle(dot) model-b.dot --> 118 ```dot 119 digraph g { 120 1 -> 2 121 2 -> 1 122 1 -> 3 123 1 -> 4 124 } 125 ``` 126 127 </details> 128 129 </td> 130 131 <td> 132 133  134 135 <details> 136 <summary>Graphviz code</summary> 137 138 <!-- :Tangle(dot) model-c.dot --> 139 ```dot 140 digraph g { 141 1 [label="#"] 142 1 -> b 143 } 144 ``` 145 146 </details> 147 148 </td> 149 </tr> 150 </table> 151 152 ### b 153 - A, a ⊨ ◇ ◇ □ ⊥, but B, 1 ⊭ ◇ ◇ □ ⊥. 154 - A, d ⊨ □ ⊥, so A, b ⊨ ◇ □ ⊥, so A, a ⊨ ◇ ◇ □ ⊥. 155 - B, 4 ⊨ □ ⊥, so B, 1 ⊨ ◇ □ ⊥ but only B, 2 ⊨ ◇ ◇ □ ⊥, not state 1. 156 157 ### c 158 Because the states a ∈ A and 1 ∈ B are not modally equivalent as shown in exercise 4b above. 159 160 ### d 161 Take the set Z = {(a, #), (b, #), (c, b), (d, b)}. 162 We claim that Z is a bisimulation, and (a, #) ∈ Z, therefore they are bisimilar. 163 No proof is necessary here.