Структура Крипке (проверка модели) - Kripke structure (model checking)

В этой статье описываются структуры Крипке, используемые при проверке модели. Для более общего описания см. Семантику Крипке .

Структура Крипке является изменение системы перехода , первоначально предложенный Saul Крипке , используемой в модели проверки , чтобы представить поведение системы. Он состоит из графа , узлы которого представляют достижимые состояния системы, а ребра представляют переходы между состояниями, вместе с функцией маркировки, которая сопоставляет каждый узел с набором свойств, которые сохраняются в соответствующем состоянии. Временная логика традиционно интерпретируется в терминах структур Крипке.

Формальное определение

Пусть AP некоторое множество атомарных предложений , т.е. логические выражения над переменными, константами и предикатных символов. Кларк и др. определим структуру Крипке над AP как 4-кортеж M = ( S , I , R , L ), состоящий из

  • конечное множество состояний S .
  • множество начальных состояний I ⊆ S .
  • переход отношение R ⊆ S × S таким образом, что R является левой общей , т.е. ∀s ∈ S ∃s' ∈ S такие , что (S, S') ∈ R .
  • функция разметки (или интерпретации ) L : S → 2 AP .

Поскольку R является тотальным слева , всегда можно построить бесконечный путь через структуру Крипке. Состояние тупика может быть смоделировано одним исходящим ребром, возвращающимся к самому себе. Функция разметки L определяет для каждого состояния s ∈ S множество L ( s ) всех атомарных предложений, которые действительны в s .

Путь от структуры М представляет собой последовательность состояний р = с 1 , с 2 , с 3 , ... таким образом, что для каждого I> 0 , R (S I , S + 1 ) имеет место. Слово на пути р представляет собой последовательность наборов атомных положений , ш = L (s 1 ), L (s 2 ), L (s 3 ), ... , который является ω-слово в алфавите 2 AP .

С помощью этого определения структура Крипке (скажем, имеющая только одно начальное состояние i ∈ I ) может быть отождествлена ​​с машиной Мура с одноэлементным входным алфавитом, а функция вывода является ее функцией маркировки.

Пример

Пример структуры Крипке

Пусть множество атомарных предложений AP = {p, q} . p и q могут моделировать произвольные логические свойства системы, которую моделирует структура Крипке.

На рисунке справа показана структура Крипке M = ( S , I , R , L ) , где

  • S = {s 1 , s 2 , s 3 } .
  • I = {s 1 } .
  • R = {(s 1 , s 2 ), (s 2 , s 1 ) (s 2 , s 3 ), (s 3 , s 3 )} .
  • L = {(s 1 , {p, q}), (s 2 , {q}), (s 3 , {p})} .

M может создать путь ρ = s 1 , s 2 , s 1 , s 2 , s 3 , s 3 , s 3 , ... и w = {p, q}, {q}, {p, q}, {q}, {p}, {p}, {p}, ... - слово выполнения на пути ρ . M может создавать слова исполнения, принадлежащие языку ({p, q} {q}) * ({p}) ω ∪ ({p, q} {q}) ω .

Отношение к другим понятиям

Хотя эта терминология широко распространена в сообществе специалистов по проверке моделей, некоторые учебники по проверке моделей не определяют «структуру Крипке» в таком расширенном виде (или вообще не определяют), а просто используют концепцию (помеченной) переходной системы , которая дополнительно имеет набор действий Act , а отношение перехода определяется как подмножество S × Act × S , которое они дополнительно расширяют, чтобы включить набор атомарных предложений и функцию разметки для состояний ( L, как определено выше). В этом подходе бинарное отношение, полученное путем абстрагирования от меток действий, называется графом состояний .

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

Смотрите также

Рекомендации