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

Эта статья включает в себя список общих ссылок , но он остается в основном непроверенным, поскольку в нем отсутствуют соответствующие встроенные ссылки . Пожалуйста, помогите улучшить эту статью, добавив более точные цитаты. ( Октябрь 2015 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

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

Синтаксис 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 U}$${\displaystyle A}$${\displaystyle E}$

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

Операторы [ править ]

Логические операторы [ править ]

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

Временные операторы [ править ]

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

• Кванторы по путям
  • A Φ - A ll: Φ должен удерживаться на всех путях, начиная с текущего состояния.
  • E Φ - E xists: существует по крайней мере один путь, начинающийся с текущего состояния, в котором выполняется Φ.
• Квантификаторы, зависящие от пути
  • X φ  - Ne x t: φ должно выполняться в следующем состоянии (этот оператор иногда обозначается N вместо X ).
  • G φ  - G локально: φ должен удерживаться на всем последующем пути.
  • F φ  - F в конечном итоге : φ в конечном итоге должен сохраниться (где-то на следующем пути).
  • φ U ψ  - U ntil: φ должно удерживаться, по крайней мере, до тех пор, пока в некоторой позиции не будет выполнено ψ . Это означает, что ψ будет проверяться в будущем.
  • φ W ψ  - 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)}$

с , где F есть множество ппфа над языком из .${\displaystyle s\in S,\phi \in 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 \neg A\Phi \equiv E\neg \Phi }$

Кроме того, таковы G и 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 - «на улице тепло».

• AG .P

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

• EF .P

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

• AF . EG .P

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

• EG . AF .P

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

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

• AG (P U Q)

«С этого момента, пока на улице не станет тепло, я буду любить шоколад каждый божий день. Как только на улице станет тепло, все ставки на то, буду ли я больше любить шоколад, сняты. Да, и в конечном итоге на улице будет тепло, даже если только один день ".

• 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.${\displaystyle \Rightarrow }$${\displaystyle \land }$

Расширения [ править ]

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

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

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

См. Также [ править ]

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

Ссылки [ править ]

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

Внешние ссылки [ править ]

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