Examples; definition of vDash

1 files changed, 69 insertions, 30 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 65b5bad..f10d767 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -6,10 +6,12 @@
 \usepackage{amsmath}
 \usepackage{amsthm}
 \usepackage{amssymb}
+\let\leq\leqslant
+\let\le\leqslant
 % See http://www.ams.org/faq?faq_id=212 for the trick to add qed at the end of
 % definitions and examples.
 \newtheoremstyle{mydefinition}%
-	{1em}{1em}% Style above and below
+	{2em}{2em}% Space above and below
 	{}% Body font
 	{}% Indent
 	{\bfseries}% Theorem head font
@@ -19,7 +21,7 @@
 \theoremstyle{mydefinition}
 \newtheorem{xdefinition}{Definition}
 \newtheoremstyle{myexample}%
-	{1em}{1em}% Style above and below
+	{2em}{2em}% Space above and below
 	{}% Body font
 	{}% Indent
 	{\itshape}% Theorem head font
@@ -39,8 +41,10 @@
 \usepackage{tikz}
 \usetikzlibrary{automata,positioning}
 \usepackage{relsize}
+\usepackage{parskip}
 \usepackage{cleveref}
 \crefname{figure}{Figure}{Figures}
+\renewcommand*{\arraystretch}{1.3}
 
 \DeclareMathOperator{\defeq}{\overset{\text{def}}{=}}
 \DeclareMathOperator{\Uop}{\mathbf{U}}
@@ -205,34 +209,76 @@ Thus, while with future modalities it is possible to look infinitely far in the
 %TODO: Give examples of semantics along the lines of subsection 5.1.1.
 Before turning to the formal semantics in the next subsection, we provide some examples.
 
-\begin{example}[Properties for an authentication system]
-	For instance, \citet{FiterauBrostean2017} use past modalities to describe properties of the Secure Shell (SSH) protocol.
+\begin{example}[Properties for a Traffic Light]
+	We return to the traffic light of Example 5.4.
+	Since dual past modalities are less useful than dual future modalities, we cannot express the liveness property $\square\lozenge\textsl{green}$ with a pure past formula.
+	However, the requirement \enquote{once red, the light cannot become green immediately} \emph{can} be expressed with past modalities.
+	To rewrite it, consider that this requirements is equivalent to \enquote{if green, the light cannot have been red previously}.
+	This yields the formula:
+	\[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\]
+\end{example}
+
+\begin{example}[Properties for an Authentication System]
+	\citet{FiterauBrostean2017} use past modalities to describe properties of the Secure Shell (SSH) protocol.
 	One property says that if a channel is opened, there must have been some successful authentication attempt in the past~\citep[p.~149]{FiterauBrostean2017}.
 	Also, since that successful authentication, no authentication failure must have occurred.
-	This formula is intuitively expressed by $\square(hasOpenedChannel \rightarrow \lnot authFailure \Sop authSuccess)$,
-		assuming $\Sop$ has \enquote{since} semantics.
+	This formula is intuitively expressed by $\square(\textsl{hasOpenedChannel} \rightarrow \lnot \textsl{authFailure} \Sop \textsl{authSuccess})$.
 	Expressing this property in LTL is obscure and tedious.
 	One way uses the Weak Until operator from Section 5.1.5:
 	%TODO please check that this is actually equivalent
 	\begin{align*}
-		& \lnot hasOpenedChannel \Wop\\
-		& \quad (authSuccess \land (\square authFailure \rightarrow \lnot hasOpenedChannel \Uop authSuccess))
+		& \lnot \textsl{hasOpenedChannel} \Wop\\
+		& \quad (\textsl{authSuccess} \land (\square \textsl{authFailure} \rightarrow \lnot \textsl{hasOpenedChannel} \Uop \textsl{authSuccess}))
 		\qedhere
 	\end{align*}
 \end{example}
 
 \subsection{Semantics}
 The semantics of LTL and PLTL are defined in a very similar way.
-We must make some modifications to the Definitions however (in particular to Definition 5.6 and 5.7).
+However, we must make some modifications to the definitions.
+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$.
+
 \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,0 \vDash \phi\}$$
-	where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics} and 5.2.
+	$$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}
+Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation.
+
+\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}
+
 \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 fragment $\pi$ of $TS$, the satisfaction relation is defined by
+		\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]$$
@@ -245,25 +291,11 @@ 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.
 
-\begin{figure}
-	\centering
-	\begin{mdframed}
-	$$
-		\begin{matrix*}[l]
-			\sigma,i &\vDash &\phi\Sop\psi &\text{iff} &\exists_{k \leq i}[\sigma,k \vDash \psi \wedge \forall_{k < j \leq i}[\sigma,j \vDash \phi]]\\
-			\sigma,i &\vDash &\Pop\phi &\text{iff} &i \geq 1 \wedge \sigma,i-1 \vDash \phi
-		\end{matrix*}
-	$$
-	\end{mdframed}
-	\caption{PLTL semantics for infinite words of $2^{AP}$}
-	\label{fig:PLTL-semantics}
-\end{figure}
-
 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,i &\vDash &\Fop^{-1}\phi &\text{iff} &\exists_{k \leq i}[\sigma,k \vDash \phi]\\
-		\sigma,i &\vDash &\Gop^{-1}\phi &\text{iff} &\forall_{k \leq i}[\sigma,k \vDash \phi]
+		\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*}
 $$
 
@@ -271,13 +303,13 @@ Now that we have defined the formal semantics of PLTL,
 we can define equivalence on PLTL formulas.
 \begin{definition}[Equivalence of PLTL Formulae]
 	PLTL formulae $\phi_1,\phi_2$ are equivalent, denoted $\phi_1 \equiv \phi_2$ iff they verify the following property:
-	\[\text{for any path } \pi \text{ and any position } i, \pi, i \vDash \phi \Leftrightarrow \pi, i \vDash \psi \qedhere\]
+	\[\text{for any path } \pi \text{ and any position } i, \pi \vDash_i \phi \Leftrightarrow \pi \vDash_i \psi \qedhere\]
 \end{definition}
 
 Additionally, we can define another form of equivalence, initial equivalence:
 \begin{definition}[Initial Equivalence of PLTL Formulae]
 	PLTL formulae $\phi_1,\phi_2$ are initial equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
-	\[\text{for any path } \pi, \pi, 0 \vDash \phi \Leftrightarrow \pi, 0 \vDash \psi \qedhere\]
+	\[\text{for any path } \pi, \pi \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\]
 \end{definition}
 
 \subsection{LTL and PLTL}
@@ -293,6 +325,13 @@ Additionally, we can define another form of equivalence, initial equivalence:
 \subsection{Minimal Bad Prefix in NuSMV}
 %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?
 
+\section{Summary}
+% TODO: points to be added to 5.3
+
+\section{Bibliographic Notes}
+% TODO: points to be added to 5.4
+% A possibly helpful list is at https://cstheory.stackexchange.com/a/29452
+
 \section{Contribution}
 %TODO: Like we are some immature group of children, we have to provide proof of contribution