\erin
\subsubsection{Equivalence of PLTL Formulae}
Now that we have defined the formal semantics of PLTL,
we can define equivalence on PLTL formulas.

\begin{definition}[Equivalence of PLTL Formulae]
	PLTL formulae $\phi_1,\phi_2$ are equivalent, denoted $\phi_1 \equiv \phi_2$ iff they satisfy the following property:
	\[\text{for any path } \pi \text{ and position } i \ge 0, \pi \vDash_i \phi \text{ if and only if } \pi \vDash_i \psi \qedhere\]
\end{definition}

Additionally, we can define a weaker form of equivalence: initial equivalence.
When two formulas are initially equivalent, they are equivalent for all paths at position 0.
This is among other things useful to compare PLTL and LTL formulas.
\begin{definition}[Initial Equivalence of (P)LTL Formulae]
	(P)LTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they satisfy the following property:
	\[\text{for any path } \pi, \pi \vDash_0 \phi \text{ if and only if } \pi \vDash_0 \psi \qedhere\]
\end{definition}

\camil
Naturally, the PLTL version of an LTL formula is initially equivalent to the original LTL formula.
This follows from a comparison of Figure 5.2 and \cref{fig:PLTL-semantics} (taking $i=0$).

\begin{example}[Equivalence of PLTL and LTL Formulae]
	Clearly, we have $\phi \equiv \Xop\Xop^{-1}\phi$ for all $\phi$.
	Because $\pi \vDash_i \Xop\psi$ iff $\pi \vDash_{i+1} \psi$, the special case for $\Xop^{-1}$ when $i=0$ never occurs.
	However, one must be careful with $\Xop^{-1}$ in other contexts.
	For instance, $\square\phi \not\equiv_0 \square\Xop^{-1}\phi$ (and hence $\square\phi \not\equiv \square\Xop^{-1}\phi$), because $\Xop^{-1}\phi$ never holds at position 0.
	On the other hand, $\lozenge\phi \equiv \lozenge\Xop^{-1}\phi$.
	If $\lozenge\phi$ for some path, there is a position $i$ at which $\phi$ holds.
	Hence, at $i+1 > 0$, $\Xop^{-1}\phi$ holds.
	Conversely, if $\lozenge\Xop^{-1}\phi$, there is an $i$ at which $\phi$ holds.
	By the semantics of $\Xop^{-1}$, $i>0$, and hence we can take $i-1$ to show that $\lozenge\phi$.

	As for $\Sop$, we e.g. have $\square(\phi \Sop \psi) \equiv_0 \psi \land \square(\phi \lor \psi)$.
	If $\phi \Sop \psi$ holds at position 0, $\psi$ must hold at position 0.
	Furthermore, if at some point $\phi \lor \psi$ does not hold, at that position $\phi \Sop \psi$ does not hold either.
	Conversely, if the right formula holds, at any position there is a $\phi$-path back to a position at which $\psi$ held, and hence the left formula holds.
	However, the two formulas are only initially equivalent.
	For instance, $\pi = ab^\omega$ satisfies $\square(b \Sop a)$ but not $a \land \square(b \lor a)$ at position 1.
\end{example}
\cbend