blob: 660f052d24beb44e13d26b9c5fdeb29504ed9686 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
\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.
When two formulas are initially equivalent, they are equivalent for all paths at position 0.
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\]
\end{definition}
\cbend
%TODO: examples
|
