Как создать структуру крипки в NuSMV?

Question

Я должен создать структуру Крипке в NuSMV, и я должен проверить некоторые свойства.

Кто-нибудь поможет мне? Структура и свойства (LTL, CTL и CTL*) приведены на рисунках.

Здесь есть структура и свойства:

http://cl.ly/image/1x0b1v3E0P0D/Screen%20Shot%202014-10-16%20at%2016.52.34.png

Answer 1

Я нашел более простой и, казалось бы, более надежный код NuSMV для вашей структуры Kripke. Спасибо dejvuth за его ответ на мой вопрос. Код выглядит следующим образом

     MODULE main
     VAR
        state : {s0,s1,s2,s3,s4};
     ASSIGN
        init(state) := s0;
        next(state):=
             case
                 state = s0 : {s1,s2};
                 state = s1 : {s1,s2};
                 state = s2 : {s1,s2,s3};
                 state = s3 : {s1,s4};
                 state = s4 : {s4};
             esac;
     DEFINE
        p := state = s1 | state = s2 | state = s3 | state = s4;
        q := state = s1 | state = s2;
        r := state = s3;
     SPEC
       EG p;
     SPEC
       AG p;
     SPEC
       EF (AG p);

Answer 2

Насколько я знаю, NuSMV обрабатывает только формулы LTL и CTL (см. NuSMV в Википедии). Формулы в задаче 1-3 являются формулами CTL, поэтому NuSMV может проверить их на модели. Однако формулы в задачах 4 и 5 являются формулами CTL*, и поэтому мы не можем напрямую использовать их в качестве входных данных для NuSMV. Вы также должны понимать, что набор всех формул CTL* является правильным надмножеством объединения всех формул LTL и CTL. Это условие подразумевает, что некоторые формулы CTL* не имеют своих эквивалентных формул LTL или CTL (см. CTL* в Википедии). Вашу структуру Kripke можно определить в NuSMV с помощью следующего кода:

MODULE main

VAR
    p       : boolean;
    q       : boolean;
    r       : boolean;
    state   : {s0,s1,s2,s3,s4};

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

    init (p) := FALSE;
    init (q) := FALSE;
    init (r) := FALSE;

    next(p) :=
        case 
            state = s1 | state = s2 | state = s3 | state = s4       : TRUE;
            TRUE                                                    : p;
        esac;
    next(q) :=
        case
            state = s1 | state = s2                                 : TRUE;
            state = s3 | state = s4                                 : FALSE;
            TRUE                                                    : q;
        esac;
    next(r) :=
        case
            state = s3                                              : TRUE;
            state = s1 | state = s2 | state = s4                    : FALSE;
            TRUE                                                    : r;
        esac;
SPEC
    EG p;
SPEC
    AG p;
SPEC
    EF (AG p);

Конечно, есть другой способ определить структуру Крипке в NuSMV, но я думаю, что это один из самых простых способов. (В любом случае, спасибо за помощь в решении моей проблемы).

Что касается формул в задаче 4 и 5, вот мой ответ.

Формула AF [p U EG ( p -> q)] имеет форму AF [\phi], где \phi - формула LTL p U EG (p-> q). Поскольку формула LTL \phi удовлетворяется в модели Крипке, если для каждого пути, начинающегося с s0, мы удовлетворяем \phi, то мы переводим AF [p U EG ( p -> q)] в AF A[p U EG (р -> д)].

По тому же аргументу мы переводим EG[(( p & q) | r) U ( r U AG p)] в EG [A ((p & q) | r) UA (r U AG p)].