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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

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

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

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

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

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

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

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

См. также[править | править вики-текст]

  1. Темпоральная логика
  2. Проверка моделей
  3. Семантика Крипке
  4. Линейная темпоральная логика

Примечания[править | править вики-текст]

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

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