Why is this formula valid in PDL

72 Views Asked by At

In the book modal logic for open minds by johan van benthem there is on page 161 a statement that the sentence $\langle (R\lor S)^* \rangle \phi$ is equivalent to the sentence $\langle (R^* ; S^*)^* \rangle \phi$
(* means iteration and ; means composition here)

So:
$\langle (R\lor S)^* \rangle \phi \equiv \langle (R^* ; S^*)^* \rangle \phi$

Why is this equivalent to each other?

1

There are 1 best solutions below

0
On BEST ANSWER

Suppose that for some arbitrary $M_w$ it holds that $M_w \models \langle (r \cup s)^\ast \rangle \varphi$. By the semantics this means that $\exists v \in W^M$ such that $M_{w,v} \models (r \cup s)^\ast$ and $M_v \models \varphi$. Now let us consider $M_{w,v} \models (r \cup s)^\ast$. According to the semantics, there is an $r \cup s$ path (which may be empty) between $w$ and $v$. Expression $r \cup s$ means that every step of the path may be either an $r$-step or an $s$-step. Examples of such paths are the empty path, $r$, $s,s$, $r,s,r,s,s,r$ and so on. Now we notice that the same paths can be described by the regular expression $(r^\ast;s^\ast)^\ast$. Moreover, we could construct automata for recognising $(r \cup s)^\ast$ and $(r^\ast;s^\ast)^\ast$, and see that they are equivalent. Therefore, we have that $M_{w,v} \models (r^\ast;s^\ast)^\ast$ and $M_v \models \varphi$, and hence $M_w \models \langle (r^\ast;s^\ast)^\ast \rangle \varphi$.