dynamic logic: how to understand the truth value?

Question

how to understand the truth value of a dynamic logic formula? for example: $S = \{u_1,u_2,u_3,u_4\}$ is the set of four states $R(a) = \{(u_1,u_1), (u_2,u_1), (u_4,u_1)\}$ is after action a, like $u_2$ state will become $u_1$ $π(p) = {u_1,u_2}$ is when $p$ is true $π(q) = {u_1,u_4}$ is when $q$ is true

then how to understand the truth value of $[a]u_1$ ? Is it true since from $R(a)$ we can know that the only destination is $u_1$? how to understand $[a](p∧q)$ ? is it means after action a you will get two states? like $[a](u_1∧u_1) $ is true but $[a](u_1∧u_2)$ is false because action a would never bring about $u_2$?

Answer 1

$[a]u_1$ means that after action $a$ you will be in state $u_1$. $[a](p \land q)$ means that after $a$ you will get into some state that satisfies both the properties $p$ and $q$. So if $u_1$ and $u_2$ are distinct states, $u_1 \land u_2$ will be false so $[a](u_1 \land u_2)$ will be false regardless of how you define $R(a)$. With your definition of $R(a)$, $[a](u_1 \land u_1)$ will be true, but that is because $[a]u_1$ is true for your $R(a)$ and $u_1 \land u_1$ is equivalent to $u_1$. An assertion like $[a](\lnot u_2 \land \lnot u_3)$ is a bit more interesting: it is true for your $R(a)$ and for other possible definitions of $R(a)$ too.

Answer 2

Just to expand what Rob Arthan said above.

So, you have got the following Kripke model $M= (S, R, V)$:

• $S = \{u_1, u_2, u_3, u_4\}$,
• $R (a) = \{u_1 \xrightarrow {a} u_1, u_2 \xrightarrow {a} u_1, u_4 \xrightarrow {a} u_1\}$,
• $V(p) = \{u_1, u_2\}, V(q) = \{u_3, u_4\}$. (or $\pi$)

Semantics for the diamond operator is as follows:

$(M,u) \models [a]\varphi \text{ iff for all } v:(u,v) \in R(a) \text{ implies } (M,v) \models \varphi$.

In your case we have:

$(M, u_3) \models [a](p \wedge q) \text{ iff }$

$(M, u_3) \models [a]p \text{ and } (M, u_3) \models [a]q \text{ iff }$

$\text {for all } v:(u_3,v) \in R(a) \text{ implies } (M,v) \models p $, which is true (since $u_3$ is a dead-end world). The same holds for $q$.