Модель Крипке (англ. Kripke structure) — это один из вариантов недетерминированного конечного автомата, который был предложен Солом Крипке. Этот вид НКА применяется при проверке моделей для представления поведения системы.
Модель Крипке является простой абстрактной машиной, позволяющей описать идеи вычислительной машины без добавления особых сложностей. Модель представляется ориентированным графом, вершины которого описывают достижимые состояния системы, а ребра — переходы из состояния в состояние.
Функция пометок сопоставляет каждой вершине множество свойств, которые выполняются в соответствующем состоянии.
Пусть множество атомарных высказываний (булевых выражений над множеством переменных, констант и предикатных символов). Моделью Крипке[1] назовем четверку состоящую из:
Условие накладываемое на отношение R утверждает, что каждое состояние имеет следующее. Если требуется эмулировать взаимную блокировку, в модель Крипке необходимо просто добавить ребро из состояния блокировки в себя.
Функция пометок L для каждого состояния s ∈ S определяет множество L(s) всех атомарных утверждений верных в s.
Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .