Логика дерева вычислений

Логика дерева вычислений ( CTL ) — это логика времени ветвления , что означает, что ее модель времени представляет собой древовидную структуру, в которой будущее не определено; в будущем существуют разные пути, любой из которых может оказаться реальным и реализованным путем. Он используется при формальной проверке программных или аппаратных артефактов, обычно программными приложениями, известными как средства проверки моделей , которые определяют, обладает ли данный артефакт свойствами безопасности или живучести . Например, CTL может указать, что, когда некоторое начальное условие удовлетворено (например, все переменные программы положительны или ни одна машина на шоссе не пересекает две полосы), тогда все возможные выполнения программы избегают некоторых нежелательных условий (например, деления числа на ноль или две машины столкнулись на шоссе). В этом примере свойство безопасности может быть проверено средством проверки модели, которое исследует все возможные переходы из состояний программы, удовлетворяющих начальному условию, и гарантирует, что все такие выполнения удовлетворяют этому свойству. Логика дерева вычислений принадлежит к классу темпоральных логик , который включает линейную темпоральную логику  (LTL). Хотя существуют свойства, выражаемые только в CTL, и свойства, выражаемые только в LTL, все свойства, выражаемые в любой логике, также могут быть выражены в CTL* .

CTL был впервые предложен Эдмундом М. Кларком и Э. Алленом Эмерсоном в 1981 году, которые использовали его для синтеза так называемых скелетов синхронизации , то есть абстракций параллельных программ .

Синтаксис CTL

Язык правильных формул для CTL генерируется следующей грамматикой :

${\displaystyle {\begin{aligned}\phi &::=\bot \mid \top \mid p\mid (\neg \phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\\&\mid \quad {\mbox{AX }}\phi \mid {\mbox{EX }}\phi \mid {\mbox{AF }}\phi \mid {\mbox{EF }}\phi \mid {\mbox{AG }}\phi \mid {\mbox{EG }}\phi \mid {\mbox{A }}[\phi {\mbox{ U }}\phi ]\mid {\mbox{E }}[\phi {\mbox{ U }}\phi ]\end{aligned}}}$

где пробегает набор атомарных формул . Необязательно использовать все связки – например, содержит полный набор связок, а остальные можно определить с их помощью. ${\displaystyle p}$ ${\displaystyle \{\neg ,\land ,{\mbox{AX}},{\mbox{AU}},{\mbox{EU}}\}}$

• ${\displaystyle {\mbox{A}}}$означает «вдоль всех путей» (неизбежно)
• ${\displaystyle {\mbox{E}}}$означает «по крайней мере (существует) один путь» (возможно)

Например, ниже приведена корректная формула CTL:

${\displaystyle {\mbox{EF }}({\mbox{EG }}p\Rightarrow {\mbox{AF }}r)}$

Следующая формула CTL не является корректной:

${\displaystyle {\mbox{EF }}{\big (}r{\mbox{ U }}q{\big )}}$

Проблема с этой строкой заключается в том, что она может возникнуть только в сочетании с или . ${\displaystyle \mathrm {U} }$ ${\displaystyle \mathrm {A} }$ ${\displaystyle \mathrm {E} }$

CTL использует атомарные предложения в качестве строительных блоков для формулирования утверждений о состояниях системы. Эти предложения затем объединяются в формулы с использованием логических операторов и темпоральных операторов .

Операторы

Логические операторы

Логические операторы обычные: ¬, ∨, ∧, ⇒ и ⇔. Наряду с этими операторами формулы CTL также могут использовать логические константы true и false .

Временные операторы

Временные операторы следующие:

• Кванторы по путям
  • A Φ – A ll: Φ должно выполняться на всех путях, начиная с текущего состояния.
  • E Φ – существует : существует хотя бы один путь, начинающийся из текущего состояния, в котором выполняется Φ.
• Кванторы, специфичные для пути
  • X φ  – Ne x t: φ должен выполняться в следующем состоянии (этот оператор иногда обозначается N вместо X ).
  • G φ  – G глобально: φ должна соблюдаться на всем последующем пути.
  • F φ  – F наконец: φ в конце концов должна выполняться (где-то на последующем пути).
  • φ U ψ  – Until : φ должно выполняться по крайней мере до тех пор, пока в некоторой позиции не будет выполнено ψ . Это означает, что ψ будет проверена в будущем.
  • φ W ψ  – Слабое до тех пор, пока: φ должно выполняться до тех пор, пока не будет выполняться ψ . Отличие от U состоит в том, что нет никакой гарантии, что ψ когда-либо будет проверена. Оператор W иногда называют «если».

В CTL* темпоральные операторы можно свободно смешивать. В CTL операторы всегда должны быть сгруппированы парами: один оператор пути, за которым следует оператор состояния. См. примеры ниже. CTL* строго более выразителен, чем CTL.

Минимальный набор операторов

В CTL существует минимальный набор операторов. Все формулы CTL можно преобразовать для использования только этих операторов. Это полезно при проверке модели . Один минимальный набор операторов: {true, ∨, ¬, EG , EU , EX }.

Некоторые из преобразований, используемых для темпоральных операторов:

• EF φ == E [истинно U ( φ )] (потому что F φ == [истинно U ( φ )] )
• AX φ == ¬ EX (¬ φ )
• AG φ == ¬ EF (¬ φ ) == ¬ E [истинное U (¬ φ )]
• AF φ == A [истина U φ ] == ¬ EG (¬ φ )
• A [ φ U ψ ] == ¬( E [(¬ ψ ) U ¬( φ ∨ ψ )] ∨ EG (¬ ψ ) )

Семантика CTL

Определение

Формулы CTL интерпретируются по системам переходов . Система переходов — это тройка , где — набор состояний, — отношение перехода, предполагающееся последовательным, т. е. каждое состояние имеет по крайней мере один преемник, и функция маркировки, присваивающая состояниям пропозициональные буквы. Позвольте быть такой моделью перехода, с , и , где – набор корректных формул на языке . ${\displaystyle {\mathcal {M}}=(S,{\rightarrow },L)}$ ${\displaystyle S}$ ${\displaystyle {\rightarrow }\subseteq S\times S}$ ${\displaystyle L}$ ${\displaystyle {\mathcal {M}}=(S,\rightarrow ,L)}$ ${\displaystyle s\in S}$ ${\displaystyle \phi \in F}$ ${\displaystyle F}$ ${\displaystyle {\mathcal {M}}}$

Тогда отношение семантического следования определяется рекурсивно на : ${\displaystyle ({\mathcal {M}},s\models \phi )}$ ${\displaystyle \phi }$

1. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}}$
2. ${\displaystyle {\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}}$
3. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}}$
4. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
5. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
6. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\not \models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
7. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}{\bigg )}}$
8. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
9. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
10. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AG\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
11. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
12. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
13. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
14. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models A[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$
15. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$

Характеристика CTL

Правила 10–15, приведенные выше, относятся к путям вычислений в моделях и в конечном итоге характеризуют «дерево вычислений»; это утверждения о природе бесконечно глубокого дерева вычислений, корнями которого являются данное состояние . ${\displaystyle s}$

Семантические эквиваленты

Формулы и называются семантически эквивалентными, если любое состояние в любой модели, удовлетворяющее одной, также удовлетворяет и другой. Это обозначается ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \phi \equiv \psi }$

