[FMFP] Finish basic summary

semester4/fmfp/parts/04_modelling/02_linear-temporal-logic/00_linear-time-properties.tex

@@ -1,4 +1,5 @@
 % TOOD: Some more intuition
+\newpage
 \subsection{Linear Temporal Logic}
 \subsubsection{Transition System of a Promela Model}
 For the transition systems, compared to earlier, we use a fixed initial configuration because we only model one program or system,
@@ -60,7 +61,42 @@ The set of all traces of $TS$ is $\cT(TS)$.
 The LT-Properties are typically specified over infinite sequences of abstract states, rather than over sequences of configurations.
 
 
-\subparagraph{Safety Properties}
+\paragraph{Safety Properties}
+\inlinedefinition An LT-property $P$ is a safety property if for all infinite sequences $t \in \cP(AP)^{\omega}$:
+if $t \notin P$ then there is a finite prefix $\hat{t}$ of $t$ such that for every $t'$ with prefix $\hat{t}$, $t \notin P$.
+
+\inlineintuition More informally, it \textit{does not allow anything bad to happen}. Or, more exhaustively, if a sequence $t$ is no allowed by the LT-property,
+then there exists a finite prefix $\hat{t}$, which contains everything that makes the sequence violate the LT-property.
+Thus, whatever sequence we append to it, it will always remain in violation of the property $P$.
 
 
-\subparagraph{Liveness Properties}
+\paragraph{Liveness Properties}
+\inlinedefinition An LT-property $P$ is a liveness property if every finite sequence $\hat{t} \in \cP(AP)^*$ is a prefix of an infinite sequence $t \in P$
+
+\inlineintuition More informally, it states that \textit{something good will happen eventually}.
+Or, more exhaustively, if every finite sequence of atomic propositions can be extended to a sequence that is allowed by the LT-property.
+
+
+\paragraph{On proves and examples}
+Some remarks for common exam multiple-choice questions
+\begin{itemize}
+    \item Safety Property and Liveness Property: Only \texttt{true} is such an example
+    \item Neither: There are no examples, since every LT-property is a conjunct of a safety and liveness property and every LT-property can be rewritten as such a conjunct.
+\end{itemize}
+
+Typically, the exam includes questions on whether or not a given LT-property $\varphi$ is a liveness property, safety property or a conjunct of both.
+To determine that, use the following flow chart:
+\begin{center}
+    \begin{tikzpicture}[node distance = 0.5cm and 0.5cm, >={Classical TikZ Rightarrow[width=7pt]}]
+        \node (start) {Is $\varphi$ safety property?};
+        \node (safety) [below left=of start] {Safety Property};
+        \node (isliveness) [below right=of start] {Is $\varphi$ a liveness property?};
+        \node (liveness) [below left=of isliveness] {Liveness Property};
+        \node (conjunct) [below right=of isliveness] {Conjunct};
+
+        \draw[arrows = ->, distance = 1.5pt] (start) -- node [above left] {\scriptsize Yes} (safety);
+        \draw[arrows = ->, distance = 1.5pt] (start) -- node [above right] {\scriptsize No} (isliveness);
+        \draw[arrows = ->, distance = 1.5pt] (isliveness) -- node [below right] {\scriptsize Yes} (liveness);
+        \draw[arrows = ->, distance = 1.5pt] (isliveness) -- node [below left] {\scriptsize No} (conjunct);
+    \end{tikzpicture}
+\end{center}

semester4/fmfp/parts/04_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex

@@ -0,0 +1,52 @@
+\subsubsection{Linear Temporal Logic}
+This is used to formalize LT-properties of traces.
+
+\paragraph{Operators}
+The basic operators are, with $p$ a proposition from $AP \neq \emptyset$ and $\Phi$ and $\Psi$ LTL formulas:
+\begin{itemize}
+    \item $p$ states that it is true ``\textit{now}''
+    \item $\Phi U \Psi$ states that $\Phi$ holds ``\textit{until}'' $\Psi$ holds. I.e. there are no other valid propositions that hold in between.
+    \item $\bigcirc \Phi$ states that the $\Phi$ holds for the ``\textit{next}''
+\end{itemize}
+
+
+\paragraph{Semantics}
+$t \models \Phi$ expresses that a trace $t \in \cP(AP)^\omega$ satisfies the LTL formula $\Phi$
+\begin{multicols}{2}
+    \begin{itemize}
+        \item $t \models p$ if and only if $p \in t_{[0]}$
+        \item $t \models \neg \Phi$ if and only if not $t \models \Phi$
+        \item $t \models \Phi \land \Psi$ if and only if $t \models \Phi$ and $t \models \Psi$
+        \item $t \models \Phi U \Psi$ if and only if there is a $k \geq 0$ with $t_{(\geq k)} \models \Psi$ and $t_{(\geq j)} \models \Phi$ for all $j$ with $0 \leq j \leq k$
+        \item $t \models \bigcirc \Phi$ if and only if $t_{(\geq 1)} \models \Phi$
+    \end{itemize}
+\end{multicols}
+
+
+\paragraph{Derived operators}
+There are a number of handy derived operators defined here that we can use, unless otherwise specified.
+\begin{itemize}
+    \item Eventually: $\Diamond \Phi \equiv (\texttt{true}\; U \Phi)$
+    \item Always (from now on): $\Square \Phi \equiv \neg \Diamond \neg \Phi$
+\end{itemize}
+
+Precedences are unary operators (such as $\Diamond \Phi \Rightarrow \Psi$ means $(\Diamond \Phi) \Rightarrow \Psi$), but we use parenthesis to avoid ambiguities.
+
+
+\newpage
+\paragraph{Useful patterns}
+\begin{itemize}
+    \item Strong invariant $\square \Psi$: $\Psi$ always holds and this is a safety property if $\Psi$ is a safety property.
+          For instance, a file is always open or closed ($\square(\texttt{open} \lor \texttt{closed})$)
+    \item Monotone invariant $\square(\Psi \Rightarrow \square \Psi)$: Once $\Psi$ is \texttt{true}, it will always be \texttt{true}.
+          It is a safety property if $\Psi$ is a safety property.
+          For instance, once information is public, it can never be private again ($\square(\texttt{public} \Rightarrow \square \texttt{public}$)
+    \item Establishing an invariant $\Diamond \square \Psi$: Eventually, $\Psi$ will \textit{always} hold. It is a liveness property if $\Psi$ is satisfiable.
+          For instance, system initialization starts server ($\Diamond \square \texttt{serverRunning}$)
+    \item Responsiveness $\square(\Psi \Rightarrow \Diamond \Phi)$: Every time that $\Psi$ holds, $\Phi$ will eventually hold.
+          It is a liveness property if $\Phi$ satisfiable.
+          For instance, all opened files must be closed eventually ($\square(\texttt{open} \Rightarrow \Diamond \texttt{closed})$)
+    \item Fairness $\square \Diamond \Psi$: $\Psi$ holds infinitely often.
+          It is a liveness property if $\Psi$ is satisfiable.
+          For instance, a producer does not wait infinitely long before entering the critical section ($\square \Diamond \texttt{critical}$)
+\end{itemize}