\erin
\subsubsection{Semantics}
The semantics of LTL and PLTL are defined in a very similar way.
However, we must make some modifications to the definitions.
\camil
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$.

\erin
\begin{definition}[Semantics of PLTL (Interpretation over Words)]
	\label{def:pltl:semantics-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 \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}
\camil
Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation.
The difference with LTL formulae is well illustrated by the $\Xop$ operator.
In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\Xop\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$.
Thus, whether $\Xop\phi$ holds for $\sigma$ cannot depend on $A_0$.
In the PLTL case, $\sigma\vDash_i\Xop\phi$ iff $\sigma\vDash_{i+1}\phi$.
The information about $A_0$ is not lost, so whether $\Xop\phi$ holds for $\sigma$ may depend on $A_0$,
	as is trivially the case with $\Xop\Xop^{-1}a$.

\begin{figure}
	\centering
	\begin{mdframed}
	\[
		\begin{matrix*}[l]
			\sigma &\vDash_i & \top\\
			\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 & \Xop\phi          &\text{iff} & \sigma \vDash_{i+1} \phi\\
			\sigma &\vDash_i & \phi_1\Uop\phi_2  &\text{iff} & \exists_{j \ge i}\big[\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $i \le k < j$}\big]\\
			\sigma &\vDash_i & \phi_1\Sop\phi_2  &\text{iff} & \exists_{0 \le j \le i}\big[\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\big]\\
			\sigma &\vDash_i & \Pop\phi          &\text{iff} & \text{$i \geq 1$ and $\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{example}[Satisfaction of PLTL Formulae by Words]
	Let $\pi = aabcdcdcd\dots$ be an infinite path over $AP=\{a,b,c,d\}$, of which on every moment only one atomic proposition holds (i.e., at position 0, $a$ holds, at position 2, $b$ holds, etc.).
	We have for instance:

	\begin{itemize}
		\item For all $i\in\mathbb N$, $\pi \vDash_i b \rightarrow \Xop^{-1}a$.
			If $i \ne 2$, $b$ does not hold and the implication is trivially satisfied.
			If $i = 2$, we have $\pi \vDash_{i-1} a$ and the formula is satisfied as well.
		\item For all $i\ge 2$, $\pi \vDash_i (d \rightarrow \Xop^{-1} c) \Sop b$.
			We need to give $0 \le j \le i$ with $\pi \vDash_j b$ and $\pi \vDash_k d \rightarrow \Xop^{-1} c$ for all $j < k \le i$.
			Clearly, we can only give $j=2$.
			Then for odd positions $k$, the implication $d \rightarrow \Xop^{-1} c$ holds trivially since $d$ does not hold.
			For even positions $k$, it holds as well since $c$ holds at odd positions $n > 2$.
		\qedhere
	\end{itemize}
\end{example}

\erin
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 &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{0 \leq j \leq i}[\sigma \vDash_j \phi]\\
		\sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{0 \leq j \leq i}[\sigma \vDash_j \phi]
	\end{matrix*}
\]

\camil
The first follows from the rule for $\Sop$ and the fact that $\sigma \vDash_i \top$ for all $i\in\mathbb N$.
The second follows from:
\begin{align*}
	\sigma \vDash_i \square^{-1}\phi
	&\quad\Leftrightarrow\quad \sigma \vDash_i \lnot\lozenge^{-1}\lnot\phi\\
	&\quad\Leftrightarrow\quad \sigma \nvDash_i \lozenge^{-1}\lnot\phi\\
	&\quad\Leftrightarrow\quad \nexists_{0\le j\le i} [\sigma \vDash_j \lnot\phi]\\
	&\quad\Leftrightarrow\quad \forall_{0\le j\le i} [\sigma \vDash_j \phi].
\end{align*}

With this result we can also derive the semantics of the dual modalities $\lozenge^{-1}\square^{-1}$ and $\square^{-1}\lozenge^{-1}$:
\[
	\sigma \vDash_i \lozenge^{-1}\square^{-1}\phi
	\quad\Leftrightarrow\quad
	\sigma \vDash_i \square^{-1}\lozenge^{-1}\phi
	\quad\Leftrightarrow\quad
	\sigma \vDash_0 \phi
\]
This is done in \cref{ex:dual-modalities}.

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 $\pi\vDash\phi$ as a shorthand for $\pi\vDash_0\phi$.

\begin{figure}[ht]
	\centering
	\begin{tikzpicture}[initial text={},node distance=3cm,->]
		\node[state,label=below:{$\{a,b\}$},initial] (s1) {$s_1$};
		\node[state,label=below:{$\{a,b\}$},right of=s1] (s2) {$s_2$};
		\node[state,label=below:{$\{a\}$},right of=s2,initial right] (s3) {$s_3$};
		\draw (s1) edge[bend left] (s2);
		\draw (s2) edge[bend left] (s1);
		\draw (s2) -- (s3);
		\draw (s3) edge[loop above,looseness=8,in=60,out=120] (s3);
	\end{tikzpicture}
	\caption{Example for semantics of PLTL.}
	\label{fig:pltl:example-ts}
\end{figure}

\begin{example}[Satisfaction of PLTL Formulae by Transition Systems]
	Consider again the transition system $TS$ from Figure 5.3, reproduced as \cref{fig:pltl:example-ts}.
	\begin{itemize}
		\item
			Recall that $TS \vDash \square a$.
			A noteworthy peculiarity is that $TS \nvDash \square\Xop^{-1}a$, since $\Xop^{-1}\phi$ is always false at position 0.
			Clearly, we do have $TS \vDash_i \square\Xop^{-1}a$ for $i \ge 1$.
		\item
			We also have $TS \vDash \square(b \rightarrow \square^{-1}b)$.
			After all, if $b$ does not hold, $b$ will never hold again.
		\item
			We have $s_1 \vDash \square(a \Sop b)$:
			since $a$ always holds, this is for $TS$ equivalent to $\square(\top \Sop b) \equiv \square(\lozenge^{-1}b)$, and $s_1 \vDash b$.
			However, since $s_2 \nvDash \square(a \Sop b)$ (because $a^\omega \nvDash \square(a \Sop b)$), also $TS \nvDash \square(a \Sop b)$.
		\qedhere
	\end{itemize}
\end{example}
\cbend