Модель Крипке

Модель Крипке (англ. Kripke structure) — это один из вариантов недетерминированного конечного автомата, который был предложен Солом Крипке. Этот вид НКА применяется при проверке моделей для представления поведения системы.

Модель Крипке является простой абстрактной машиной, позволяющей описать идеи вычислительной машины без добавления особых сложностей. Модель представляется ориентированным графом, вершины которого описывают достижимые состояния системы, а ребра — переходы из состояния в состояние.

Функция пометок сопоставляет каждой вершине множество свойств, которые выполняются в соответствующем состоянии.

Пусть ${\displaystyle AP}$ множество атомарных высказываний (булевых выражений над множеством переменных, констант и предикатных символов). Моделью Крипке^[1] назовем четверку ${\displaystyle M=(S,\;I,\;R,\;L)}$ состоящую из:

• конечного множества состояний ${\displaystyle S\;}$;
• множества начальных состояний ${\displaystyle I\subseteq S}$;
• отношения перехода ${\displaystyle R\subseteq S\!\times \!S\;}$, где ${\displaystyle \;\forall s\!\in \!S,\;\exists s^{'}\!\!\in \!S}$ такое, что ${\displaystyle (s,s^{'})\in R}$;
• функции пометок ${\displaystyle L:S\rightarrow 2^{AP}}$.

Условие накладываемое на отношение R утверждает, что каждое состояние имеет следующее. Если требуется эмулировать взаимную блокировку, в модель Крипке необходимо просто добавить ребро из состояния блокировки в себя.

Функция пометок L для каждого состояния s ∈ S определяет множество L(s) всех атомарных утверждений верных в s.

• Темпоральная логика
• Проверка моделей
• Семантика Крипке
• Линейная темпоральная логика