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()
    state: {s0, s1, s2, s3};

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

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


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.


Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.