From dff0d9ab2507fac388784308099eafa2e225bff3 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Tue, 10 Apr 2018 15:19:29 +0200
Subject: Define equivalence for LTLP

---
 Assignment1/assignment1.tex | 13 +++++++++++++
 1 file changed, 13 insertions(+)

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
 
-- 
cgit v1.2.3