summaryrefslogtreecommitdiff
path: root/Assignment1
diff options
context:
space:
mode:
Diffstat (limited to 'Assignment1')
-rw-r--r--Assignment1/semantics.tex18
1 files changed, 2 insertions, 16 deletions
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex
index 791eb15..a48e163 100644
--- a/Assignment1/semantics.tex
+++ b/Assignment1/semantics.tex
@@ -79,20 +79,6 @@ With this result we can also derive the semantics of the dual modalities $\lozen
\]
This is done in \cref{ex:dual-modalities}.
-\erin
-\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 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]\]
- \item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
- \qedhere
- \end{itemize}
-\end{definition}
-In order to make these definitions suitable for use with our PLTL operators,
-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.
+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$.
\cbend