1 files changed, 76 insertions, 0 deletions
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex
new file mode 100644
index 0000000..43942b5
--- /dev/null
+++ b/Assignment1/semantics.tex
@@ -0,0 +1,76 @@
+\subsubsection{Semantics}
+\erin
+The semantics of LTL and PLTL are defined in a very similar way.
+However, we must make some modifications to the definitions.
+\camil
+In particular, the $\vDash$ operator must be redefined.
+Recall that for LTL we wrote $\sigma \vDash \phi$ when $\sigma$ satisfies $\phi$ and $\sigma[i\dots]$ for the suffix of $\sigma$ starting in the $(j+1)$st symbol.
+The latter notation effectively loses information about the prefix.
+In the case of PLTL, we cannot lose this information.
+For this reason, we use a satisfaction relation at a specific index.
+We will write this as $\sigma \vDash_i \phi$, read as \enquote{$\sigma$ satisfies $\phi$ at $i$}.%
+\footnote{%
+	The notation used in literature varies.
+	\citet{Lichtenstein1985} use $(\sigma,i) \vDash \phi$; \citet{Markey2003} uses $\sigma,i \vDash \phi$.
+	Although the difference is minor, we find $\vDash_i$ more intuitive because it shows that the object being checked is the same in $\sigma\vDash_i\phi$ and $\sigma\vDash_j\phi$.}
+We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$.
+
+\erin
+\begin{definition}[Semantics of PLTL (Interpretation over Words)]
+	Let $\phi$ be a PLTL formula over $AP$. The LT property induced by $\phi$ is
+	\[Words(\phi) = \{\sigma \in \left(2^{AP}\right)^\omega \mid \sigma \vDash \phi\}\]
+	where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times \mathbb{N} \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics}.
+\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$.
+
+\begin{figure}
+	\centering
+	\begin{mdframed}
+	\[
+		\begin{matrix*}[l]
+			\sigma &\vDash_i & \text{true}\\
+			\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 & \phi_1\Uop\phi_2  &\text{iff} & \exists_{j \le 0}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_i \phi_1$ for all $0 \le i < j$}\\
+			\sigma &\vDash_i & \phi_1\Sop\phi_2  &\text{iff} & \exists_{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} & i \geq 1 \wedge \sigma \vDash_{i-1} \phi
+		\end{matrix*}
+	\]
+	\end{mdframed}
+	\caption{PLTL semantics for infinite words $\sigma=A_0A_1A_2\dots \in \left(2^{AP}\right)^\omega$.}
+	\label{fig:PLTL-semantics}
+\end{figure}
+
+\erin
+\begin{definition}[Semantics of PLTL over Paths and States]
+	Let $TS = (S, Act, \rightarrow, I, AP, L)$ be a transition system without terminal states, and let $\phi$ be an PLTL-formula over AP.
+	\begin{itemize}
+		\item For infinite path fragments $\pi$ of $TS$, the satisfaction relation is defined by
+			\[\pi \vDash \phi \Leftrightarrow trace(\pi) \vDash \phi\]
+		\item For state $s \in S$, the satisfaction relation $\vDash$ is defined by
+			\[s \vDash \phi \Leftrightarrow \forall_{\pi \in Paths(s)}[\pi \vDash \phi]\]
+			\item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
+				\qedhere
+	\end{itemize}
+\end{definition}
+In order to make these definitions suitable for use with our PLTL operators,
+we must provide their semantics.
+\Cref{fig:PLTL-semantics} shows the formal semantics of the operators defined in the grammar.
+Note that we need to add a index $i$, since we must also be able to look in the past.
+
+Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well:
+\[
+	\begin{matrix*}[l]
+		\sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{k \leq i}[\sigma \vDash_k \phi]\\
+		\sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{k \leq i}[\sigma \vDash_k \phi]
+	\end{matrix*}
+\]