0
$\begingroup$

Would anyone care to explain how can we deduce the Loop Invariance rule from the Reflexive Transitive Closure rule in PDL:

$$\frac{\psi\rightarrow (\phi\vee [\alpha]\psi)}{\psi\rightarrow [\alpha^*]\phi}$$? to: $$\frac{(\phi\vee\langle\alpha\rangle\psi)\rightarrow\psi}{\langle\alpha^*\rangle\phi\rightarrow\psi}$$

I've already deduced that $$\frac{(\phi\vee\langle\alpha\rangle\psi)\rightarrow\psi}{\langle\alpha^*\rangle\phi\rightarrow\psi}$$ is equivalent to $$ \frac{\psi \rightarrow [\alpha]\psi}{\psi \rightarrow [\alpha^*]\psi} \enspace, $$ if that helps.

Where $\alpha$ is a program, $\phi,\psi$ are formulas and $\langle\alpha\rangle$ is the diamond from PDL.

$\endgroup$
  • $\begingroup$ Is this what you are looking for? $\endgroup$ – Fabio Somenzi Feb 7 '17 at 21:32
  • $\begingroup$ I just noted that you asked the other question as well. The last rule you show is the loop invariance rule and $\psi$ is the invariant, while $\alpha$ is the loop body. $\endgroup$ – Fabio Somenzi Feb 7 '17 at 21:35
  • 1
    $\begingroup$ From the loop invariance rule alone, you cannot derive $\psi \rightarrow \psi$. However, if you assume $\psi \rightarrow \psi$ and $\psi \rightarrow [\alpha]\psi$, then the loop invariance rule allows you to conclude that $\psi \rightarrow [\alpha^*]\phi$. $\endgroup$ – Fabio Somenzi Feb 8 '17 at 0:46
  • 1
    $\begingroup$ Also note that the invariance rule is not equivalent to the dual of the reflexive transitive closure rule. Rather, it's a special case of it. $\endgroup$ – Fabio Somenzi Feb 8 '17 at 0:48
  • 1
    $\begingroup$ You are welcome. Actually, I mistyped in one of the comments above. I meant $\psi \rightarrow \phi$, not the tautologous $\psi \rightarrow \psi$. $\endgroup$ – Fabio Somenzi Feb 8 '17 at 2:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.