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

Question

Is AG(~q ∨ Fp) Формула LTL удовлетворяет в модели ниже? Почему или почему нет?

модель?

Answer 1

В первую очередь это 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 is s.t. ~q FALSE, поэтому, чтобы удовлетворить ~q v F p, он должен обязательно придерживаться того, что F p имеет значение ИСТИНА, то есть обязательно, что рано или поздно p станет ИСТИННЫМ.
• Существует бесконечный путь, начинающийся с S2 s.t. p всегда ЛОЖНО: путь, который перескакивает от S2 до S0 и обратно и не касается ни S1, либо.
• Противоречие: LTL формула не устраивает.