Можно видеть, что и являются двойственными, являясь кванторами универсального и экзистенциального пути вычисления соответственно: . ${\displaystyle \mathrm {A} }$ ${\displaystyle \mathrm {E} }$ ${\displaystyle \neg \mathrm {A} \Phi \equiv \mathrm {E} \neg \Phi }$

Кроме того, таковы и . ${\displaystyle \mathrm {G} }$ ${\displaystyle \mathrm {F} }$

Следовательно, пример законов Де Моргана можно сформулировать в CTL:

${\displaystyle \neg AF\phi \equiv EG\neg \phi }$

${\displaystyle \neg EF\phi \equiv AG\neg \phi }$

${\displaystyle \neg AX\phi \equiv EX\neg \phi }$

Используя такие тождества, можно показать, что подмножество временных связок CTL является адекватным, если оно содержит хотя бы одну из и хотя бы одну из и логических связок. ${\displaystyle EU}$ ${\displaystyle \{AX,EX\}}$ ${\displaystyle \{EG,AF,AU\}}$

Важные эквивалентности, приведенные ниже, называются законами расширения ; они позволяют развернуть проверку CTL-коннекта по отношению к его преемникам во времени.

${\displaystyle AG\phi \equiv \phi \land AXAG\phi }$

${\displaystyle EG\phi \equiv \phi \land EXEG\phi }$

${\displaystyle AF\phi \equiv \phi \lor AXAF\phi }$

${\displaystyle EF\phi \equiv \phi \lor EXEF\phi }$

${\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}$

${\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}$

Примеры

Пусть «P» означает «Я люблю шоколад», а Q означает «На улице тепло».

• АГ .П

«Теперь я буду любить шоколад, что бы ни случилось».

• ЭФ .П

«Возможно, когда-нибудь мне понравится шоколад, хотя бы на один день».

• АФ . ЭГ .П

«Всегда возможно (А.Ф.), что мне вдруг навсегда понравится шоколад». (Примечание: не только оставшаяся часть моей жизни, поскольку моя жизнь конечна, а G бесконечна).

• ЭГ . АФ .П

«В зависимости от того, что произойдет в будущем (E), возможно, что в оставшееся время (G) мне будет гарантирован по крайней мере один (AF) шоколадный день впереди. Однако, если что-нибудь когда-нибудь произойдет ошибаюсь, тогда все ставки отменены, и нет никакой гарантии, полюблю ли я когда-нибудь шоколад».

