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
|
