How to deal with propositional First-Order-Logic Dynamic Logic formula

111 Views Asked by At

Let p be an atomic proposition, let a be an atomic program, and let $π = (K, M)$ be a Kripke frame with

$K = \{u, v, w\}$

$Mπ(p) = \{u, v\}$

$Mπ(a) = \{(u, v), (u, w), (v, w), (w, v)\}.$

The answer is:

In this structure, $u⊨$<$a$>$¬p∧$$p$, but $v⊨[a] ¬p$ and $w⊨[a] p$.

I don't understand the answer. Why?

1

There are 1 best solutions below

0
On

Your Kripke model is $M = (\{u,v,w\}, \{(u,v), (u,w). (v,w), (w,v)\}, \{u,v\})$. The first set are states in the model. The second one defines an accessibility relation (i.e. for each program (agent) a set of states that can be reached from the current one), and the last set is a valuation set for a propositional variable $p$ (i.e. where $p$ is true).

So, the first formula $(M,u) \models (\langle a \rangle \neg p) \wedge p$ (obviously, the brackets are not necessary) says that in the model $M$ there is a state $u$, such that there is an $a$-transition to a state where $p$ does not hold and $p$ is true in $u$. Since $(u,w) \in R (a)$, $w \notin V(p)$, and $v \in V(p)$ (that is, we can reach a state via $a$ from $u$ where $p$ is false, and $p$ is true in $u$), the formula holds.

The second formula $(M,v) \models[a] \neg p$ says that in the model $M$ there is a state $v$, such that for all $a$-transitions $p$ does not hold in destination states. Since $(v,w)$ and $w \notin V(p)$ (that is, there is only one state reachable from $v$, which is $w$, and there $p$ is false), the formula holds.

The last formula is vacuously true.