diff options
author | Erin van der Veen | 2018-04-19 09:51:08 +0200 |
---|---|---|
committer | Erin van der Veen | 2018-04-19 09:51:08 +0200 |
commit | cef8271999ce007abe7be1d0190f8c01ff6fd993 (patch) | |
tree | c732f15530006b75b2182b515fa2da6c4e64d10c /Assignment1/conversion.tex | |
parent | Safra's determinization algorithm (diff) | |
parent | Example: protocol dependencies (diff) |
Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 89 |
1 files changed, 63 insertions, 26 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 5fdc04f..1221952 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -7,6 +7,7 @@ The second algorithm makes use of the translation of PLTL formulas to automata a This algorithm is described in more detail below. \paragraph{Syntactic Algorithm} +\label{pltl:to-ltl:syntactic} The syntactic algorithm as proposed by Gabbay has its foundation in the following three facts:% \footnote{% Note that Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators. @@ -90,13 +91,13 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite \erin \begin{enumerate}[resume] - \item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where: - % TODO Verify all except 3 + \item Suppose $E = (q \lor \alpha\Uop\beta) \Sop a$, then $E \equiv E_1 \vee E_2 \vee E_3$ where: \begin{align*} - E_1 &= (a \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\ - E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\ - E_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a) + E_1 &= \bot \Sop a\\ + E_2 &= (\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a\\ + E_3 &= \neg(\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a \land (\neg a \land \neg\beta) \Sop (\neg q \land \neg a) \end{align*} + where $c = (\neg a \land \neg\beta) \Sop (\neg q \land \neg a) \land \neg\alpha \land \neg\beta$. \item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where: \begin{align*} @@ -105,46 +106,58 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite E_3 &= q \Sop (\neg \alpha \wedge \neg \beta \wedge q \wedge (\neg \beta \wedge q) \Sop a) \end{align*} - \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$, then $E \equiv \neg (\neg a \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a) \wedge \Fop^{-1} a$, + \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$, + then $E \equiv \neg (\neg a \Sop (\neg q \wedge (\alpha \Uop \beta) \wedge \neg a)) \wedge \Fop^{-1} a$, which can be reduced via rule 1. - \item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee (E_2 \wedge E_3)$ where: + \item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \lor E_2 \lor E_3$ where: \begin{align*} - E_1 &= (\alpha \Sop a) \wedge (\beta \vee (\alpha \wedge (\alpha \Uop \beta)))\\ - E_2 &= (\beta \vee \alpha \vee \neg(\neg\beta \Sop \neg q) \Sop \beta \wedge (\alpha \Sop a))\\ - E_3 &= (\beta \vee (\alpha \wedge (\alpha \Uop \beta))) \vee \neg (\neg\beta \Sop \neg q) + E_1 &= \alpha \Sop a \wedge (\beta \vee \alpha \wedge \alpha \Uop \beta)\\ + E_2 &= \beta \lor \alpha \land \alpha\Uop\beta \land \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a)\\ + E_3 &= \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a) \land (\beta \vee \alpha \wedge \alpha \Uop \beta) \land \neg (\neg\beta \Sop \neg q) \end{align*} \item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \neg(\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where: \begin{align*} - E_1 &= (\neg \beta \wedge q \Sop a) \wedge \neg \beta \wedge \neg \alpha\\ - E_2 &= q \vee (\alpha \Uop \beta) \Sop \neg \beta \wedge \neg \alpha \wedge (q \vee (\alpha \Uop \beta)) \wedge (\neg \beta \wedge q \Sop a)\\ - E_3 &= (q \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta) + E_1 &= ((\neg \beta \wedge q) \Sop a) \wedge \neg \alpha \wedge \neg \beta\\ + E_2 &= [q \vee \alpha \Uop \beta] \Sop [\neg \alpha \wedge \neg \beta \wedge (q \vee \alpha \Uop \beta) \wedge (\neg \beta \wedge q) \Sop a]\\ + E_3 &= (q \wedge \neg \beta) \Sop a \wedge \neg \beta \wedge \neg (\alpha \Uop \beta) \end{align*} + $E_2$ has a $\Uop$ in a $\Sop$, but can be further rewritten using elimination 5. \item Suppose $E = (q \vee \neg(\alpha \Uop \beta)) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2$ where: \begin{align*} - E_1 &= (q \vee \neg (\alpha \Uop \beta) \Sop \beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q \Sop a))\\ - E_2 &= (\alpha \wedge q \Sop a) \wedge \alpha \wedge (\alpha \Uop \beta) + E_1 &= [q \vee \neg (\alpha \Uop \beta)] \Sop [\beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q) \Sop a]\\ + E_2 &= (\alpha \wedge q) \Sop a \wedge \alpha \wedge \alpha \Uop \beta \end{align*} $E_1$ can be further reduced using eliminations 8 and 4. - \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ where: + + \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg (E_1 \vee E_2 \vee E_3)$ where: \begin{align*} - E_1 &= \neg a \vee \neg (\alpha \Uop \beta)\\ - E_2 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a\\ - E_3 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta) + E_1 &= \square^{-1} (\neg a \vee \alpha \Uop \beta)\\ + E_2 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta \wedge \neg a)\\ + E_3 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta) \end{align*} - After elimination of $\Gop^{-1}$, this formula can be further eliminated, in particular using elimination 5. + \camil + Since $\sigma \vDash_i E_2$ entails $\sigma \vDash_i E_3$ for all $i\in\mathbb N$, we also have $E \equiv \neg(E_1 \lor E_3)$.\cbend% + \footnote{\cbcolor{red}\cbstart + According to \citet[p.~439]{Gabbay1989}, $E_3$ is \enquote{subsumed by} $E_2$. + Assuming the straightforward understanding of subsumption ($\phi$ subsumes $\psi$ if and only if $\textsl{Words}(\phi) \supseteq \textsl{Words}(\psi)$), this is incorrect and $E_2$ is subsumed by $E_3$ instead.\cbend} + The term\erin\ $E_3$ (and $E_2$) can be further eliminated, in particular using elimination 5. + \cbend{} \end{enumerate} +\erin Note that these rules can only be applied when a $\Uop$ is within the scope of a $\Sop$. -In order to move the $\Sop$ out of the scope of the $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical. -These equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$. +In order to move an $\Sop$ out of the scope of a $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical. +The above equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$. -The final step of the algorithm entails removing the parts of the formula that contains the $\Sop$-operators. +The final step of the algorithm entails removing the pure past formulas from the boolean combination. +After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's definitions) these formulas can only say things about exclusive past time. \camil -\begin{example}[Properties for an Authentication System] +\begin{example}[A property for an Authentication System] + \label{ex:pltl-to-ltl:authentication} Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names: $\phi = \square (c \rightarrow \lnot f \Sop s)$. This can be rewritten to a form with only $\Uop$ and $\Sop$: @@ -254,8 +267,31 @@ The final step of the algorithm entails removing the parts of the formula that c \item $\square\lnot(f \land \psi)$. After an authentication failure, a connection cannot be established without prior authentication success. \end{itemize} - We see that the formula is reasonably succinct compared to its PLTL version, $\square(c \rightarrow \lnot f \Sop s)$. - Using past modalities was not needed in this case. + The resulting LTL formula is reasonably succinct, but is clear that the PLTL formula is easier to construct and understand. + + Note that we have not proven that no smaller LTL formula exists. + For an example of such a proof, see \cref{ex:succinctness}. +\end{example} + +\begin{example}[Protocol Dependencies] + In \cref{ex:pltl:protocol-dependencies}, we considered the PLTL formula + $\square \big(\psi \rightarrow + \lozenge^{-1} (\phi_3 \land + \lozenge^{-1} (\phi_2 \land + \lozenge^{-1} \phi_1))\big)$. + By the definitions of $\square$ and $\lozenge^{-1}$, it is equivalent to + \[ + \lnot\big( + \top \Uop ( + \psi \land \lnot ( + \top \Sop ( + \phi_3 \land \top \Sop (\phi_2 \land \top \Sop \phi_1) + )))\big). + \] + No other temporal operators besides $\Uop$ and $\Sop$ are used, so to transform it to an initially equivalent LTL formula step 1 is not needed. + + Rewriting the formula to Gabbay's definitions and separating the pure past formulas in step 2 proceeds as in the previous example. + The exact steps are not shown here for reasons of brevity. \end{example} \erin @@ -338,6 +374,7 @@ Let us first define the Muller Automaton: Converting a NBA to a Muller automaton was shown to be possible by R. McNaughton~\cite{McNaughton1966} and is part of what is known as McNaughton's theorem. +<<<<<<< HEAD There are multiple ways to convert a NBA to a Muller Automaton. In this book we will describe Safra's Determinization Algorithm. |