CTL*

CTL* — это надмножество вычислительной древовидной логики (CTL) и линейной темпоральной логики (LTL). Он свободно комбинирует квантификаторы пути и темпоральные операторы. Как и CTL, CTL* представляет собой логику времени ветвления. Формальная семантика формул CTL* определяется относительно заданной структуры Крипке .

История

LTL был предложен для проверки компьютерных программ сначала Амиром Пнуэли в 1977 году. Четыре года спустя, в 1981 году, Э.М. Кларк и Э.А. Эмерсон изобрели CTL и проверку моделей CTL . CTL* был определен Э.А. Эмерсоном и Джозефом Ю. Халперном в 1983 году. ^[1]

CTL и LTL были разработаны независимо до CTL*. Обе подлогики стали стандартами в сообществе по проверке моделей , тогда как CTL* имеет практическое значение, поскольку обеспечивает выразительный испытательный стенд для представления и сравнения этой и других логик. Это удивительно ^{[ нужна ссылка ]} потому что вычислительная сложность проверки модели в CTL* не хуже, чем в LTL: они оба лежат в PSPACE .

Синтаксис

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

\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 A\phi \mid E\phi

\phi ::=\Phi \mid (\neg \phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\mid X\phi \mid F\phi \mid G\phi \mid [\phi U\phi ]\mid [\phi R\phi ]

где $p$ колеблется в пределах набора атомарных формул . Действительные CTL*-формулы строятся с использованием нетерминального $\Phi$ . Эти формулы называются формулами состояния , а те, которые созданы символом $\phi$ называются формулами пути . (Приведенная выше грамматика содержит некоторые избыточности; например $\Phi \lor \Phi$ а также импликация и эквивалентность могут быть определены только для булевых алгебр (или логики высказываний ) из отрицания и конъюнкции, а временные операторы X и U достаточны для определения двух других .)

Операторы в основном такие же, как и в CTL . Однако в CTL каждый темпоральный оператор ( $X,F,G,U$ ) должен непосредственно предваряться квантором, тогда как в CTL* это не требуется. Квантор универсального пути может быть определен в CTL* так же, как и для классического исчисления предикатов. $A\phi =\neg E\neg \phi$ , хотя это невозможно во фрагменте CTL.

Примеры формул

Формула CTL*, которая не находится ни в LTL, ни в CTL: $EX(p)\land AFG(p)$
Формула LTL, которой нет в CTL: $\ AFG(p)$
Формула CTL, которая не указана в LTL: $\ EX(p)$
Формула CTL* в CTL и LTL: $\ AG(p)$

Примечание. Если LTL рассматривается как подмножество CTL*, к любой формуле LTL неявно добавляется квантор универсального пути. $A$ .

Семантика

Семантика CTL* определяется относительно некоторой структуры Крипке . Как следует из названия, формулы состояния интерпретируются относительно состояний этой структуры, а формулы пути интерпретируются относительно путей на ней.

Формулы состояния

Если государство $s$ структуры Крипке удовлетворяет формуле состояния $\Phi$ это обозначается $s\models \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 A\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi$ для всех путей $\ \pi$ начиная с $s{\Big )}$
${\Big (}({\mathcal {M}},s)\models E\phi {\Big )}\Leftrightarrow {\Big (}\pi \models \phi$ по какому-то пути $\ \pi$ начиная с $s{\Big )}$

Формулы пути

Отношение удовлетворения $\pi \models \phi$ для формул пути $\ \phi$ и путь $\pi =s_{0}\to s_{1}\to \cdots$ также определяется индуктивно. Для этого пусть $\ \pi [n]$ обозначаем подпуть $s_{n}\to s_{n+1}\to \cdots$ :

