WikiDer > Справедливая вычислительная древовидная логика

Fair computational tree logic

Справедливая вычислительная древовидная логика обычный вычислительная древовидная логика изучено с явными ограничениями справедливости.

Слабая честность / справедливость

Это объявляет такие условия, что все процессы выполняются бесконечно часто. Если рассматривать процессы как P_я, тогда условие становится:

{displaystyle igwedge GFP_ {i}}

Сильная справедливость / сострадание

Здесь, если процесс запрашивает ресурс бесконечно часто (R), ему должно быть разрешено получать ресурс (C) бесконечно часто:

{displaystyle igwedge (GFRlongrightarrow GFC)}

Проверка модели на справедливый CTL

Если вы рассматриваете модель Крипке, справедливая модель Крипке имеет набор состояний F. Путь ${displaystyle pi = s_ {o}, s_ {1} dots}$ считается справедливым путем тогда и только тогда, когда путь включает в себя все члены F бесконечно часто.
Проверка модели честного CTL ограничивает проверки только справедливыми путями. Есть два вида:

1. M_ж, с_я | = А

{displaystyle phi}

если и только если

{displaystyle phi}

держится на ВСЕХ честных путях.

2. M_ж, с_я | = E

{displaystyle phi}

если и только если

{displaystyle phi}

держится на одном или нескольких честных путях.

Справедливое состояние - это такое состояние, из которого берет начало хотя бы один справедливый путь. Это переводится как M_ж, s | = EGtrue.

Подход на основе SCC

В компонент сильной связности (SCC) ориентированного графа - это максимально связный граф - все узлы достижимы друг от друга. Справедливый SCC - это тот, который имеет преимущество по крайней мере в одном узле для каждого из справедливых условий.

Чтобы проверить справедливость EG для любой формулы,

Вычислить то, что называется обозначение формулы. В основном все состояния такие, что M, s | = формула.
ограничить модель обозначением.
Найдите ярмарку SCC.
Получите объединение всех 3 (см. Выше).
Вычислите состояния, которые могут достичь союза.

Алгоритм Эмерсона Лея

Характеристика фиксированной точки Exist Globally задается следующим образом: [EGφ] = νZ. ([Φ] ∩ [EXZ]), что, по сути, является пределом, применяемым согласно теореме Клини. Для правильных путей это становится [Ef Gφ] = νZ. ([Φ] ∩_{Fi ∈FT} [EX [E (Z U (Z ∧ Fi))]), что означает, что формула выполняется в текущем состоянии, а также в следующих состояниях и состояниях, следующих за следующими, до тех пор, пока не будут выполнены все условия справедливости. Это означает, что условие эквивалентно своего рода точке принятия, где условием принятия является весь набор справедливых условий.

Navigation