Структура Крипке (проверка модели)

В этой статье описываются структуры Крипке, используемые при проверке моделей. Более общее описание см. в разделе Семантика Крипке .

Структура Крипке — это вариант переходной системы , первоначально предложенной Солом Крипке . ^[1] используется при проверке модели ^[2] для представления поведения системы.Он состоит из графа, узлы которого представляют достижимые состояния системы, а ребра представляют переходы состояний, а также функции маркировки, которая сопоставляет каждый узел с набором свойств, которые сохраняются в соответствующем состоянии. Темпоральная логика традиционно интерпретируется в терминах структур Крипке. ^{[ нужна ссылка ]}

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

Пусть $AP$ — набор атомарных предложений , т.е. логических выражений, сформированных из переменных, констант и символов предикатов. Кларк и др. ^[3] определим структуру Крипке над $AP$ как набор из 4 $M = (S, I, R, L),$ состоящий из

конечное множество состояний $S$ .
набор начальных состояний $I \subseteq S$ .
отношение перехода $R \subseteq S \times S$ такое, что $R$ , тотально слева т. е. $\foralls \in S \existss' \in S$ такое, что $(s,s') \in R$ .
функция разметки (или интерпретации ) $L : S \to 2 АП$ .

Поскольку $R$ тотален слева , всегда можно построить бесконечный путь через структуру Крипке. Состояние тупика можно смоделировать с помощью одного исходящего ребра, возвращающегося к самому себе.Функция разметки $L$ определяет для каждого состояния $s \in S$ множество $L (s)$ всех атомарных предложений, которые действительны в $s$ .

Путь i структуры $M$ — это последовательность состояний $ρ = s 1, s 2, s 3, ...$ такая, что для каждого $0 выполняется$ > $R (s i, s i +1)$ . Слово — на пути $ρ$ это последовательность множеств атомарных высказываний $ш знак равно L (s 1), L (s 2), L (s 3), ...$ ,которое является ω-словом в алфавите $2 АП$ .

С помощью этого определения структура Крипке (скажем, имеющая только одно начальное состояние $i \in I)$ может быть отождествлена с машиной Мура с одноэлементным входным алфавитом, а выходная функция является ее функцией разметки. ^[4]

Пример

Пусть множество атомарных предложений $AP = {p, q}$ . $p$ и $q$ могут моделировать произвольные логические свойства системы, которыми является структура Крипке. моделирование.

Рисунок справа иллюстрирует структуру Крипке $M = (S, I, R, L)$ ,где

$S знак равно {s1, s2, s3}$ .
$я = {s 1}$ .
$р знак равно {(s 1, s 2), (s 2, s 1) (s 2, s 3), (s 3, s 3)}$ .
$L = {(s 1, {p, q}), (s 2, {q}), (s 3, {p})}$ .

$M$ может создать путь $ρ = s1, s2, s1, s2, s3, s3, s3, ...$ и $w = {p, q}, {q}, {p, q}, {q}, {p}, {p}, {p}, ...$ — слово выполнения по пути $ρ$ . $M$ может создавать исполняемые слова, принадлежащие языку $({p, q}{q})*({p}) ой \cup ({p, q}{q}) ой$ .

Отношение к другим понятиям

Хотя эта терминология широко распространена в сообществе по проверке моделей, некоторые учебники по проверке моделей не определяют «структуру Крипке» в таком расширенном смысле (или вообще вообще), а просто используют концепцию (помеченной) системы переходов , которая дополнительно имеет набор $действий Act$ , а отношение перехода определяется как подмножество $S \times Act \times S$ , которое они дополнительно расширяют, включив в него набор атомарных предложений и функцию маркировки для состояний ( $L$ , как определено выше). В этом подходе бинарное отношение, полученное путем абстрагирования меток действий, называется графом состояний . ^[5]

Кларк и др. переопределить структуру Крипке как набор переходов (вместо одного), что эквивалентно помеченным выше переходам, когда они определяют семантику модального μ-исчисления . ^[6]

См. также

Ссылки

^ Крипке, Саул, 1963, «Семантические соображения по модальной логике», Acta Philosophica Fennica, 16: 83-94
^ Кларк, Эдмунд М. (2008): Рождение проверки моделей. в: Грумберг, Орна и Вейт, ред. Хельмута: 25 лет проверки моделей, Vol. 5000: Конспекты лекций по информатике. Springer Berlin Heidelberg, с. 1-26.
^ Кларк, Эдмунд М. младший; Грумберг, Орна ; Пелед, Дорон (декабрь 1999 г.). Проверка модели . Серия «Киберфизические системы». МТИ Пресс. п. 14. ISBN 978-0-262-03270-4 .
^ Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы . Спрингер. п. 45. ИСБН 978-3-540-00296-3 .
^ Кристель Байер ; Йост-Питер Катоен (2008). Принципы проверки моделей . Массачусетский технологический институт Пресс. стр. 20–21 и 94–95. ISBN 978-0-262-02649-9 .
^ Кларк и др. п. 98

[1] Крипке, Саул, 1963, «Семантические соображения по модальной логике», Acta Philosophica Fennica, 16: 83-94

[2] Кларк, Эдмунд М. (2008): Рождение проверки моделей. в: Грумберг, Орна и Вейт, ред. Хельмута: 25 лет проверки моделей, Vol. 5000: Конспекты лекций по информатике. Springer Berlin Heidelberg, с. 1-26.

[Clarke1999-3] Кларк, Эдмунд М. младший; Грумберг, Орна ; Пелед, Дорон (декабрь 1999 г.). Проверка модели . Серия «Киберфизические системы». МТИ Пресс. п. 14. ISBN 978-0-262-03270-4 .

[Schneider2004-4] Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы . Спрингер. п. 45. ИСБН 978-3-540-00296-3 .

[BaierKatoen2008-5] Кристель Байер ; Йост-Питер Катоен (2008). Принципы проверки моделей . Массачусетский технологический институт Пресс. стр. 20–21 и 94–95. ISBN 978-0-262-02649-9 .

[6] Кларк и др. п. 98

[1]

[2]

[3]

[4]

[5]

[6]