Могут ли структуры Крипке иметь охранников?

Question

У меня есть простая структура крипке, где у меня есть 3 состояния со следующими переходами:

s1 --> s2
s2 --> s1
s1 --> s3
s3 --> s3

s1 является единственным начальным состоянием. Я не хочу, чтобы цикл от s1 до s2 повторялся больше, чем определенное количество (скажем, дважды). В других системах перехода я мог бы добавить охрану при переходе.

В1: Могут ли структуры Крипке иметь охрану на переходах?

Q2: Если да, как я могу смоделировать его в NuSmv?

Спасибо

Answer 1

Вы сравниваете яблоки и апельсины здесь. Модель со средствами защиты (например, в NuSMV) определяет пространство состояний, которое снова можно рассматривать как структуру Крипке (давайте здесь проигнорируем такие проблемы, как взаимоблокировки).

Охранники являются элементом подхода к моделированию, тогда как структура Крипке является основной теоретической концепцией, которая используется для описания пространства состояний.

Давайте рассмотрим пример: у нас есть модель с переменной v, которая может принимать два значения 1 и 2 с 1 в качестве начального значения, и два перехода с защитными элементами:

a == WHEN v=1 THEN v:=2
b == WHEN v=2 THEN v:=1

Результирующее пространство состояний будет:

[v=1] --> [v=2]
[v=2] --> [v=1]

На самом деле это структура Крипке (с [v=1] в качестве единственного начального состояния и без каких-либо меток, определенных на узлах), которая не содержит никаких охранников.

Обновление : Примером набора меток для каждого узла могут быть все логические выражения, которые оцениваются как истинные.

Подводя итог этому для ваших двух вопросов:

1. Нет, в самих структурах Крипке нет стражи.
2. Тем не менее (как объяснено, никакие охранники в структурах Крипке не означают, что в модели не должно быть охранников), я думаю, вы можете рассматривать условия в заявлении по делу как защиту для права действия толстой кишки. Или с TRANS у вас есть охранники, скрытые в выражении.