1 files changed, 16 insertions, 0 deletions
diff --git a/Assignment1/equivalence.tex b/Assignment1/equivalence.tex
new file mode 100644
index 0000000..6195afc
--- /dev/null
+++ b/Assignment1/equivalence.tex
@@ -0,0 +1,16 @@
+\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 verify the following property:
+	\[\text{for any path } \pi \text{ and any position } i, \pi \vDash_i \phi \Leftrightarrow \pi \vDash_i \psi \qedhere\]
+\end{definition}
+
+Additionally, we can define another form of equivalence, initial equivalence:
+\begin{definition}[Initial Equivalence of PLTL Formulae]
+	PLTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
+	\[\text{for any path } \pi, \pi \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\]
+\end{definition}
+\cbend