diff options
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/semantics.tex | 18 |
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 |