From 7be7f9774737bab46d5b60688b89b790b1624a0f Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Sun, 22 Apr 2018 21:06:18 +0200 Subject: Typesetting --- Assignment1/assignment1.tex | 2 ++ Assignment1/equivalence.tex | 2 +- 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*} \] -- cgit v1.2.3