Модель Крипке (Bk;yl, Tjnhty)

Перейти к навигации Перейти к поиску

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

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

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

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

[править | править код]

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

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

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

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

Примечания

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