+Now that we have defined the formal semantics of LTLP,

+we can define equivalence on LTLP formulas.

+\begin{definition}

+ LTLP formulae $\phi_1,\phi_2$ are equivalent, denoted $\phi_1 \equiv \phi_2$ iff they verify the following property:

+ $$\text{for any path } \pi \text{ and any position } i, \pi, i \vDash \phi \Leftrightarrow \pi, i \vDash \psi$$.

+\end{definition}

+

+Additionally, we can define another form of equivalence, initial equivalence:

+\begin{definition}

+ LTLP formulae $\phi_1,\phi_2$ are initial equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:

+ $$\text{for any path } \pi, \pi, 0 \vDash \phi \Leftrightarrow \pi, 0 \vDash \psi$$.

+\end{definition}

+