lectures.alex.balgavy.eu

commit 6aea3a00fa9ab5db4634c2d2f8cbdec7f5b6e17d
parent e5eef87c4dfe82b93ed5c2ce7a0be1caf954d237
Author: Alex Balgavy <alex@balgavy.eu>
Date:   Thu, 17 Feb 2022 11:51:11 +0100

Advanced logic lecture 4

Diffstat:
M
content/advanced-logic-notes/_index.md
 | 
1
+
A
content/advanced-logic-notes/lecture-4.md
 | 
38
++++++++++++++++++++++++++++++++++++++

2 files changed, 39 insertions(+), 0 deletions(-)
diff --git a/content/advanced-logic-notes/_index.md b/content/advanced-logic-notes/_index.md
@@ -6,6 +6,7 @@ title = 'Advanced Logic'
 2. [Lecture 2](lecture-2)
 3. [Exercise 1](exercise-1)
 4. [Lecture 3](lecture-3)
+5. [Lecture 4](lecture-4)
 
 I drew the graphs on these pages with [Graphviz](https://graphviz.org/).
 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-4.md b/content/advanced-logic-notes/lecture-4.md
@@ -0,0 +1,38 @@
++++
+title = 'Lecture 4'
+template = 'page-math.html'
++++
+
+# Lecture 4
+## Bisimulations
+A non-empty relation Z ⊆ W × W' is bisimulation ($Z : M \underline{\leftrightarrow} M'$) if for all pairs (w, w') ∈ Z we have:
+- w ∈ V(p) iff w' ∈ V'(p)
+- if Rwv then for some v' ∈ W' we have R'w'v' and vZv'
+- if R'w'v' then for some v ∈ W we have Rwv and vZv'
+
+Two models are bisimilar ($M \underline{\leftrightarrow} M'$) if there exists a bisimulation Z ∈ W × W'.
+
+Two pointed models are bisimilar if there exists a bisimulation such that (w,w') ∈ Z
+
+Two states are modally equivalent if they satisfy exactly the same formulas.
+So if M,w and M',w' are bisimilar, then they are modally equivalent.
+
+## Transforming and constructing models
+Disjoint union of models: combine models by union of states, relations, and valuations.
+A state in one of the models is modally equivalent with the state in the union.
+
+Generated submodel: starting from state w, only take its future.
+
+Tree unravelling: unravelling of world s in (W,R,V) is:
+- $W' : (s_{1} \dots s_{n})$ with $s_{1} = s$ and $Rs_{i} s_{i+1}$
+- $R'$ relates ($s_{1} \dots s_{n}$) to ($s_{1} \dots s_{n+1}$) if $Rs_{n} s_{n+1}$
+- $V'(p) = \{ (s_{1} \dots s_{n} | s_{n} \in V(p) \}$
+- a state in (W',R',V') is bisimilar to $s_{n}$ in (W,R,V)
+- if φ is satisfiable in M,w it is satisfiable in tree unravelling of s in M
+
+Bisimulation contraction
+- W' consists of equivalence classes |s| = { t such that $s \underline{\leftrightarrow} t$ }
+- R' relates |s| to |t| if Ruv for some u ∈ |s| and some v ∈ |t|
+- V'(p) = { |s| | s ∈ V(p) }
+
+If two states are modally equivalent, then they are bisimilar.