Структура Крипке (проверка модели)

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

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

Формальное определение [ править ]

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

конечное множество состояний $S$ .
множество начальных состояний $I \subseteq S$ .
переход отношение $R \subseteq S \times S$ таким образом, что $R$ является левой общей , т.е. $\foralls \in S \existss' \in S$ такие , что $(S, S') \in R$ .
функция разметки (или интерпретации ) $L : S \to 2 AP$ .

Поскольку $R$ является тотальным слева , всегда можно построить бесконечный путь через структуру Крипке. Состояние тупика можно смоделировать с помощью одного исходящего ребра, возвращаемого самому себе. Функция разметки $L$ определяет для каждого состояния $s \in 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 \in I)$ может быть отождествлена с машиной Мура с одноэлементным входным алфавитом, а функция вывода является ее функцией маркировки. ^[4]

Пример [ править ]

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

Пусть множество атомарных предложений $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}) ω \cup ({p, q} {q}) ω$ .

Отношение к другим понятиям [ править ]

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

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

См. Также [ править ]

Викискладе есть медиафайлы по теме моделей Крипке .

Ссылки [ править ]

↑ Крипке, Саул, 1963, «Семантические соображения по модальной логике», Acta Philosophica Fennica, 16: 83-94.
^ Кларк, Эдмунд М. (2008): Рождение проверки модели. в: Grumberg, Orna and Veith, Helmut eds .: 25 Years of Model Checking, Vol. 5000: Конспект лекций по информатике. Springer Berlin Heidelberg, стр. 1-26.
^ Кларк, Эдмунд М., младший; Грумберг, Орна; Пелед, Дорон (декабрь 1999 г.). Проверка модели . Серия киберфизических систем. MIT Press. п. 14. ISBN 9780262032704.
↑ Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы . Springer. п. 45. ISBN 978-3-540-00296-3.
^ Кристель Байер ; Йост-Питер Катоэн (2008). Принципы проверки моделей . MIT Press. стр. 20 -21 и 94-95. ISBN 978-0-262-02649-9.
^ Кларк и др. п. 98

[1] Крипке, Саул, 1963, «Семантические соображения по модальной логике», Acta Philosophica Fennica, 16: 83-94.

[2] Кларк, Эдмунд М. (2008): Рождение проверки модели. в: Grumberg, Orna and Veith, Helmut eds .: 25 Years of Model Checking, Vol. 5000: Конспект лекций по информатике. Springer Berlin Heidelberg, стр. 1-26.

[Clarke1999-3] Кларк, Эдмунд М., младший; Грумберг, Орна; Пелед, Дорон (декабрь 1999 г.). Проверка модели . Серия киберфизических систем. MIT Press. п. 14. ISBN 9780262032704.

[Schneider2004-4] Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы . Springer. п. 45. ISBN 978-3-540-00296-3.

[BaierKatoen2008-5] Кристель Байер ; Йост-Питер Катоэн (2008). Принципы проверки моделей . MIT Press. стр. 20 -21 и 94-95. ISBN 978-0-262-02649-9.

[6] Кларк и др. п. 98

[1]