summaryrefslogtreecommitdiff
path: root/Assignment1/equivalence.tex
diff options
context:
space:
mode:
Diffstat (limited to 'Assignment1/equivalence.tex')
-rw-r--r--Assignment1/equivalence.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/Assignment1/equivalence.tex b/Assignment1/equivalence.tex
index 6373088..660f052 100644
--- a/Assignment1/equivalence.tex
+++ b/Assignment1/equivalence.tex
@@ -10,7 +10,7 @@ we can define equivalence on PLTL formulas.
Additionally, we can define another form of equivalence, initial equivalence.
When two formulas are initially equivalent, they are equivalent for all paths at position 0.
-This is mainly useful to compare PLTL and LTL formulas.
+This is among other things useful to compare PLTL and LTL formulas.
\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\]