Formal semantics of LTLP

1 files changed, 37 insertions, 1 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 4875752..842047c 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -5,7 +5,10 @@
 
 \usepackage{amsmath}
 \usepackage{amsthm}
+\usepackage{amssymb}
 \newtheorem{definition}{Definition}
+\usepackage{mathtools}
+\usepackage{mdframed}
 \usepackage{tikz}
 \usetikzlibrary{automata,positioning}
 
@@ -44,7 +47,7 @@ Markey achieves this proof by providing an formula that is in exactly this class
 
 \subsection{Syntax and Semantics}
 % Provide formal syntax
-%TODO: Provide intuitive semantics
+% Provide intuitive semantics
 %TODO: Provide formal semantics
 This subsection describes the syntax and semantics of LTLP.
 Given that LTLP is an extension of LTL, we are left with two options.
@@ -53,6 +56,7 @@ This options is slightly more verbose, but does ensure that this subsection does
 The second option builds on the syntax and semantics that were already defined for LTL formulae.
 It is this option that we will use for this book, since it allows us to focus exclusively on the past modalities that are the focus of this section.
 
+\subsubsection{Syntax}
 \begin{definition}
 	LTLP formulae over the set $LTL$ of LTL formulae are formed according to the following grammar:
 	$$\phi ::= l \mid \phi_1 \Sop \phi_2 \mid \Xop^{-1} \phi$$
@@ -135,6 +139,38 @@ we include an arrow that points to the state for which the formula holds.
 	\label{fig:LTLP_intuitive}
 \end{figure}
 
+%TODO: Give examples of semantics along the lines of subsection 5.1.1.
+
+\subsubsection{Semantics}
+The semantics of LTL and LTLP are defined in a very similar way.
+In fact, we can use most definitions as defined in section 5.1.2 (in particular: Definition 5.6 and 5.7).
+In order to make these definitions suitable for use with our LTLP operators,
+we must provide their semantics.
+Figure~\ref{fig:LTLP-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 \phi \wedge \forall_{k < j \leq i}[\sigma,j \vDash \phi]]\\
+			\sigma,i &\vDash &\Xop^{-1}\phi &\text{iff} &i \geq 1 \wedge \sigma,i-1 \vDash \phi
+		\end{matrix*}
+	$$
+	\end{mdframed}
+	\caption{LTLP semantics for infinite words of $2^{AP}$}
+	\label{fig:LTLP-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]
+	\end{matrix*}
+$$
+
 \subsection{LTL and LTL-Past}
 %TODO: Consider/Analyse differences between LTL and LTL-Past