diff options
| -rw-r--r-- | Assignment1/equivalence.tex | 36 | ||||
| -rw-r--r-- | Assignment1/syntax.tex | 2 |
2 files changed, 30 insertions, 8 deletions
diff --git a/Assignment1/equivalence.tex b/Assignment1/equivalence.tex index 660f052..ad78c7b 100644 --- a/Assignment1/equivalence.tex +++ b/Assignment1/equivalence.tex @@ -4,16 +4,38 @@ 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\] + 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 another form of equivalence, initial equivalence. +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 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\] +\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 -%TODO: examples diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 6d86281..ac2e13c 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -167,7 +167,7 @@ Before turning to the formal semantics in the next subsection, we provide some e However, the requirement \enquote{once red, the light cannot become green immediately} \emph{can} be expressed with past modalities. To rewrite it, consider that this requirements is equivalent to \enquote{if green, the light cannot have been red previously}. This yields the formula: - \[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\] + \[\square(\textsl{green} \rightarrow \lnot \Pop\textsl{red}) \qedhere\] \end{example} \begin{example}[A property for an Authentication System] |