# Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model

I have been learning Verification by model checking recently and I get the following question:

Is the CTL formula $$s_{0} \models EG\ AF\ p$$ valid in the following model?

I think it is incorrect because there is a deadlock or infinite loop about $$s_0$$ after the state is starting from $$s_0$$, which make it invalid under $$EG\ AF\$$ condition.

Am I correct? How can I prove it (or give a counterexample)?

You're correct. Another way to see would be to consider the de-morgan equivalent: $$\neg (AF~EG~\neg p)$$. To show this invalid, we can show its negation $$AF~EG~\neg p$$ is valid, which is easier: The formula $$AF~EG~\neg p$$ says on all paths starting at $$s_0$$, we eventually get to a state such that there is a path where $$\neg p$$ holds forever. And indeed that is true in the path $$s_0 \rightarrow s_0 \rightarrow\ldots~.$$ Since we established the negation, your original formula is invalid as you yourself concluded.

Thinking about CTL can be tricky. A good way is to always double-check using a CTL model checker, like the following:

MODULE main()
VAR
state: {s0, s1, s2, s3};

ASSIGN
init(state) := s0;
next(state) := case
state = s0: {s0, s1, s3};
state = s1: s2;
state = s2: s1;
state = s3: s2;
esac;

DEFINE
p := (state = s1) | (state = s3);
r := (state = s0) | (state = s1) | (state = s2);
q := (state = s2) | (state = s3);
t := (state = s1);

SPEC EG AF p;


Using nuSMV (http://nusmv.fbk.eu/), I get:

-- specification EG (AF p)  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
state = s0
t = FALSE
q = FALSE
r = TRUE
p = FALSE


Which is NuSMV's way of saying you can simply stay in the starting state and it would be a counter-example to your property.