diff options
Diffstat (limited to 'Assignment1')
| -rw-r--r-- | Assignment1/conversion.tex | 111 |
1 files changed, 102 insertions, 9 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 7635f05..607d030 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -91,6 +91,7 @@ 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 \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)\\ @@ -99,9 +100,9 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite \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*} - E_1 &= (q \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 &= q \Sop (\neg \beta \wedge \neg \alpha \wedge q \wedge (\neg \beta \wedge q \Sop a)) + E_1 &= (q \wedge \neg \beta) \Sop a \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\ + E_2 &= \neg \alpha \wedge \neg \beta \wedge (\neg \beta \wedge q) \Sop a\\ + 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$, @@ -145,7 +146,7 @@ The final step of the algorithm entails removing the parts of the formula that c \camil \begin{example}[Properties for an Authentication System] Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names: - $\square (c \rightarrow \lnot f \Sop s)$. + $\phi = \square (c \rightarrow \lnot f \Sop s)$. This can be rewritten to a form with only $\Uop$ and $\Sop$: \begin{align*} \square(c \rightarrow \lnot f \Sop s) @@ -157,12 +158,104 @@ The final step of the algorithm entails removing the parts of the formula that c \begin{align*} \lnot (\top \Uop (c \land \lnot(\lnot f \Sop s))) &\rightarrow \lnot (\top \Uop (c \land \lnot(s \lor \lnot f \land \lnot f \Sop s)))\\ - &\equiv \lnot (\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))) \\ - &\rightarrow \lnot ((c \land \lnot s \land f \land \lnot (\lnot f \Sop s)) \lor (\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))))\\ - &\equiv \lnot (c \land \lnot s \land f \land \lnot (\lnot f \Sop s)) \land \lnot(\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s)))\\ - &\equiv (\lnot c \lor s \lor \lnot f \Sop s) \land \lnot(\top \Uop (c \land \lnot s \land f \land \lnot (\lnot f \Sop s))). + &\equiv \lnot (\top \Uop (c \land \lnot s \land (f \lor \lnot (\lnot f \Sop s)))) \\ + &\equiv \lnot (\top \Uop (c \land \lnot s \land f) \lor \top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))) \\ + &\rightarrow \lnot \big( + [c \land \lnot s \land f] + \lor [\top \Uop (c \land \lnot s \land f)] + \\&\quad\qquad\lor [c \land \lnot s \land \lnot (\lnot f \Sop s)] + \lor [\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))]\big)\\ + &\equiv \lnot \big( + [c \land \lnot s \land (f \lor \lnot (\lnot \Sop s))] + \lor [\top \Uop (c \land \lnot s \land f)] + \\&\quad\qquad\lor [\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))]\big)\\ + &\equiv + \lnot [c \land \lnot s \land (f \lor \lnot (\lnot f \Sop s))] + \land \lnot [\top \Uop (c \land \lnot s \land f)] + \\&\quad\qquad\land \lnot [\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))]\\ + &\equiv + [\lnot c \lor s \lor (\lnot f \land \lnot f \Sop s)] + \land \lnot [\top \Uop (c \land \lnot s \land f)] + \\&\quad\qquad\land \lnot [\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))]\\ + \end{align*} + Only the subterm $\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))$ needs to be rewritten in step 2. + Rule 3 applies (with $\Sop$ and $\Uop$ swapped). + This gives: + \begin{align*} + \top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s)) + &\equiv + \lnot s \Uop (c \land \lnot s) \land \lnot s \land \lnot (\lnot f \Sop s) + \\&\qquad \lor f \land \lnot s \land \lnot s \Uop (c \land \lnot s) + \\&\qquad \lor \top \Uop (f \land \lnot s \land \lnot s \Uop (c \land \lnot s)) + \end{align*} + And hence our original formula is initially equivalent to: + \begin{alignat*}{3} + \phi \equiv_0\enspace + & &&[\lnot c \lor s \lor (\lnot f \land \lnot f \Sop s)] + \land \lnot [\top \Uop (c \land \lnot s \land f)]\\ + & &&\quad\land \lnot + \big[ + \lnot s \Uop (c \land \lnot s) \land \lnot s \land \lnot (\lnot f \Sop s) + \\& &&\qquad\qquad \lor f \land \lnot s \land \lnot s \Uop (c \land \lnot s) + \\& &&\qquad\qquad \lor \top \Uop (f \land \lnot s \land \lnot s \Uop (c \land \lnot s)) + \big] + \end{alignat*} + In step 3, we remove the pure past formulas from the boolean combination: + \begin{alignat*}{3} + \phi \equiv_0\enspace + & &&[\lnot c \lor s \lor \lnot f] + \land \lnot [\top \Uop (c \land \lnot s \land f)] + \\& &&\quad\land \lnot [\lnot s \Uop (c \land \lnot s) \land \lnot s] + \\& &&\quad\land \lnot [f \land \lnot s \land \lnot s \Uop (c \land \lnot s)] + \\& &&\quad\land \lnot [\top \Uop (f \land \lnot s \land \lnot s \Uop (c \land \lnot s))]\\ + \equiv_0\enspace + & &&[\lnot c \lor s \lor \lnot f] + \land \lnot [\top \Uop (c \land \lnot s \land f)] + \\& &&\quad\land [\lnot (\lnot s \Uop (c \land \lnot s)) \lor s] + \\& &&\quad\land [\lnot f \lor s \lor \lnot (\lnot s \Uop (c \land \lnot s))] + \\& &&\quad\land \lnot [\top \Uop (f \land \lnot s \land \lnot s \Uop (c \land \lnot s))] + \end{alignat*} + We can rewrite this back to our semantics of $\Uop$:% + \footnote{The first two terms (the first line of the original formula) are collapsed into one term. + This is because Gabbay's $\phi \land \lnot(\top \Uop \lnot\phi)$ is equivalent to our $\lnot (\top \Uop \lnot\phi)$ (and hence $\square\phi$). + The same can be done for the last two terms (the last two lines of the original formula). + The third term can be rewritten via $\Xop$: + $\lnot (\lnot \phi \Uop \psi) \lor \phi + \enspace\rightarrow\enspace \psi \lor \lnot\Xop (\lnot\psi \Uop \phi) + \enspace\equiv\enspace \lnot(\lnot \psi \land \Xop (\lnot \psi \Uop \phi)) + \enspace\equiv\enspace \lnot(\lnot\psi \Uop \phi)$.} + \begin{align*} + \dots &\rightarrow\enspace + \lnot [\top \Uop (c \land \lnot s \land f)] + \enspace\land\enspace \lnot (\lnot s \Uop (c \land \lnot s)) + \enspace\land\enspace \lnot [\top \Uop (f \land \lnot s \Uop (c \land \lnot s))]\\ + &\equiv\enspace + \square\lnot(c \land \lnot s \land f) + \enspace\land\enspace \lnot (\lnot s \Uop (c \land \lnot s)) + \enspace\land\enspace \square\lnot(f \land \lnot s \Uop (c \land \lnot s))\\ + &\equiv\enspace + \square\lnot(c \land \lnot s \land f) + \enspace\land\enspace \lnot \psi + \enspace\land\enspace \square\lnot(f \land \psi) + \quad \text{where $\psi = \lnot s \Uop (c \land \lnot s)$}\\ + &\equiv\footnotemark\enspace + \lnot \psi + \enspace\land\enspace \square\lnot(f \land \psi) \end{align*} - % TODO: step 2 and 3 on the right part (S nested in U) + \footnotetext{Because $\square\lnot(f \land \psi) \equiv \square\lnot(c \land \lnot s \land f)$.} + Consider again the semantics of $c$, $s$ and $f$: + if $c$, a connection is established. + $s$ indicates that authentication succeeded; $f$ that authentication failed. + Thus, $\psi$ means that a connection will be established without authentication success. + The two terms of the conjunction then mean: + \begin{itemize} + \item $\lnot\psi$. + A connection cannot be established without prior authentication success. + \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. \end{example} \erin |