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

Справедливая логика вычислительного дерева — это традиционная логика вычислительного дерева, изучаемая с явными ограничениями справедливости.

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

Это объявляет такие условия, как все процессы, выполняемые бесконечно часто. Если вы считаете, что процессы представляют собой Pi _, то условие становится следующим:

$\bigwedge GFP_{i}$

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

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

$\bigwedge (GFR\longrightarrow GFC)$

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

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

1. M _f , s _i |= A $\phi$ тогда и только тогда, когда $\phi$ держится на всех честных путях.

2. M _f , s _i |= E $\phi$ тогда и только тогда, когда $\phi$ держится на одном или нескольких справедливых путях.

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

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

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

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

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

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

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

Ссылки

• Эмерсон, Э.А.; Халперн, JY (1985). «Процедуры принятия решений и выразительность во темпоральной логике ветвления времени» . Журнал компьютерных и системных наук . 30 (1): 1–24. дои : 10.1016/0022-0000(85)90001-7 .
• Кларк, Эм. Эм . ; Эмерсон, Э.А. и Систла, AP (1986). «Автоматическая верификация параллельных систем с конечным числом состояний с использованием спецификаций темпоральной логики» . Транзакции ACM в языках и системах программирования . 8 (2): 244–263. дои : 10.1145/5397.5399 . S2CID   52853200 .