PDL without converse operator -

52 Views Asked by At

I found this exercise (5.14) in the book "Dynamic Logic" by Harel, Kozen and Tiuryn. I have no clue how to construct the mentioned model in the exercise body.

Construct the Kripke model, such that the operator $<\alpha>$ is not continous.

In PDL with - (converse operator), the map $\phi \rightarrow <\alpha>\phi$ is continuous with respect to the order of logical implication. That is, if $K$ is a Kripke frame, $A$ a (finite or infinite) set of formulas, and $\phi$ a formula such that $m_K(\phi) = sup_{\psi \in A}m_K(\psi)$ then $sup_{\psi \in A}m_K(<\alpha>\psi)$ exists and is equal to $m_K(<\alpha>\phi)$.

We define $m_K(\psi)$ as a set of states in $K$ satisfying formula $\psi$.

If program $\alpha$ maps state $s_1$ to state $s_2$ then program $\alpha-$ ($\alpha$ with converse operator) maps $s_2$ to $s_1$.