index.md (2914B)
1 +++ 2 title = 'Temporal logic' 3 +++ 4 # Temporal logic using temporal frames 5 Linear time logic: events along a single computation path. 'at some point we will have p' 6 7 Branching time logic: quantify over possible paths. 'there is a path where eventually p' 8 9 A frame F = (T, <) is a temporal frame if both: 10 - < is irreflexive: not t < t for all t 11 - < is transitive: if t < u and u < v then t < v 12 13 Truth and validity: 14 15  16 17 Right-linearity: 18 - "all future points are related" 19 - definition: ∀ x,y,z: (x < y) ∧ (x < z) → (y < z) ∨ (y = z) ∨ (z < y) 20 - is modally definable 21 22 Right-branching: 23 - "right-branching is _not_ right-linear, so some point has two unrelated points in the future" 24 - definition: there exist x,y,z such that x < y and x < z but ¬ (y < z) ∧ y ≠ z ∧ ¬ (z < y) 25 - is _not_ modally definable 26 27 Discrete: 28 - "every point with a successor has an immediate successor 29 - definition: (x < y ) → ∃ z : x < z ∧ ¬ ∃ u: ( x < u) ∧ (u < z) 30 - is modally definable in basic temporal logic 31 32 Dense: 33 - "between any two points is a third one" 34 - definition: x < z → ∃ y (x < y ∧ y < z) 35 - is modally definable 36 37 Operator next: 38 - symbol ⊗ 39 - M,t ⊨ ⊗ φ iff ∃ v : t < v ∧ (¬ ∃ u : t < u < v) ∧ M,v ⊨ φ 40 - e.g. x ⊨ ⊗p: there a future we can reach only in 1 step from x where p holds 41 - not true if other options. e.g. you can go directly from Centraal to Utrecht, but Amstel station is still there. 42 - next not definable in basic modal logic 43 44 Operator until: 45 - symbol U 46 - M,t ⊨ φ U ψ iff ∃ v : t < v ∧ M,v ⊨ ψ ∧ ∀ u : t < u < v → M,u ⊨ φ 47 - if we have a future where ψ holds, then φ holds in all points between now and that future 48 - not definable in basic modal logic 49 50 Examples of until: 51 52 <table> 53 <tr> 54 <td> 55 56  57 58 <details> 59 <summary>Graphviz code</summary> 60 61 <!-- :Tangle(dot) until-1.dot --> 62 ```dot 63 digraph g { 64 rankdir=BT 65 a -> b 66 a -> c 67 c -> d 68 b -> d 69 c -> e 70 c [xlabel="p"] 71 d [xlabel="q"] 72 e [xlabel="q"] 73 } 74 ``` 75 </details> 76 77 </td> 78 <td> 79 80  81 82 <details> 83 <summary>Graphviz code</summary> 84 85 <!-- :Tangle(dot) until-2.dot --> 86 ```dot 87 digraph g { 88 rankdir=BT 89 a -> b 90 a -> c 91 c -> d 92 b -> d 93 d [xlabel="q"] 94 c [xlabel="p"] 95 } 96 ``` 97 98 </details> 99 </td> 100 </tr> 101 102 <tr> 103 <td> 104 a ⊨ p U q. e.g. state e, we have q, and in any paths we have to go through states that have p. 105 </td> 106 107 <td> 108 a ⊭ p U q. because we do not have p in state b. 109 </td> 110 </tr> 111 </table> 112 113 In a temporal frame: 114 - ◇ p is equivalent to T U p 115 - ⊗ p i equivalent to ⊥ U p 116 117 <!-- 118 TODO: Things to look at: 119 - until not definable in basic modal logic in temporal frames 120 - until not definable in temporal modal logic in temporal frames 121 - next not definable in basic modal logic in temporal frames 122 - define discrete in temporal logic 123 - use next to define discrete in temporal logic 124 - define right-linearity in temporal logic 125 -->