index.md (3414B)
1 +++ 2 title = 'Propositional dynamic logic (PDL)' 3 template = 'page-math.html' 4 +++ 5 # Propositional dynamic logic (PDL) 6 In propositional dynamic logic (PDL), aim to prove: φ → [while σ do α] ψ 7 - i.e. starting with φ true, for any terminating execution of the program, we have ψ true. 8 9 Definitions: 10 - state of program execution: state/world 11 - program: regular program which slightly generalizes a while program 12 - statement {pre}program{post}: formula pre → [program] post 13 14 For every program α we have modality 〈α〉: 15 - 〈α〉φ: it's possible to execute α from current state, and successfully halt in state satisfying φ (like existential quantification) 16 - [α]φ: for all executions of α, if α successfully halts, then it halts in a state satisfying φ (like universal quantification) 17 18 Program definitions: 19 - a: program from set A of atomic programs (letters, like in prop. logic) 20 - α; β: sequential composition 21 - α ∪ β: non-deterministic choice 22 - α\*: iteration, 0 or more times. 23 - φ?: test, depends on the grammar for formulas 24 - if φ then continue without changing state, if not then block without halting 25 26 Examples of formulas: 27 28  29 30 We obtain semantics of PDL as instance of multi-modal logic. 31 32 Operators: 33 - composition "R;S" = {(x, z) | ∃ y : Rxy ∧ Syz} 34 - union "R ∪ S" = {(x, y) | Rxy ∨ Sxy} 35 - R\*: repeat R one or more times 36 37 A model M is a PDL-model if the frame is a PDL-frame and $R_{\phi ?} = \\{ (w,w) \\;|\\; M, w \models \phi\\}$ 38 39 The R of the frame is all sets of Rₐ where _a_ is a program (i.e. a label on an arrow). 40 41 <details> 42 <summary>Proof example of 〈α, β〉 p → 〈α〉〈β〉p</summary> 43 44 - Take a PDL model and a state x. 45 - Assume x ⊨ 〈α, β〉 p 46 - That is, there is a state y such that $(x, y) \in R_{\alpha;\beta}$ and y ⊨ p. 47 - $R_{\alpha;\beta} = R_{\alpha}; R_{\beta}$ 48 - That is, there is a state u such that $(x, u) \in R_{\alpha}$ and $(u,y) \in R_{\beta}$. 49 - Because $(u,y) ∈ R_{\beta}$ and y ⊨ p, we have u ⊨ 〈β〉 p 50 - Because $(x,u) ∈ R_{\alpha}$, we have and u ⊨ 〈β〉p we have x ⊨ 〈α〉〈β〉p. 51 </details> 52 53 If then else: 54 - program: `if p then a else b` 55 - encoding: (p?; a) ∪ (¬ p? ; b) 56 57 <details> 58 <summary>Example</summary> 59 60  61 62 <details> 63 <summary>Graphviz code</summary> 64 65 <!-- :Tangle(dot) model-if-then-else.dot --> 66 ```dot 67 digraph g { 68 rankdir=LR 69 1 [xlabel="[p]"] 70 1 -> 2 [label="a"] 71 4 -> 2 [label="b"] 72 1 -> 3 [label="b"] 73 4 -> 3 [label="a"] 74 } 75 76 ``` 77 78 </details> 79 80 Calculate the relation for `if p then a else b`, which is encoded as `(p?; a) ∪ (¬ p?; b)`: 81 82  83 </details> 84 85 While: 86 - program: `while p do a` 87 - encoding: (p?; a)\*; ¬ p? 88 89 <details> 90 <summary>Example</summary> 91 92  93 94 <details> 95 <summary>Graphviz code</summary> 96 97 <!-- :Tangle(dot) model-while.dot --> 98 ```dot 99 digraph g { 100 rankdir=LR 101 1 -> 2 [label="a"] 102 2 -> 3 [label="a"] 103 3 -> 4 [label="a"] 104 4 -> 5 [label="a"] 105 5 -> 6 [label="a"] 106 1 [xlabel="[p]"] 107 2 [xlabel="[p]"] 108 3 [xlabel="[p]"] 109 4 [xlabel="[p]"] 110 } 111 ``` 112 113 </details> 114 115 Calculating the relation `while p do a`, encoded as `(p?; a)*; ¬ p?`: 116 117  118 </details> 119 120 If E is a bisimulation between two A-models, then it is a bisimulation for the models' PDL-extensions. 121 However, intersection and inverse are not safe for bisimulation.