Модель Крипке () — один из вариантов недетерминированного конечного автомата, применяющийся при проверке моделей для представления поведения параллельной системы. Предложен Солом Крипке.
Является простой абстрактной машиной, позволяющей описать идеи вычислительной машины без добавления особых сложностей. Модель представляется ориентированным графом, вершины которого описывают достижимые состояния системы, а рёбра — переходы из состояния в состояние. Функция пометок сопоставляет каждой вершине множество свойств, которые выполняются в соответствующем состоянии.
Формально определяется для множества атомарных высказываний (булевых выражений над множеством переменных, констант и предикатных символов) как четвёрка , состоящая из: конечного множества состояний , множества начальных состояний , отношения перехода , такого, что для любого существует , что , функции пометок .
Накладываемое на отношение условие утверждает, что каждое состояние имеет следующее. Если требуется эмулировать взаимную блокировку, в модель Крипке добавляется ребро из состояния блокировки в себя. Функция пометок для каждого состояния определяет множество всех атомарных утверждений верных в .
Примечания
Категория:Математическая логика Категория:Формальные методы