summaryrefslogtreecommitdiff
path: root/Assignment1/equivalence.tex
blob: 6195afc01b9be3586f8f7763d8dd054906aecc94 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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