Linear temporal logic question

120 Views Asked by At

I am curious about what if we have this Kripke model

enter image description here

and I am trying determine the set of worlds where $\Box\Box p$ is satisfied

This is the part I am confused about when we have $\Box$ I am assuming it means for the next state or it is also for the initial starting place $a$

For example it would mean for this path $p$ -> $p, q$ is valid $\Box p$. This would be true if the other path wasnt false right? $p$ -> $r$ not valid.

The other question is when we have $\Box\Box p$ the initial state is not counted like this $p$ -> $r$$(\Box p)$ -> $p$$(\Box\Box p)$


This is how I think I would solve it and this are my thoughts on how I arrive at the conclusion. I have added an extra $\Box$ so everyone can see how I arrive at the conclusion to make it easier to correct me if I am wrong

enter image description here

1

There are 1 best solutions below

6
On BEST ANSWER

Let's take this step by step.

What is the set of worlds where $p$ is true? Answer: $\{a,b\}$.

We have three worlds, $a$, $b$, and $c$. In your diagram, the letters inside the circles are the propositions which are true at those worlds. So $p$ is true at $a$ and $b$, but not at $c$.

What is the set of worlds where $\square p$ is true? Answer: $\{c\}$.

$\square p$ is true at $w$ iff $p$ is true at every world accessible from $w$. And we determined that $p$ is true at $a$ and $b$. So $\square p$ is false at $a$ (since $c$ is accessible from $a$), $\square p$ is false at $b$ (since $c$ is accessible from $b$), and $\square p$ is true at $c$ (since the only world accessible from $c$ is $a$).

What is the set of worlds where $\square\square p$ is true? Answer: $\{b\}$.

$\square \square p$ is true at $w$ iff $\square p$ is true at every world accessible from $w$. And we determined that $\square p$ is only true at $c$. So $\square \square p$ is false at $a$ (since $b$ is accessible from $a$), $\square \square p$ is true at $b$ (since $c$ is the only world accessible from $b$), and $\square \square p$ is false at $c$ (since $a$ is accessible from $c$).