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

Материал из Seo Wiki - Поисковая Оптимизация и Программирование

Перейти к: навигация, поиск

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

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

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

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

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

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

Литература

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

fr:Structure de Kripke ko:크립키 구조

Личные инструменты

Served in 0.050 secs.