Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

7 files changed, 57 insertions, 12 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index e859f41..c1e6a0d 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -62,6 +62,8 @@
 \usepackage{algpseudocode}
 \usepackage{tikz}
 \usetikzlibrary{automata,positioning}
+\tikzset{>=stealth}
+\tikzset{state/.append style={minimum size=15pt}}
 \usepackage{relsize}
 \usepackage{parskip}
 \usepackage{cleveref}
@@ -111,14 +113,22 @@
 \setcounter{section}{5}
 \setcounter{subsection}{2}
 
+% The extra newlines are needed for correct changebars
+
 \input{intro}
+
 \input{syntax}
+
 \input{semantics}
+
 \input{equivalence}
+
 \input{conversion}
+
 \input{bad-prefix}
 
 \input{summary}
+
 \input{exercises}
 
 \both
diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex
index c9145b3..e357359 100644
--- a/Assignment1/bad-prefix.tex
+++ b/Assignment1/bad-prefix.tex
@@ -1,6 +1,5 @@
 \camil
 \subsection{Minimal Bad Prefixes}
-%TODO: Given a formula of the form vw^\omega, can we find a n \in \mathbb{N} such that vw^n is a bad prefix?
 \emph{NB: this section is not particularly about PLTL. It is better added as 4.4.3.}
 
 Model checking tools, such as NuSMV, often give counterexamples in the form of $vw^\omega$, i.e., a finite prefix with a infinite loop.
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 5eb9dba..72624e6 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -20,7 +20,11 @@ The syntactic algorithm as proposed by Gabbay has its foundation in the followin
 		For this paragraph we will use Gabbay's definitions.}
 \begin{enumerate}
 	\item Every PLTL formula can be written using no other temporal operators than $\Sop$ and $\Uop$ operators.
