Модель Крипке (англ. Kripke structure) это недетерминированный конечный автомат, применяемый при проверке моделeй для представления поведения системы. Модель представляется ориентированным графом, вершины которого описывают достижимые состояния системы, а ребра - переходы из состояния в состояние. Функция пометок сопоставляет каждой вершине множество свойств, которые выполняются в соответствующем состоянии.

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

Пусть множество атомарных высказываний. моделью Крипке^[1] назовем четверку состоящую из:

• конечного множества состояний ;
• множества начальных состояний ;
• отношения перехода , где такое, что ;
• функции пометок .

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

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

Литература

1. ↑ Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: МЦНМО. 2002.