удовлетворяющие формуле LTL в модели

Прежде всего, AG(~q ∨ Fp) не является формулой LTL, потому что оператор AG не принадлежит LTL. Я предполагаю, что вы имели в виду G(~q v Fp).

Моделирование: закодируем систему в 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)

И проверьте это:

~$ 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

Объяснение. Таким образом, формула LTL не удовлетворяется моделью. Почему?

• G означает, что формула удовлетворяется, только если ~q v F p проверяется каждым достижимым состоянием.
• Состояние S2 является с.т. ~q является ЛОЖНЫМ, поэтому для того, чтобы удовлетворить ~q v F p, необходимо обязательно считать, что F p является ИСТИННЫМ, то есть это обязательно тот случай, когда p рано или поздно становится ИСТИННЫМ.
• Существует бесконечный путь, начинающийся с S2 ул. p всегда ЛОЖЬ: путь, который переходит от S2 к S0 и обратно и никогда не касается ни S1, ни S3.
• Противоречие: формула LTL не выполняется.