Would anyone care to explain how can we dualize the Reflexive Transitive Closure in PDL from : $$\frac{(\phi\vee\langle\alpha\rangle\psi)\rightarrow\psi}{\langle\alpha^*\rangle\phi\rightarrow\psi}$$ to: $$\frac{\psi\rightarrow (\phi\vee [\alpha]\psi)}{\psi\rightarrow [\alpha^*]\phi}$$?

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

  • $\begingroup$ Are you sure it's not $(\phi \wedge [\alpha]\psi)$? $\endgroup$ – Fabio Somenzi Jan 18 '17 at 23:32

$\def\<#1>{\langle#1\rangle}$We start from the relation between box and diamond:

$$ \<\alpha>p \equiv \neg [\alpha] \neg p \enspace. $$

Substitution in the reflexive transitive closure rule yields

$$ \frac{(\phi \vee \neg[\alpha]\neg \psi) \rightarrow \psi}{\neg[\alpha^*]\neg\phi \rightarrow \psi} \enspace. $$

Taking the contrapositive of both premise and conclusion,

$$ \frac{\neg \psi \rightarrow (\neg\phi \wedge [\alpha]\neg \psi)}{\neg\psi \rightarrow [\alpha^*]\neg\phi} \enspace. $$

We now rename, so that $\neg\phi$ is replaced by $\phi$ and $\neg\psi$ is replaced by $\psi$:

$$ \frac{\psi \rightarrow (\phi \wedge [\alpha]\psi)}{\psi \rightarrow [\alpha^*]\phi} \enspace. $$

Finally, if we wish to obtain the loop invariance rule, we substitute $\psi$ for $\phi$ and simplify:

$$ \frac{\psi \rightarrow [\alpha]\psi}{\psi \rightarrow [\alpha^*]\psi} \enspace, $$

having noted that $\psi \rightarrow (\psi \wedge [\alpha]\psi) \equiv \psi \rightarrow [\alpha]\psi$.


Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.