diff options
Diffstat (limited to 'Assignment1/equivalence.tex')
| -rw-r--r-- | Assignment1/equivalence.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Assignment1/equivalence.tex b/Assignment1/equivalence.tex index 6195afc..6373088 100644 --- a/Assignment1/equivalence.tex +++ b/Assignment1/equivalence.tex @@ -8,9 +8,12 @@ we can define equivalence on PLTL formulas. \[\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: +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. \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 +%TODO: examples |