Как сравнить два LTL?

Question

Как сравнить два LTL, чтобы увидеть, можно ли противоречить друг другу? Я спрашиваю об этом, потому что у меня есть иерархическая машина состояний и LTL, описывающая поведение в каждом состоянии. Мне нужно знать, может ли локальная LTL противоречить глобальной LTL. Я видел в статье «Спецификация функций и автоматическое обнаружение конфликтов», что два свойства LTLs f и g противоречивы, если L (f) пересечение L (g) пусто. И это точно вопрос проверки модели с f как программой и ¬g как свойство. Кто-нибудь может мне с этим помочь? Как преобразовать LTL f в программу в SPIN/Promela?

Спасибо.

Answer 1

Следующие работы для меня. (Предупреждение: я не видел этого в официальной документации. Это может означать, что есть другие, более эффективные способы сделать это. Или что я не выглядел достаточно сложно.)

Мы хотим проверить, подразумевает ли [] <> p && [] <> q<> (p && q) , (Это не так.)

Напишите тривиальный процесс P, который может выполнять все переходы и написать заявку как свойство LTL A.

bool p; bool q; 

active proctype P() { 
    do :: d_step { p = false; q = false } 
    :: d_step { p = false; q = true } 
    :: d_step { p = true; q = false } 
    :: d_step { p = true; q = true } 
    od 
} 

ltl A { (([] <> p) && ([] <> q)) -> <> (p && q) } 

(EDIT 1-ноября-2016: это может быть неправильным, потому что мы могли бы быть пропущены некоторые переходы из-за скрытого начального состояния, см how to make a non-initialised variable in Spin?)

Затем поместите это в файл check.pml и

spin -a check.pml 
cc  pan.c -o pan 
./pan -a -n 
./pan -r check.pml.trail -v 

показана модель отрицания претензии (в конечном счете, периодический след, где p и q являются истинными бесконечно часто, но p && q никогда не бывает).

Двойная проверка: измените вывод в претензии на <> (p || q), тогда нет встречного экзамена, доказывающего, что импликация действительна.

В вашем случае иск составляет ! (f && g) (они никогда не должны быть истинными одновременно).

Возможно, существует какой-то умный способ сделать код для тривиального процесса меньше.

Кроме того, третья команда на самом деле ./pan -a -i -n (-i, чтобы найти кратчайший пример), но она дает предупреждение. И он находит более короткий цикл.