Интернет магазин китайских планшетных компьютеров



Компьютеры - Модель Крипке

23 января 2011





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

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

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

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

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

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



Просмотров: 644


<<< Машина Тьюринга
Охрана (программирование) >>>