В двух следующих примерах показана разница между CTL и CTL*, поскольку они позволяют оператору Until не уточняться каким-либо оператором пути ( A или E ):

• АГ (П У К)

«С этого момента, пока на улице не станет тепло, я буду любить шоколад каждый божий день. Как только на улице станет тепло, все ставки на то, буду ли я больше любить шоколад, будут сделаны. О, и рано или поздно на улице будет тепло, даже если только на какое-то время». один день».

• EF (( EX .P) U ( AG .Q))

«Возможно, что: в конечном итоге наступит время, когда будет тепло всегда (AG.Q), и что до этого времени всегда будет какой-то способ заставить меня полюбить шоколад на следующий день (EX.P)».

Отношения с другой логикой

Логика дерева вычислений (CTL) является подмножеством CTL*, а также модального µ-исчисления . CTL также является фрагментом темпоральной логики переменного времени (ATL) Алура, Хенцингера и Купфермана.

Логика дерева вычислений (CTL) и линейная временная логика (LTL) являются подмножеством CTL*. CTL и LTL не эквивалентны и имеют общее подмножество, которое является подмножеством как CTL, так и LTL.

• FG .P существует в LTL, но не существует в CTL.
• AG (P⇒(( EX .Q)∧( EX ¬Q))) и AG.EF .P существуют в CTL, но не в LTL.

Расширения

CTL был расширен количественной оценкой второго порядка и количественной логикой вычислительного дерева (QCTL). ^[1] Существует две семантики: ${\displaystyle \exists p}$ ${\displaystyle \forall p}$

• семантика дерева. Помечаем узлы дерева вычислений. QCTL* = QCTL = MSO над деревьями. Проверка модели и ее удовлетворительность завершены.
• Семантика структуры. Мы маркируем состояния. QCTL* = QCTL = MSO над графиками . Проверка модели является PSPACE-полной , но выполнимость неразрешима .

Чтобы воспользоваться преимуществами решателей QBF, было предложено свести проблему проверки модели QCTL со структурной семантикой к TQBF (истинным количественным логическим формулам). ^[2]

Смотрите также

• Вероятностный CTL
• Справедливая логика вычислительного дерева
• Линейная темпоральная логика

Рекомендации

1. Дэвид, Амели; Ларуссини, Франсуа; Марки, Николас (2016). Дешарне, Жозе; Джагадисан, Радха (ред.). «О выразительности ККТЛ». 27-я Международная конференция по теории параллелизма (CONCUR 2016) . Международные труды Лейбница по информатике (LIPIcs). Дагштуль, Германия: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. 59 : 28:1–28:15. doi : 10.4230/LIPIcs.CONCUR.2016.28. ISBN 978-3-95977-017-0.
2. Хоссейн, Акаш; Ларуссини, Франсуа (2019). Гампер, Иоганн; Пинчинат, Софи; Скьявикко, Гвидо (ред.). «От количественного CTL до QBF». 26-й Международный симпозиум по временному представлению и рассуждению (TIME 2019) . Международные труды Лейбница по информатике (LIPIcs). Дагштуль, Германия: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. 147 : 11:1–11:20. doi : 10.4230/LIPIcs.TIME.2019.11. ISBN 978-3-95977-127-6. S2CID  195345645.

• Э.М. Кларк; Э.А. Эмерсон (1981). «Проектирование и синтез скелетов синхронизации с использованием временной логики ветвления» (PDF) . Логика программ, Материалы семинара, Конспект лекций по информатике . Конспекты лекций по информатике. Шпрингер, Берлин. 131 : 52–71. дои : 10.1007/BFb0025774. ISBN 3-540-11212-Х.
• Майкл Хут; Марк Райан (2004). Логика в информатике (второе изд.). Издательство Кембриджского университета. п. 207. ИСБН 978-0-521-54310-1.
• Эмерсон, Э.А.; Халперн, JY (1985). «Процедуры принятия решений и выразительность во временной логике ветвления времени». Журнал компьютерных и системных наук . 30 (1): 1–24. CiteSeerX  10.1.1.221.6187 . дои : 10.1016/0022-0000(85)90001-7.
• Кларк, EM; Эмерсон, Э.А. и Систла, AP (1986). «Автоматическая верификация параллельных систем с конечным состоянием с использованием спецификаций темпоральной логики». Транзакции ACM в языках и системах программирования . 8 (2): 244–263. дои : 10.1145/5397.5399 . S2CID  52853200.
• Эмерсон, Э.А. (1990). «Временная и модальная логика». Ян ван Леувен (ред.). Справочник по теоретической информатике, том. Б. _ МТИ Пресс. стр. 955–1072. ISBN 978-0-262-22039-2.

Внешние ссылки

• Обучающие слайды CTL