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

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

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

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

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

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

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

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