commit fc70cca85a415e5f36216d7c260eacde1b9abc02
parent 9ee9ee677ad1a21810c947573692b501ff2ab897
Author: Alex Balgavy <alex@balgavy.eu>
Date: Thu, 17 Mar 2022 10:46:53 +0100
Advanced logic lecture 12
Diffstat:
8 files changed, 271 insertions(+), 1 deletion(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -17,7 +17,8 @@ title = 'Advanced Logic'
13. [Lecture 10](lecture-10/)
14. [Exercise 4](exercise-4/)
15. [Some midterm solutions](some-midterm-solutions/)
-15. [Lecture 11](lecture-11/)
+16. [Lecture 11](lecture-11/)
+17. [Lecture 12](lecture-12/)
I drew the graphs on these pages with [Graphviz](https://graphviz.org/), I used [vim-literate-markdown](https://github.com/thezeroalpha/vim-literate-markdown)'s tangling functionality to quickly extract graph code to separate files.
You can install Graphviz and run e.g. `dot < graph.dot -Tsvg > graph.svg` (also accepts input files as parameters).
diff --git a/content/advanced-logic-notes/lecture-12/if-then-else-calculation.png b/content/advanced-logic-notes/lecture-12/if-then-else-calculation.png
Binary files differ.
diff --git a/content/advanced-logic-notes/lecture-12/index.md b/content/advanced-logic-notes/lecture-12/index.md
@@ -0,0 +1,92 @@
++++
+title = 'Lecture 12'
+template = 'page-math.html'
++++
+# Lecture 12
+- composition "R;S" = {(x, z) | ∃ y : Rxy ∧ Syz}
+- union "R ∪ S" = {(x, y) | Rxy ∨ Sxy}
+- R\*: repeat R one or more times
+
+A model M is a PDL-model if the frame is a PDL-frame and $R_{\phi ?} = \\{ (w,w) \\;|\\; M, w \models \phi\\}$
+
+The R of the frame is all sets of Rₐ where _a_ is a program (i.e. a label on an arrow).
+
+<details>
+<summary>Proof example of 〈α, β〉 p → 〈α〉〈β〉p</summary>
+- Take a PDL model and a state x.
+- Assume x ⊨ 〈α, β〉 p
+- That is, there is a state y such that $(x, y) \in R_{\alpha;\beta}$ and y ⊨ p.
+- $R_{\alpha;\beta} = R_{\alpha}; R_{\beta}$
+- That is, there is a state u such that $(x, u) \in R_{\alpha}$ and $(u,y) \in R_{\beta}$.
+- Because $(u,y) ∈ R_{\beta}$ and y ⊨ p, we have u ⊨ 〈β〉 p
+- Because $(x,u) ∈ R_{\alpha}$, we have and u ⊨ 〈β〉p we have x ⊨ 〈α〉〈β〉p.
+</details>
+
+If then else:
+- program: `if p then a else b`
+- encoding: (p?; a) ∪ (¬ p? ; b)
+
+<details>
+<summary>Example</summary>
+
+
+
+<details>
+<summary>Graphviz code</summary>
+
+<!-- :Tangle(dot) model-if-then-else.dot -->
+```dot
+digraph g {
+rankdir=LR
+1 [xlabel="[p]"]
+1 -> 2 [label="a"]
+4 -> 2 [label="b"]
+1 -> 3 [label="b"]
+4 -> 3 [label="a"]
+}
+
+```
+
+</details>
+
+Calculate the relation for `if p then a else b`, which is encoded as `(p?; a) ∪ (¬ p?; b)`:
+
+
+</details>
+
+While:
+- program: `while p do a`
+- encoding: (P?; a)\*; ¬ p?
+
+<details>
+<summary>Example</summary>
+
+
+
+<details>
+<summary>Graphviz code</summary>
+
+<!-- :Tangle(dot) model-while.dot -->
+```dot
+digraph g {
+rankdir=LR
+1 -> 2 [label="a"]
+2 -> 3 [label="a"]
+3 -> 4 [label="a"]
+4 -> 5 [label="a"]
+5 -> 6 [label="a"]
+1 [xlabel="[p]"]
+2 [xlabel="[p]"]
+3 [xlabel="[p]"]
+4 [xlabel="[p]"]
+}
+```
+
+</details>
+
+Calculating the relation `while p do a`, encoded as `(p?; a)*; ¬ p?`:
+
+
+</details>
+
+If E is a bisimulation between two A-models, then it is a bisimulation for the models' PDL-extensions.
diff --git a/content/advanced-logic-notes/lecture-12/model-if-then-else.dot b/content/advanced-logic-notes/lecture-12/model-if-then-else.dot
@@ -0,0 +1,10 @@
+digraph g {
+rankdir=LR
+1 [xlabel="[p]"]
+1 -> 2 [label="a"]
+4 -> 2 [label="b"]
+1 -> 3 [label="b"]
+4 -> 3 [label="a"]
+}
+
+
diff --git a/content/advanced-logic-notes/lecture-12/model-if-then-else.dot.svg b/content/advanced-logic-notes/lecture-12/model-if-then-else.dot.svg
@@ -0,0 +1,66 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: g Pages: 1 -->
+<svg width="175pt" height="126pt"
+ viewBox="0.00 0.00 175.00 125.79" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 121.79)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-121.79 171,-121.79 171,4 -4,4"/>
+<!-- 1 -->
+<g id="node1" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="43" cy="-89.79" rx="27" ry="18"/>
+<text text-anchor="middle" x="43" y="-86.09" font-family="Times,serif" font-size="14.00">1</text>
+<text text-anchor="middle" x="8" y="-60.59" font-family="Times,serif" font-size="14.00">[p]</text>
+</g>
+<!-- 2 -->
+<g id="node2" class="node">
+<title>2</title>
+<ellipse fill="none" stroke="black" cx="140" cy="-99.79" rx="27" ry="18"/>
+<text text-anchor="middle" x="140" y="-96.09" font-family="Times,serif" font-size="14.00">2</text>
+</g>
+<!-- 1->2 -->
+<g id="edge1" class="edge">
+<title>1->2</title>
+<path fill="none" stroke="black" d="M69.96,-92.52C80.12,-93.59 91.94,-94.83 102.91,-95.99"/>
+<polygon fill="black" stroke="black" points="102.76,-99.49 113.07,-97.06 103.49,-92.53 102.76,-99.49"/>
+<text text-anchor="middle" x="91.5" y="-98.59" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+<!-- 3 -->
+<g id="node4" class="node">
+<title>3</title>
+<ellipse fill="none" stroke="black" cx="140" cy="-30.79" rx="27" ry="18"/>
+<text text-anchor="middle" x="140" y="-27.09" font-family="Times,serif" font-size="14.00">3</text>
+</g>
+<!-- 1->3 -->
+<g id="edge3" class="edge">
+<title>1->3</title>
+<path fill="none" stroke="black" d="M63.22,-77.85C76.91,-69.35 95.52,-57.79 110.88,-48.25"/>
+<polygon fill="black" stroke="black" points="112.83,-51.16 119.48,-42.91 109.14,-45.21 112.83,-51.16"/>
+<text text-anchor="middle" x="91.5" y="-65.59" font-family="Times,serif" font-size="14.00">b</text>
+</g>
+<!-- 4 -->
+<g id="node3" class="node">
+<title>4</title>
+<ellipse fill="none" stroke="black" cx="43" cy="-24.79" rx="27" ry="18"/>
+<text text-anchor="middle" x="43" y="-21.09" font-family="Times,serif" font-size="14.00">4</text>
+</g>
+<!-- 4->2 -->
+<g id="edge2" class="edge">
+<title>4->2</title>
+<path fill="none" stroke="black" d="M69.59,-28.27C78.21,-30.33 87.53,-33.6 95,-38.79 102.15,-43.75 113.79,-60.09 123.3,-74.61"/>
+<polygon fill="black" stroke="black" points="120.53,-76.78 128.89,-83.3 126.42,-72.99 120.53,-76.78"/>
+<text text-anchor="middle" x="91.5" y="-42.59" font-family="Times,serif" font-size="14.00">b</text>
+</g>
+<!-- 4->3 -->
+<g id="edge4" class="edge">
+<title>4->3</title>
+<path fill="none" stroke="black" d="M60.57,-10.61C70.34,-3.96 83.09,1.79 95,-1.79 101.71,-3.8 108.35,-7.2 114.35,-10.99"/>
+<polygon fill="black" stroke="black" points="112.4,-13.9 122.63,-16.68 116.37,-8.13 112.4,-13.9"/>
+<text text-anchor="middle" x="91.5" y="-5.59" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/lecture-12/model-while.dot b/content/advanced-logic-notes/lecture-12/model-while.dot
@@ -0,0 +1,13 @@
+digraph g {
+rankdir=LR
+1 -> 2 [label="a"]
+2 -> 3 [label="a"]
+3 -> 4 [label="a"]
+4 -> 5 [label="a"]
+5 -> 6 [label="a"]
+1 [xlabel="[p]"]
+2 [xlabel="[p]"]
+3 [xlabel="[p]"]
+4 [xlabel="[p]"]
+}
+
diff --git a/content/advanced-logic-notes/lecture-12/model-while.dot.svg b/content/advanced-logic-notes/lecture-12/model-while.dot.svg
@@ -0,0 +1,88 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN"
+ "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<!-- Generated by graphviz version 2.50.0 (20211204.2007)
+ -->
+<!-- Title: g Pages: 1 -->
+<svg width="563pt" height="59pt"
+ viewBox="0.00 0.00 563.00 59.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
+<g id="graph0" class="graph" transform="scale(1 1) rotate(0) translate(4 55)">
+<title>g</title>
+<polygon fill="white" stroke="transparent" points="-4,4 -4,-55 559,-55 559,4 -4,4"/>
+<!-- 1 -->
+<g id="node1" class="node">
+<title>1</title>
+<ellipse fill="none" stroke="black" cx="43" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="43" y="-29.3" font-family="Times,serif" font-size="14.00">1</text>
+<text text-anchor="middle" x="8" y="-3.8" font-family="Times,serif" font-size="14.00">[p]</text>
+</g>
+<!-- 2 -->
+<g id="node2" class="node">
+<title>2</title>
+<ellipse fill="none" stroke="black" cx="140" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="140" y="-29.3" font-family="Times,serif" font-size="14.00">2</text>
+<text text-anchor="middle" x="105" y="-3.8" font-family="Times,serif" font-size="14.00">[p]</text>
+</g>
+<!-- 1->2 -->
+<g id="edge1" class="edge">
+<title>1->2</title>
+<path fill="none" stroke="black" d="M70.21,-33C80.28,-33 91.96,-33 102.81,-33"/>
+<polygon fill="black" stroke="black" points="102.87,-36.5 112.87,-33 102.87,-29.5 102.87,-36.5"/>
+<text text-anchor="middle" x="91.5" y="-36.8" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+<!-- 3 -->
+<g id="node3" class="node">
+<title>3</title>
+<ellipse fill="none" stroke="black" cx="237" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="237" y="-29.3" font-family="Times,serif" font-size="14.00">3</text>
+<text text-anchor="middle" x="202" y="-3.8" font-family="Times,serif" font-size="14.00">[p]</text>
+</g>
+<!-- 2->3 -->
+<g id="edge2" class="edge">
+<title>2->3</title>
+<path fill="none" stroke="black" d="M167.21,-33C177.28,-33 188.96,-33 199.81,-33"/>
+<polygon fill="black" stroke="black" points="199.87,-36.5 209.87,-33 199.87,-29.5 199.87,-36.5"/>
+<text text-anchor="middle" x="188.5" y="-36.8" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+<!-- 4 -->
+<g id="node4" class="node">
+<title>4</title>
+<ellipse fill="none" stroke="black" cx="334" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="334" y="-29.3" font-family="Times,serif" font-size="14.00">4</text>
+<text text-anchor="middle" x="299" y="-3.8" font-family="Times,serif" font-size="14.00">[p]</text>
+</g>
+<!-- 3->4 -->
+<g id="edge3" class="edge">
+<title>3->4</title>
+<path fill="none" stroke="black" d="M264.21,-33C274.28,-33 285.96,-33 296.81,-33"/>
+<polygon fill="black" stroke="black" points="296.87,-36.5 306.87,-33 296.87,-29.5 296.87,-36.5"/>
+<text text-anchor="middle" x="285.5" y="-36.8" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+<!-- 5 -->
+<g id="node5" class="node">
+<title>5</title>
+<ellipse fill="none" stroke="black" cx="431" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="431" y="-29.3" font-family="Times,serif" font-size="14.00">5</text>
+</g>
+<!-- 4->5 -->
+<g id="edge4" class="edge">
+<title>4->5</title>
+<path fill="none" stroke="black" d="M361.21,-33C371.28,-33 382.96,-33 393.81,-33"/>
+<polygon fill="black" stroke="black" points="393.87,-36.5 403.87,-33 393.87,-29.5 393.87,-36.5"/>
+<text text-anchor="middle" x="382.5" y="-36.8" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+<!-- 6 -->
+<g id="node6" class="node">
+<title>6</title>
+<ellipse fill="none" stroke="black" cx="528" cy="-33" rx="27" ry="18"/>
+<text text-anchor="middle" x="528" y="-29.3" font-family="Times,serif" font-size="14.00">6</text>
+</g>
+<!-- 5->6 -->
+<g id="edge5" class="edge">
+<title>5->6</title>
+<path fill="none" stroke="black" d="M458.21,-33C468.28,-33 479.96,-33 490.81,-33"/>
+<polygon fill="black" stroke="black" points="490.87,-36.5 500.87,-33 490.87,-29.5 490.87,-36.5"/>
+<text text-anchor="middle" x="479.5" y="-36.8" font-family="Times,serif" font-size="14.00">a</text>
+</g>
+</g>
+</svg>
diff --git a/content/advanced-logic-notes/lecture-12/while-calculation.png b/content/advanced-logic-notes/lecture-12/while-calculation.png
Binary files differ.
