Definitions do change, change definitions

1 files changed, 16 insertions, 1 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 1994cf1..03b80d0 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -143,7 +143,22 @@ we include an arrow that points to the state for which the formula holds.
 
 \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).
+We must make some modifications to the Definitions however (in particular to Definition 5.6 and 5.7).
+\begin{definition}
+	Let $\phi$ be a LTLP formula over $AP$. The LT property induced by $\phi$ is
+	$$Words(\phi) = \{\sigma \in (2^{AP})^\omega \mid \sigma,0 \vDash \phi\}$$
+	where $\vDash \subseteq (2^{AP})^\omega \times LTLP$ is the smallest relation with the properties in Figure~\ref{fig:LTLP-semantics} and 5.2.
+\end{definition}
+\begin{definition}
+	Let $TS = (S, Act, \rightarrow, I, AP, L)$ be a transition system without terminal states, and let $\phi$ be an LTLP-formula over AP.
+\begin{itemize}
+	\item For infinite path fragment $\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]$$
+		\item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
+\end{itemize}
+\end{definition}
 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.