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

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

История

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

С момента появления CTL ведутся споры об относительных достоинствах CTL и LTL. Поскольку CTL более эффективен в вычислительном отношении для проверки моделей, он стал более распространенным в промышленном использовании, и многие из наиболее успешных инструментов проверки моделей используют CTL в качестве языка спецификации. ^[1]

Синтаксис CTL

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

{\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}}

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

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

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

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

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

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

Проблема с этой строкой заключается в том, что $\mathrm {U}$ может возникнуть только в сочетании с $\mathrm {A}$ или $\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 интерпретируются по системам переходов . Переходная система представляет собой тройку ${\mathcal {M}}=(S,{\rightarrow },L)$ , где $S$ представляет собой совокупность состояний, ${\rightarrow }\subseteq S\times S$ является переходным отношением, которое считается последовательным, т. е. каждое состояние имеет хотя бы одного преемника, и $L$ — это функция маркировки, присваивающая состояниям пропозициональные буквы. Позволять ${\mathcal {M}}=(S,\rightarrow ,L)$ быть такой переходной моделью, с $s\in S$ , и $\phi \in F$ , где $F$ набор корректных формул на языке представляет собой ${\mathcal {M}}$ .

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

${\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}$
${\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}$
${\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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 )}$
${\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, приведенные выше, относятся к путям вычислений в моделях и в конечном итоге характеризуют «дерево вычислений»;это утверждения о природе бесконечно глубокого дерева вычислений, корнями которого являются данное состояние. $s$ .

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

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

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

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

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

\neg AF\phi \equiv EG\neg \phi

\neg EF\phi \equiv AG\neg \phi

\neg AX\phi \equiv EX\neg \phi

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

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

AG\phi \equiv \phi \land AXAG\phi

EG\phi \equiv \phi \land EXEG\phi

AF\phi \equiv \phi \lor AXAF\phi

EF\phi \equiv \phi \lor EXEF\phi

A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])

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 расширен второго порядка. количественной оценкой $\exists p$ и $\forall p$ к количественной вычислительной древовидной логике (QCTL). ^[2] Есть две семантики:

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

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

См. также

Ссылки

^ Варди, Моше Ю. (2001). «Ветвление против линейного времени: финальная схватка» (PDF) . Конспекты лекций по информатике. Том. 2031. Шпрингер, Берлин. стр. 1–22. дои : 10.1007/3-540-45319-9_1 . ISBN 978-3-540-41865-8 . {{cite book}}: |journal= игнорируется ( помощь ) ; Отсутствует или пусто |title= ( помощь )
^ Дэвид, Амели; Ларуссини, Франсуа; Марки, Николас (2016). Дешарне, Жозе; Джагадисан, Радха (ред.). «О выразительности ККТЛ» . 27-я Международная конференция по теории параллелизма (CONCUR 2016) . Международные труды Лейбница по информатике (LIPIcs). 59 . Дагштуль, Германия: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 28:1–28:15. doi : 10.4230/LIPIcs.CONCUR.2016.28 . ISBN 978-3-95977-017-0 .
^ Хоссейн, Акаш; Ларуссини, Франсуа (2019). Гампер, Иоганн; Пинчинат, Софи; Скьявикко, Гвидо (ред.). «От количественного CTL к QBF» . 26-й Международный симпозиум по временному представлению и рассуждению (TIME 2019) . Международные труды Лейбница по информатике (LIPIcs). 147 . Дагштуль, Германия: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 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

[1] Варди, Моше Ю. (2001). «Ветвление против линейного времени: финальная схватка» (PDF) . Конспекты лекций по информатике. Том. 2031. Шпрингер, Берлин. стр. 1–22. дои : 10.1007/3-540-45319-9_1 . ISBN 978-3-540-41865-8 . {{cite book}}: |journal= игнорируется ( помощь ) ; Отсутствует или пусто |title= ( помощь )

[2] Дэвид, Амели; Ларуссини, Франсуа; Марки, Николас (2016). Дешарне, Жозе; Джагадисан, Радха (ред.). «О выразительности ККТЛ» . 27-я Международная конференция по теории параллелизма (CONCUR 2016) . Международные труды Лейбница по информатике (LIPIcs). 59 . Дагштуль, Германия: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik: 28:1–28:15. doi : 10.4230/LIPIcs.CONCUR.2016.28 . ISBN 978-3-95977-017-0 .

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

[1]

[2]

[3]