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

Question

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)?

Answer 1

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.