Search code examples
model-checkingnusmv

satisfying the LTL formula in model

Is AG(~q ∨ Fp) LTL formula satisfy in model below? why or why not?

model?

Solution

  • First of all AG(~q ∨ Fp) is not an LTL formula, because the operator AG does not belong to LTL. I assume you meant G(~q v Fp).

    Modeling: let's encode the system in NuSMV:

    MODULE main ()
VAR
  state : { S0, S1, S2, S3 };
  p : boolean;
  q : boolean;

ASSIGN
  init(state) := S0;
  next(state) := case
    state = S0 : {S1, S2};
    state = S1 : {S0, S3};
    state = S2 : {S0};
    state = S3 : {S3};
  esac;

INVAR state = S0 <-> (!p & !q);
INVAR state = S1 <-> ( p &  q);
INVAR state = S2 <-> (!p &  q);
INVAR state = S3 <-> ( p & !q);


LTLSPEC G(!q | F p)

    And verify it:

    ~$ NuSMV -int
NuSMV > reset; read_model -i f.smv; go; check_property
-- specification  G (!q |  F p)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample 
Trace Type: Counterexample 
-- Loop starts here
-> State: 2.1 <-
  state = S0
  p = FALSE
  q = FALSE
-> State: 2.2 <-
  state = S2
  q = TRUE
-> State: 2.3 <-
  state = S0
  q = FALSE

    Explanation: So the LTL formula is not satisfied by the model. Why?

    • G means that the formula is satisfied only if ~q v F p is verified by every reachable state.
    • State S2 is s.t. ~q is FALSE, so in order to satisfy ~q v F p it must necessarily hold that F p is TRUE, that is it is necessarily the case that sooner or later p becomes TRUE.
    • There exists an infinite path starting from S2 s.t. p is always FALSE: the path that jumps from S2 to S0 and back and never touches either S1 or S3.
    • Contradiction: the LTL formula is not satisfied.