1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
\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 satisfy the following property:
\[\text{for any path } \pi \text{ and position } i \ge 0, \pi \vDash_i \phi \text{ if and only if } \pi \vDash_i \psi \qedhere\]
\end{definition}
Additionally, we can define a weaker 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 (P)LTL Formulae]
(P)LTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they satisfy the following property:
\[\text{for any path } \pi, \pi \vDash_0 \phi \text{ if and only if } \pi \vDash_0 \psi \qedhere\]
\end{definition}
\camil
Naturally, the PLTL version of an LTL formula is initially equivalent to the original LTL formula.
This follows from a comparison of Figure 5.2 and \cref{fig:PLTL-semantics} (taking $i=0$).
\begin{example}[Equivalence of PLTL and LTL Formulae]
Clearly, we have $\phi \equiv \Xop\Xop^{-1}\phi$ for all $\phi$.
Because $\pi \vDash_i \Xop\psi$ iff $\pi \vDash_{i+1} \psi$, the special case for $\Xop^{-1}$ when $i=0$ never occurs.
However, one must be careful with $\Xop^{-1}$ in other contexts.
For instance, $\square\phi \not\equiv_0 \square\Xop^{-1}\phi$ (and hence $\square\phi \not\equiv \square\Xop^{-1}\phi$), because $\Xop^{-1}\phi$ never holds at position 0.
On the other hand, $\lozenge\phi \equiv \lozenge\Xop^{-1}\phi$.
If $\lozenge\phi$ for some path, there is a position $i$ at which $\phi$ holds.
Hence, at $i+1 > 0$, $\Xop^{-1}\phi$ holds.
Conversely, if $\lozenge\Xop^{-1}\phi$, there is an $i$ at which $\phi$ holds.
By the semantics of $\Xop^{-1}$, $i>0$, and hence we can take $i-1$ to show that $\lozenge\phi$.
As for $\Sop$, we e.g. have $\square(\phi \Sop \psi) \equiv_0 \psi \land \square(\phi \lor \psi)$.
If $\phi \Sop \psi$ holds at position 0, $\psi$ must hold at position 0.
Furthermore, if at some point $\phi \lor \psi$ does not hold, at that position $\phi \Sop \psi$ does not hold either.
Conversely, if the right formula holds, at any position there is a $\phi$-path back to a position at which $\psi$ held, and hence the left formula holds.
However, the two formulas are only initially equivalent.
For instance, $\pi = ab^\omega$ satisfies $\square(b \Sop a)$ but not $a \land \square(b \lor a)$ at position 1.
\end{example}
\cbend
|
