diff options
| author | Camil Staps | 2018-04-22 21:06:18 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-04-22 21:06:33 +0200 |
| commit | 7be7f9774737bab46d5b60688b89b790b1624a0f (patch) | |
| tree | e9a805d8a4c2b392b6b2c37cc90d5ddd9b85defb /Assignment1 | |
| parent | OCD (if this causes conflict, feel free to rollback) (diff) | |
Typesetting
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/assignment1.tex | 2 | ||||
| -rw-r--r-- | Assignment1/equivalence.tex | 2 | ||||
| -rw-r--r-- | Assignment1/semantics.tex | 4 |
3 files changed, 5 insertions, 3 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index c75367b..a725397 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -95,6 +95,8 @@ \DeclareMathOperator{\Gop}{\square} \DeclareMathOperator{\Sop}{\mathbf{S}} \DeclareMathOperator{\Pop}{\raisebox{1pt}{$\bigcirc$}^{--1}} +\let\vDash\models +\def\nvDash{\not\models} \newcommand{\wff}{\emph{wff}} % Well-formed formula \newcommand{\wffn}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{0}}} % Pure present wff diff --git a/Assignment1/equivalence.tex b/Assignment1/equivalence.tex index 6373088..660f052 100644 --- a/Assignment1/equivalence.tex +++ b/Assignment1/equivalence.tex @@ -10,7 +10,7 @@ we can define equivalence on PLTL formulas. Additionally, we can define another form of equivalence, initial equivalence. When two formulas are initially equivalent, they are equivalent for all paths at position 0. -This is mainly useful to compare PLTL and LTL formulas. +This is among other things useful to compare PLTL and LTL formulas. \begin{definition}[Initial Equivalence of PLTL Formulae] PLTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property: \[\text{for any path } \pi, \pi \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\] diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index d99e636..05e96fb 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -41,8 +41,8 @@ The information about $A_0$ is not lost, so whether $\Xop\phi$ holds for $\sigma \sigma &\vDash_i & \phi_1\land\phi_2 &\text{iff} & \text{$\sigma\vDash_i\phi_1$ and $\sigma\vDash_i\phi_2$}\\ \sigma &\vDash_i & \lnot\phi &\text{iff} & \sigma \nvDash_i \phi\\ \sigma &\vDash_i & \Xop\phi &\text{iff} & \sigma \vDash_{i+1} \phi\\ - \sigma &\vDash_i & \phi_1\Uop\phi_2 &\text{iff} & \exists_{j \ge i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $i \le k < j$}\\ - \sigma &\vDash_i & \phi_1\Sop\phi_2 &\text{iff} & \exists_{0 \le j \le i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\\ + \sigma &\vDash_i & \phi_1\Uop\phi_2 &\text{iff} & \exists_{j \ge i}\big[\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $i \le k < j$}\big]\\ + \sigma &\vDash_i & \phi_1\Sop\phi_2 &\text{iff} & \exists_{0 \le j \le i}\big[\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\big]\\ \sigma &\vDash_i & \Pop\phi &\text{iff} & \text{$i \geq 1$ and $\sigma \vDash_{i-1} \phi$} \end{matrix*} \] |