summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorCamil Staps2018-04-19 20:11:57 +0200
committerCamil Staps2018-04-19 20:11:57 +0200
commitaffdaaba8b1f98cce8b297b6ecdee145b604e88c (patch)
tree7d8cb5dcc6f2c89cbb151a545827744a7e8ff0e1
parentMinor textual enhancements; remove outdated todos (diff)
Fix vertical placing of Xop
-rw-r--r--Assignment1/assignment1.tex4
-rw-r--r--Assignment1/semantics.tex14
-rw-r--r--Assignment1/syntax.tex4
3 files changed, 11 insertions, 11 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index c1e6a0d..d96839e 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -90,11 +90,11 @@
\DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
\DeclareMathOperator{\Uop}{\mathbf{U}}
\DeclareMathOperator{\Wop}{\mathbf{W}}
-\DeclareMathOperator{\Xop}{\bigcirc}
+\DeclareMathOperator{\Xop}{\raisebox{1pt}{$\bigcirc$}}
\DeclareMathOperator{\Fop}{\lozenge}
\DeclareMathOperator{\Gop}{\square}
\DeclareMathOperator{\Sop}{\mathbf{S}}
-\DeclareMathOperator{\Pop}{\bigcirc^{--1}}
+\DeclareMathOperator{\Pop}{\raisebox{1pt}{$\bigcirc$}^{--1}}
\newcommand{\wff}{\emph{wff}} % Well-formed formula
\newcommand{\wffn}{\ifmmode\expandafter\text\fi{\wff\textsuperscript{0}}} % Pure present wff
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex
index dcc8e6b..1bca0b2 100644
--- a/Assignment1/semantics.tex
+++ b/Assignment1/semantics.tex
@@ -24,12 +24,12 @@ We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$.
\end{definition}
\camil
Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation.
-The difference with LTL formulae is well illustrated by the $\bigcirc$ operator.
-In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\bigcirc\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$.
-Thus, whether $\bigcirc\phi$ holds for $\sigma$ cannot depend on $A_0$.
-In the PLTL case, $\sigma\vDash_i\bigcirc\phi$ iff $\sigma\vDash_{i+1}\phi$.
-The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\sigma$ may depend on $A_0$,
- as is trivially the case with $\bigcirc\bigcirc^{-1}a$.
+The difference with LTL formulae is well illustrated by the $\Xop$ operator.
+In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\Xop\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$.
+Thus, whether $\Xop\phi$ holds for $\sigma$ cannot depend on $A_0$.
+In the PLTL case, $\sigma\vDash_i\Xop\phi$ iff $\sigma\vDash_{i+1}\phi$.
+The information about $A_0$ is not lost, so whether $\Xop\phi$ holds for $\sigma$ may depend on $A_0$,
+ as is trivially the case with $\Xop\Xop^{-1}a$.
\begin{figure}
\centering
@@ -40,7 +40,7 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s
\sigma &\vDash_i & a &\text{iff} & a\in A_i\\
\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 & \bigcirc\phi &\text{iff} & \sigma \vDash_{i+1} \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 & \Pop\phi &\text{iff} & \text{$i \geq 1$ and $\sigma \vDash_{i-1} \phi$}
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex
index 5d2830a..6d86281 100644
--- a/Assignment1/syntax.tex
+++ b/Assignment1/syntax.tex
@@ -22,7 +22,7 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2
\enspace\middle|\enspace a
\enspace\middle|\enspace \phi_1 \land \phi_2
\enspace\middle|\enspace \lnot \phi
- \enspace\middle|\enspace \bigcirc \phi
+ \enspace\middle|\enspace \Xop \phi
\enspace\middle|\enspace \phi_1 \Uop \phi_2
\enspace\middle|\enspace \Pop \phi
\enspace\middle|\enspace \phi_1 \Sop \phi_2
@@ -208,6 +208,6 @@ Before turning to the formal semantics in the next subsection, we provide some e
These include
$\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep{Markey2003},
but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep{Gabbay1989}
- and $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep{Havelund2002}.
+ and $\stackinset{c}{}{c}{}{$\cdot$}{$\Xop$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep{Havelund2002}.
\end{remark}
\cbend