index.md (2372B)
1 +++ 2 title = 'Exercise 5' 3 template = 'page-math.html' 4 +++ 5 # Exercise 5 6 ## 2b 7 Show validity of: [a\*] ↔ φ ∧ [α][α\*]φ 8 - Take a PDL model M = ((W,R),V) and let x ∈ W 9 - Implication left-to-right: 10 - assume x ⊨ [a\*]φ 11 - so for every y ∈ W such that $(x,y) \in R_{\alpha *}$, y ⊨ φ 12 - because M is a PDL model, $R_{\alpha \*} = (R_{\alpha})\* = R_{\alpha}^{0} \cup R_{\alpha}^{1} \cup R_{\alpha}^{2} \dots$ 13 - So $R_{\alpha}^{0} = Id \subseteq R_{\alpha \*}$ so $(x,x) \in R_{\alpha \*}$ so x ⊨ φ. 14 - To prove x ⊨ [α][α\*]φ, take u ∈ W such that $(x,u) \in R_{\alpha}^{1}$. 15 - Aim to show u ⊨ [α\*]φ 16 - Take state v ∈ W such that $(u,v) \in R_{\alpha \*}$ 17 - We have $(x,u) \in (R_{\alpha} ; R_{\alpha \*}) \subseteq R_{\alpha \*}$ 18 - So $(x,v) \in R_{\alpha \*}$ so v ⊨ φ (because x ⊨ [α\*]φ) 19 - Other way is similar. 20 21 ## 4 22 ### a 23 24 25 $\begin{aligned} 26 \delta &= \text{while $\lnot p$ do $b \cup ac$} \\\\ 27 \hat{R}_{\lnot p} &= \\{(2,2), (3,3), (4,4)\\} \\\\ 28 \hat{R}\_{ac} &= R\_{a}; R\_{c} = \\{(1,2), (2,3), (4,3)\\}; \\{(3,1)\\} \\\\ 29 &= \\{(2,1), (4,1) \\} \\\\ 30 R\_{b \cup ac} &= R\_{b} \cup R\_{ac} = \\{(3,4), (3,2), (2,1) \\} \cup \\{(2,1), (4,1)\\} \\\\ 31 &= \\{(3,4), (3,2), (2,1), (4,1)\\} \\\\ 32 R\_{\lnot p; b \cup ac} &= \\{ (2,2), (3,3), (4,4) \\}; \\{(3,4), (3,2), (2,1), (4,1) \\} \\\\ 33 &= \\{(2,1), (3,4), (3,2), (4,1) \\} \\\\ 34 R\_{(\lnot p; b \cup ac)*}: R\_{\lnot p; b \cup ac}^{0} &= \\{(1,1), (2,2), (3,3), (4,4) \\} \\\\ 35 R\_{\lnot p; b \cup ac}^{1} &= \\{(2,1), (3,4), (3,2), (4,1)\\} \\\\ 36 R\_{\lnot p; b \cup ac}^{2} &= R\_{\lnot p; b \cup ac}^{1} \cup \\{(3,1)\\} \\\\ 37 R\_{p} &= \\{(1,1)\\} \\\\ 38 R\_{\delta} &= \\{(1,1), (2,1), (4,1), (3,1) \\} 39 \end{aligned}$ 40 41 42 ### b 43 M ?⊨ [δ]p → p 44 - No. 45 - For example, 2 ⊨ [δ]p because $(2,1) \in R_{\delta}$ and 1 ⊨ p, but 2 ⊭ p.