-	\item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.
+	\item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.%
+		\footnote{%
+			This is known as the Separation Theorem.
+			It was originally proven by \citet{Gabbay1980}.
+			Folklore has it that when Hans Kamp, a philosopher working on temporal logics, heard of the result, he went out and bought Gabbay a cake (\url{https://cstheory.stackexchange.com/a/29452}, retrieved April 19, 2018).}
 	\item The same formula without past modalities $\psi$, a boolean combination of $\wfff \cup \wffn$, is initially equivalent to $\phi$.
 \end{enumerate}
 When these facts are considered in sequence,
diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
index ddbaa5a..fb2255e 100644
--- a/Assignment1/intro.tex
+++ b/Assignment1/intro.tex
@@ -1,12 +1,8 @@
 \erin
 \subsection{Past Modalities in LTL}\label{sec:intro}
-% Explain that past Modalities are not necessary for a complete logic
-% Explain that PLTL does make the logic more succinct (Paper 1)
-%TODO: Give example on what kind of things we want to express with PLTL
 As mentioned in Remark 5.16, LTL can be extended with \emph{past modalities}.
 This section discusses this extension.
-The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL.
-For the sake of brevity we will use the second (PLTL) to denote this combination.
+The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL; we will use the second.
 When temporal logic was first introduced by Arthur N. Prior in his 1957 book~\cite{Prior1957},
 the logic consisted of both past and future modalities.
 The complexity of the model problem does not increase with this extension~\citep{Sistla1985},
@@ -22,6 +18,5 @@ In other words, there is a class of PLTL formulae%
 	for which the size of all equivalent LTL formulas is $\Omega\left(2^n\right)$.
 Markey achieves this proof by providing a formula that is in exactly this class.
 Besides being smaller, PLTL formulas can also be easier to write and understand, as examples below will demonstrate.
-They are also included in many model checking tools, such as NuSMV.%
-	\footnote{\url{http://nusmv.fbk.eu/}}
+They are also included in many model checking tools, such as NuSMV,\footnote{\url{http://nusmv.fbk.eu/}}, and as we will see in the examples they are used in practice.
 For this reason, it is useful to discuss them here.
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex
index 055d66b..dcc8e6b 100644
--- a/Assignment1/semantics.tex
+++ b/Assignment1/semantics.tex
@@ -51,6 +51,23 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s
 	\label{fig:PLTL-semantics}
 \end{figure}
 
+\begin{example}[Satisfaction of PLTL Formulae by Words]
+	Let $\pi = aabcdcdcd\dots$ be an infinite path over $AP=\{a,b,c,d\}$, of which on every moment only one atomic proposition holds (i.e., at position 0, $a$ holds, at position 2, $b$ holds, etc.).
+	We have for instance:
+
+	\begin{itemize}
+		\item For all $i\in\mathbb N$, $\pi \vDash_i b \rightarrow \Xop^{-1}a$.
+			If $i \ne 2$, $b$ does not hold and the implication is trivially satisfied.
+			If $i = 2$, we have $\pi \vDash_{i-1} a$ and the formula is satisfied as well.
+		\item For all $i\ge 2$, $\pi \vDash_i (d \rightarrow \Xop^{-1} c) \Sop b$.
+			We need to give $0 \le j \le i$ with $\pi \vDash_j b$ and $\pi \vDash_k d \rightarrow \Xop^{-1} c$ for all $j < k \le i$.
+			Clearly, we can only give $j=2$.
+			Then for odd positions $k$, the implication $d \rightarrow \Xop^{-1} c$ holds trivially since $d$ does not hold.
+			For even positions $k$, it holds as well since $c$ holds at odd positions $n > 2$.
+		\qedhere
+	\end{itemize}
+\end{example}
+
 \erin
 Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well:
 \[
@@ -59,6 +76,7 @@ Given these definitions, it is possible to derive the formal semantics of the $\
 		\sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{0 \leq j \leq i}[\sigma \vDash_j \phi]
 	\end{matrix*}
 \]
+
 \camil
 The first follows from the rule for $\Sop$ and the fact that $\sigma \vDash_i \top$ for all $i\in\mathbb N$.
 The second follows from:
@@ -81,5 +99,25 @@ With this result we can also derive the semantics of the dual modalities $\lozen
 This is done in \cref{ex:dual-modalities}.
 
 The semantics over words extend to transition systems similar to the LTL case in Definition 5.7.
-The only difference is that $\vDash$ now is a ternary relation, and we use $\vDash$ as shorthand for $\vDash_0$.
+The only difference is that $\vDash$ now is a ternary relation, and we use $\pi\vDash\phi$ as a shorthand for $\pi\vDash_0\phi$.
+
+\begin{figure}[h]
+	\centering
+	\begin{tikzpicture}[initial text={},node distance=3cm,->]
+		\node[state,label=below:{$\{a,b\}$},initial] (s1) {$s_1$};
+		\node[state,label=below:{$\{a,b\}$},right of=s1] (s2) {$s_2$};
+		\node[state,label=below:{$\{a\}$},right of=s2,initial right] (s3) {$s_3$};
+		\draw (s1) edge[bend left] (s2);
+		\draw (s2) edge[bend left] (s1);
+		\draw (s2) -- (s3);
+		\draw (s3) edge[loop above,looseness=8,in=60,out=120] (s3);
+	\end{tikzpicture}
+	\caption{Example for semantics of PLTL.}
+	\label{fig:pltl:example-ts}
+\end{figure}
+
+\begin{example}[Satisfaction of PLTL Formulae by Transition Systems]
+	Consider again the transition system from Figure 5.3, reproduced as \cref{fig:pltl:example-ts}.
+	% TODO
+\end{example}
 \cbend
diff --git a/Assignment1/summary.tex b/Assignment1/summary.tex
index 31b65f8..ef9f458 100644
--- a/Assignment1/summary.tex
+++ b/Assignment1/summary.tex
@@ -1,6 +1,5 @@
 \camil
 \subsection{Summary}
-% TODO: points to be added to 5.3
 \emph{NB: these points are to be added to the current section 5.3.}
 \begin{itemize}
 	\item
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex
index 81a7d7f..5d2830a 100644
--- a/Assignment1/syntax.tex
+++ b/Assignment1/syntax.tex
@@ -95,7 +95,6 @@ we include an arrow that points to the state for which the formula holds.
 
 \begin{figure}
 	\tikzset{intuitive semantics/.style={shorten >=1pt,node distance=16mm,on grid,initial text={},baseline=-0.5ex,->}}
-	\tikzset{state/.append style={minimum size=15pt}}
 	\tikzset{arbitrary/.style={state,label={[font=\relsize{-2}]arbitrary}}}
 	\centering
 	\[\begin{array}{rcl}
@@ -200,6 +199,7 @@ Before turning to the formal semantics in the next subsection, we provide some e
 			\lozenge^{-1} (\phi_3 \land
 				\lozenge^{-1} (\phi_2 \land
 					\lozenge^{-1} \phi_1))\big)
+		\qedhere
 	\]
 \end{example}