${\Big (}\pi \models \Phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s_{0})\models \Phi {\Big )}$
${\Big (}\pi \models \neg \phi {\Big )}\Leftrightarrow {\Big (}\pi \not \models \phi {\Big )}$
${\Big (}\pi \models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}$
${\Big (}\pi \models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}$
${\Big (}\pi \models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}\pi \not \models \phi _{1}{\big )}\lor {\big (}\pi \models \phi _{2}{\big )}{\Big )}$
${\bigg (}\pi \models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}\pi \models \phi _{1}{\big )}\land {\big (}\pi \models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}\pi \models \phi _{1}{\big )}\land \neg {\big (}\pi \models \phi _{2}{\big )}{\Big )}{\bigg )}$
${\Big (}\pi \models X\phi {\Big )}\Leftrightarrow {\Big (}\pi [1]\models \phi {\Big )}$
${\Big (}\pi \models F\phi {\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:\pi [n]\models \phi {\Big )}$
${\Big (}\pi \models G\phi {\Big )}\Leftrightarrow {\Big (}\forall n\geqslant 0:\pi [n]\models \phi {\Big )}$
${\Big (}\pi \models [\phi _{1}U\phi _{2}]{\Big )}\Leftrightarrow {\Big (}\exists n\geqslant 0:{\big (}\pi [n]\models \phi _{2}\land \forall 0\leqslant k<n:~\pi [k]\models \phi _{1}{\big )}{\Big )}$

Проблемы с решением

Проверка модели CTL* (входной формулы для фиксированной модели) является PSPACE-полной. ^[2] и выполнимости проблема 2EXPTIME -полна. ^[2]^[3]

См. также

Ссылки

^ Эмерсон, Э. Аллен; Халперн, Джозеф Ю. (1983). « Пересмотр «Иногда» и «Не никогда». Материалы 10-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования — POPL '83 . стр. 127–140. дои : 10.1145/567067.567081 . ISBN 0897910907 . S2CID 15728260 .
^ Jump up to: ^а ^б Байер, Кристель ; Катоен, Йост-Питер (1 января 2008 г.). Принципы проверки моделей (серия «Представление и разум») . Массачусетский технологический институт Пресс. ISBN 978-0262026499 .
^ Орна Купферман ; Моше Ю. Варди (июнь 1999 г.). «Возвращение к проблеме церкви». Бюллетень символической логики . 5 (2): 245–263. дои : 10.2307/421091 . JSTOR 421091 . S2CID 18833301 .

Амир Пнуэли : Временная логика программ. Труды 18-го Ежегодного симпозиума IEEE по основам информатики (FOCS), 1977, 46–57. DOI= 10.1109/SFCS.1977.32
Э. Аллен Эмерсон , Джозеф Ю. Халперн : Еще раз о «иногда» и «не никогда»: о ветвлениях и линейной временной логике. Журнал ACM 33, 1 (январь 1986 г.), 151–178. DOI= http://doi.acm.org/10.1145/4904.4999
Ф. Шнобелен: Сложность проверки модели темпоральной логики. Достижения в модальной логике 2002: 393–436.

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

CTL Преподавание слайдов профессора Алессандро Артале в Свободном университете Боцен-Больцано

[EmersonHalpern1983-1] Эмерсон, Э. Аллен; Халперн, Джозеф Ю. (1983). « Пересмотр «Иногда» и «Не никогда». Материалы 10-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования — POPL '83 . стр. 127–140. дои : 10.1145/567067.567081 . ISBN 0897910907 . S2CID 15728260 .

[:0-2] Jump up to: ^а ^б Байер, Кристель ; Катоен, Йост-Питер (1 января 2008 г.). Принципы проверки моделей (серия «Представление и разум») . Массачусетский технологический институт Пресс. ISBN 978-0262026499 .

[3] Орна Купферман ; Моше Ю. Варди (июнь 1999 г.). «Возвращение к проблеме церкви». Бюллетень символической логики . 5 (2): 245–263. дои : 10.2307/421091 . JSTOR 421091 . S2CID 18833301 .

[1]

[2]

[3]