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

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

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

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

Пусть ${\displaystyle AP}$ множество атомарных высказываний (булевых выражений над множеством переменных, констант и предикатных символов). Моделью Крипке назовем четверку ${\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 .

См. также

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

Примечания