Define equivalence for LTLP

1 files changed, 13 insertions, 0 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 03b80d0..1e50572 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -186,6 +186,19 @@ $$
 	\end{matrix*}
 $$
 
+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}
+
 \subsection{LTL and LTL-Past}
 %TODO: Consider/Analyse differences between LTL and LTL-Past