Computational tree logic satisfiability.

81 Views Asked by At

enter image description here

In the model I pasted above where $S_0$ and $S_1$ are starting states, is the $EXp$ formula satisfiable?

$$M,s\vDash EXp$$

Does it have to be satisfiable for all the starting states given the $M$, $s$? So to speak "There exists a next state in which the $p$ is satisfied" for both starting states or one of the states is enough, e.g. $S_0$ is satisfied while $S_1$ does not satisfy the formula. Is it the latter or the former?

1

There are 1 best solutions below

8
On

$M, s \vDash EXp$ does not make sense since $s$ is not a state in the model.

However, $M, S_0 \vDash EXp$ is the case. Why?

Let us review the semantics of the formula.

$EXp$ means that there should exist a path from $s_0$ s.t the successor of $s_0$ in the given path satisfies the formula $p$ which is only the case of $p$ is included in the set of atomic propositions in the successor state.

I.e $M, S_2 \vDash p$ and therefore $M, S_0 \vDash EXp$.

As one of the states satisfy the formula, it is satisfiable.

Refer to the semantics given here or wikipedia