Intuitive Semantics

1 files changed, 71 insertions, 2 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index c00caf6..4875752 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -6,6 +6,8 @@
 \usepackage{amsmath}
 \usepackage{amsthm}
 \newtheorem{definition}{Definition}
+\usepackage{tikz}
+\usetikzlibrary{automata,positioning}
 
 \newcommand{\defeq}{\overset{\text{def}}{=}}
 \newcommand{\Uop}{\mathbf{U}}
@@ -56,16 +58,83 @@ It is this option that we will use for this book, since it allows us to focus ex
 	$$\phi ::= l \mid \phi_1 \Sop \phi_2 \mid \Xop^{-1} \phi$$
 	where $l \in LTL$.
 \end{definition}
-Additionally, we extend LTLP further with the following abbreviations:
+
+In this grammar, $\Sop$ is the ``since'' operator and $\Xop^{-1}$ is the ``previous'' operator.
+Intuitively, the since operator defines that the second proposition must have occurred continuously since the first occurred.
+The previous operator defines that a proposition must have occurred in the previous state.
+
+Like we did in LTL, we can also derive additional operators in LTLP:
 \begin{definition}
 	Given $\phi \in LTLP$, then\footnote{Note that we assume that the LTL formulas are also extended as given in subsection 5.1.1}:
 	\begin{align*}
 		%\Fop \phi &\defeq \top \Uop \phi\\
 		%\Gop \phi &\defeq \neg \Fop \neg \phi\\
 		\Fop^{-1} \phi &\defeq \top \Sop \phi\\
-		\Gop^{-1} \phi &\defeq \neg \Fop^{-1} \neg \phi	\end{align*}
+		\Gop^{-1} \phi &\defeq \neg \Fop^{-1} \neg \phi
+	\end{align*}
 \end{definition}
 
+As a result, we can derive the following intuitive meaning for $\Fop^{-1}$ and $\Gop^{-1}$.
+$\Fop^{-1} \phi$ ensures that at some point in the past $\phi$ was true.
+$\Gop^{-1} \phi$ is satisfied only if it is not true that $\phi$ didn't hold in the past.
+This is equivalent to the fact that $\phi$ held globally until this point.
+
+Figure \ref{fig:LTLP_intuitive} shows the intuitive meanings of the past modalities for the simple case where $a$ and $b$ are the only atomic propositions.
+The left hand side of the figure shows some LTLP formulae,
+the right hand side shows sequences for which this formula trivially holds.
+Since we need to also consider the past,
+we include an arrow that points to the state for which the formula holds.
+
+\begin{figure}
+	\centering
+	$a \Sop b$
+	\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,initial text={},baseline=-0.5ex]
+		\node                                          (0)                {\dots};
+		\node[state,label=arbitrary,minimum size=15pt] (1) [right of = 0] {};
+		\node[state,label=$b$      ,minimum size=15pt] (2) [right of = 1] {};
+		\node[state,label=$a$      ,minimum size=15pt] (3) [right of = 2] {};
+		\node[state,label=$a$      ,minimum size=15pt,initial below] (4) [right of = 3] {};
+		\node[state,label=arbitrary,minimum size=15pt] (5) [right of = 4] {};
+		\node                                          (6) [right of = 5] {\dots};
+		\path[->] (0) edge (1) (1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
+	\end{tikzpicture}\\
+	$\Xop^{-1} a$
+	\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,initial text={},baseline=-0.5ex]
+		\node                                          (0)                {\dots};
+		\node[state,label=arbitrary,minimum size=15pt] (1) [right of = 0] {};
+		\node[state,label=arbitrary,minimum size=15pt] (2) [right of = 1] {};
+		\node[state,label=$a$      ,minimum size=15pt] (3) [right of = 2] {};
+		\node[state,label=arbitrary,minimum size=15pt,initial below] (4) [right of = 3] {};
+		\node[state,label=arbitrary,minimum size=15pt] (5) [right of = 4] {};
+		\node                                          (6) [right of = 5] {\dots};
+		\path[->] (0) edge (1) (1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
+	\end{tikzpicture}\\
+	$\Fop^{-1} a$
+	\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,initial text={},baseline=-0.5ex]
+		\node                                          (0)                {\dots};
+		\node[state,label=arbitrary,minimum size=15pt] (1) [right of = 0] {};
+		\node[state,label=$a$      ,minimum size=15pt] (2) [right of = 1] {};
+		\node[state,label=arbitrary,minimum size=15pt] (3) [right of = 2] {};
+		\node[state,label=arbitrary,minimum size=15pt,initial below] (4) [right of = 3] {};
+		\node[state,label=arbitrary,minimum size=15pt] (5) [right of = 4] {};
+		\node                                          (6) [right of = 5] {\dots};
+		\path[->] (0) edge (1) (1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
+	\end{tikzpicture}\\
+	$\Gop^{-1} a$
+	\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,initial text={},baseline=-0.5ex]
+		\node                                          (0)                {\dots};
+		\node[state,label=$a$      ,minimum size=15pt] (1) [right of = 0] {};
+		\node[state,label=$a$      ,minimum size=15pt] (2) [right of = 1] {};
+		\node[state,label=$a$      ,minimum size=15pt] (3) [right of = 2] {};
+		\node[state,label=$a$      ,minimum size=15pt,initial below] (4) [right of = 3] {};
+		\node[state,label=arbitrary,minimum size=15pt] (5) [right of = 4] {};
+		\node                                          (6) [right of = 5] {\dots};
+		\path[->] (0) edge (1) (1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6);
+	\end{tikzpicture}\\
+	\caption{Intuitive semantics of past modalities.}
+	\label{fig:LTLP_intuitive}
+\end{figure}
+
 \subsection{LTL and LTL-Past}
 %TODO: Consider/Analyse differences between LTL and LTL-Past