Алгоритмические свойства модальных логик информационных систем тема диссертации и автореферата по ВАК РФ 05.13.17, кандидат физико-математических наук Шапировский, Илья Борисович

• Шапировский, Илья Борисович
• кандидат физико-математических наук
• 2007

Оглавление диссертации кандидат физико-математических наук Шапировский, Илья Борисович

Введение

1 Основные понятия

1.1 Модальные логики.

1.2 Семантика Крипке.

1.3 Канонические шкалы и модели.

1.4 Подшкалы и подмодели.

1.5 р-морфизмы шкал и моделей.

1.6 Свойства бинарных отношений.

1.7 Транзитивные шкалы.

2 Аксиоматизация одномодальных геометрических структур

2.1 Релятивистские модальности.

2.2 2-плотные транзитивные логики.

2.3 Финитная аппроксимируемость 2-плотных транзитивных логик

2.4 Удобные шкалы.

2.5 Аксиоматизация логики хронологического будущего.

2.6 Регионы в W1.

2.7 Насыщенные множества регионов

2.8 Не конечно аксиоматизируемые логики.

3 Логики с универсальной модальностью

3.1 Универсальная модальность.

3.2 Перевод.

3.3 Антинаправленные шкалы.

3.4 Логики геометрических структур с универсальным отношением.

4 Алгоритмические вопросы

4.1 Контрмодели для 2-плотных логик.

4.2 PSPACE-разрешимость 2-плотных логик.

4.3 PSPACE-трудпость 2-плотных логик.

Введение диссертации (часть автореферата) на тему «Алгоритмические свойства модальных логик информационных систем»

Актуальность темы. При построении и анализе сложных информационных систем во многих случаях оказывается невозможным оперировать с точным численным описанием системы: это может быть связано как с недоступностью такого описания, так и с практической невозможностью его обработки. В таких случаях возникает задача описания системы средствами формальных языков. Используемый при этом формальный язык должен быть, с одной стороны, достаточно выразительном для отражения содержательных свойств системы; с другой стороны — предлагаемое описание должно быть приемлемым с алгоритмической точки зрения. Удобным формализмом для такого (качественного) описания оказываются пропозициональные модальные логики.

С точки зрения математической логики, модальные логики являются логиками второго порядка, и потому в них могут быть описаны свойства, невыразимые в классических первопорядковых логиках. Кроме того, для модальных логик характерна относительно невысокая алгоритмическая сложность, что оказывается принципиальным для их реальных приложений.

Как область математической логики, модальная логика возникла в середине прошлого века. В 1960—1970 гг. были развиты математические методы для изучения различных свойств модальных логик — полноты, финитной аппроксимируемости, разрешимости, и др. (см., например, [8]). Было начато исследование алгоритмической сложности модальных логик

25]. В конце 70-х годов 20-го века начался новый этап — появляются многочисленные приложения модальных логик в информатике, такие как динамические логики вычислимости [31, 16, 17], логики параллельности [30,11, 29, И, 13], логики алгебр процессов [23, 28], изучаются свойства этих логик [34, 32, 12, 13, 14, 24]. В задачах искусственного интеллекта активно используются модальные логики представления знаний [33], в том числе так называемые пространственные модальные логики, предназначенные для качественного анализа пространственной информации (см., например, [27]). Таким образом, в настоящее время модальная логика оформилась как самостоятельная дисциплина на стыке информатики и математической логики с широким кругом приложений.

Следует отмстить, что для представления пространственной информации при решении прикладных задач (как, например, распознавание образов или построение геоинформационных систем) оказывается удобным использовать формальные языки, в которых высказывания относятся не к отдельным точкам в пространстве, а к множествам определённого вида (регионам).

В модальных логиках подобный подход для решения задач информатики впервые был описан в работе [21], где введены модальные логики временных интервалов. Предложенный подход оказался эффективным при решении задач верификации моделей программ, спецификации систем реального времени, компьютерной лингвистики (см., например, обзорную работу [19]). Как было замечено позднее

26], этот подход естественным образом обобщается на многомерный случай для решения задач представления пространственной информации: аналогом интервалов являются регионы в действительном (или ином топологическом или метрическом) пространстве. Однако на этом пути был получен ряд отрицательных результатов: оказалось [26], что различные многомодальные логики регионов являются неразрешимыми или даже неперечислимыми. Таким образом, возникает задача построения модальных логик регионов, с одной стороны, достаточно выразительных, с другой — разрешимых и обладающих невысокой алгоритмической сложностью, что и являлось предметом исследований.

Цель работы. Целью работы является построение разрешимых пространственных модальных логик, и исследование их алгоритмической сложности.

Научная новизна. Все основные результаты диссертации являются новыми.

Для ряда модальных логик пространственных отношений на регионах в действительном пространстве впервые построены полные системы аксиом. Кроме того, в противовес известным отрицательным алгоритмическим результатам о логиках регионов получены положительные результаты — о разрешимости и PSPACE-полноте.

Для доказательства финитной аппроксимируемости модальных логик используется метод селективной фильтрации в сочетании с методом максимальных точек в канонической модели. Комбинация двух этих хорошо известных подходов даёт эффективный метод доказательства финитной аппроксимируемости (следовательно, разрешимости) транзитивных модальных логик.

В работе [44] было замечено, что изучение свойств релятивистских модальных логик может быть использовано при исследовании модальных логик интервалов. В диссертации эта взаимосвязь распространяется на многомерный случай. Постановка задачи о релятивистских модальных логиках принадлежит А. Прайору. Первые конкретные примеры таких логик для отношения причинного будущего — были построены Р. Голдблаттом [18] и В.Б. Шехтманом [43]. Вопрос о модальной аксиоматизации отношения хронологического будущего долгое время оставался открытым, его решение излагается в диссертации.

Предложен новый метод доказательства PSPACE-разрешимости транзнтнвиых модальных логик.

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

Теоретическая и практическая ценность. Работа носит теоретический характер. Полученные в ней результаты и развитые методы могут быть полезны специалистам, работающим в ИППИ РАН им. А.А. Харкевича, МГУ им. М. В. Ломоносова, МИ РАН им. В.А. Стеклова, Тверском Государственном Университете и др. Кроме того, описанные в диссертации алгоритмы могут быть реализованы в программных средствах, предназначенных для анализа пространственной информации.

Апробация работы. Результаты диссертации докладывались и обсуждались в течении 2002-2007 гг. на научном семинаре Добрушинской лаборатории Института проблем передачи информации РАН; на научно-исследовательском семинаре 'Алгоритмические вопросы алгебры и логики' под руководством академика РАН С.И.Адяна и па других спецсеминарах кафедры математической логики и теории алгоритмов МГУ; на научных семинарах в Институте исследований по информатике Тулузы (Франция). Результаты были также представлены на 4-й, 5-й и 6-й Международных конференциях по модальной логике (Тулуза, Франция, 2002; Манчестер, Англия, 2004; Брисбен, Австралия, 2006); на Международном симпозиуме по логике и вычислимости (Москва, 2004); на Международной конференции 'Модальные логики и их приложения в информатике' (Москва, 2005); на XXVIII Конференции молодых учёных механико-математического факультета МГУ (Москва, 2006).

Работа была поддержана грантами РФФИ 'Пространственные модальные логики' (А^ 02-01-22003) и 'Геометрические модальные логики' (№ 06-01-72555).

Публикации. По теме диссертации опубликованы работы [35, 36, 37, 38, 39, 40, 41, 42, 5, 6]. Работы [40, 41, 42] написаны в соавторстве с В.Б. Шехтманом.

СОДЕРЖАНИЕ РАБОТЫ

Во Введении даётся обзор проблем и результатов, связанных с темой диссертации, приводятся основные полученные результаты и описывается её содержание.

В Главе 1 содержатся предварительные сведения из теории модальных логик. В частности, вводится семантика Крипке, описываются некоторые преобразования шкал и моделей Крипке, сохраняющие истинность модальных формул.

Множество п-модальных формул FM(§i,.,0n) строится из счетного множества пропозициональных переменных PV = {pi,p2,.}, пропозициональной константы L (ложь), двуместной связки —> (импликация), и одноместных связок Qi,.,On (модальности типа "возмоэ/сно") следующим образом:

• ±,р\,р2, ■. - формулы;

• Если А, В— формулы, то (А —> В) — формула;

• Если А — формула, то О\А — формула, i — 1,., п.

Связки -1, Л, V, Т, Ц- рассматриваются как сокращения, в частности:

DiA — -i<)j-iA (модальности типа "неодходимо").

Для формулы А пусть Sub(A) обозначает множество всех её подформул. п-модальной логикой называется множество n-модальных формул L С FM(Оь • • •, Отг), такое, что

• L содержит все пропозициональные тавтологии,

• L содержит формулы —кОг-L? г = 1,., n,

• L содержит формулы Oi(pi V p2) OiPi V O1P2, г = 1,., n,

• L замкнуто относительно правила Modus Ponens, правила подстановки, и правил монотонности Morij, г = 1,., п:

Monj : Л Б 6 L =4> 0г-Л OiB G L.

Кп обозначает наименьшую п-модальную логику. При п = 1 в дальнейшем мы будем опускать индексы, т.е. вместо ОьПьКх будем писать 0,ЦКи т.п.

Для тг-модальной логики L и множества формул Ф С FM{Oi,., Qn), L + Ф обозначает наименьшую n-модальную логику, содержащую L U Ф. п-модальная логика L называется конечно аксиоматизируемой, если L = Кп + Ф для некоторого конечного Ф. Если Ф = {Л}, то пишем L + А вместо L + {Л}. Lb А обозначает А G L. п-модальной шкалой Крите (или просто п-шкалой) $ называется кортеж (W, R\,., Rn), где W — непустое множество и Ri,., Rn С W х W. Оценкой на шкале $ называется отображение в-.PV

Моделью (Крите) 9Л над шкалой $ называется пара 9), где 0 — оценка на Для всякой модальной формулы А 6 FM(0i, • • •, On) индуктивно определяется истинность формулы Л в точке ж модели (обозначение — Ш,х\= А): ш,х\=р & х е 0(р),

ЯЛ, ж 1= OiA для некоторого у имеем: и 9Л, у И А.

Формула А называется истинной в модели 9Л (обозначение: Ш 1= А), если она истинна во всех точках этой модели. Формула А называется общезначимой в шкале $ (обозначение: $ \= А), если она истинна в любой модели над А называется общезначимой в классе шкал Т (обозначение: Т \= А), если А общезначима в любой шкале $ 6 Т. Множество всех формул, общезначимых в классе Т будем обозначать через L(#)

- сокращение L({#}). Для логики L и шкалы если L(#) Э L, то $ называется L-шкалой. Формула А называется h-выполнимой, если А выполнима в некоторой L-шкале.

Хорошо известно, что если Т - класс n-шкал, то L(Т) является п-модальной логикой. Логика L называется полной относительно класса шкал Тесли L = L называется полной (по Крипке), если она полна относительно некоторого класса шкал. L называется финитно аппроксимируемой, если она полна относительно некоторого класса конечных шкал.

В Главе 2 исследуется аксиоматизация одномодальиых логик п ространствен н ых структур.

Параграфы 2.1—2.5 посвящены модальной аксиоматизации логик хронологического будущего. Отношение причинного будущего и отношение хронологического будущего -< в Rn определяются следующим образом: для X = (жь ., хп) и Y = (уи ., уп)

X < Y <£> (Vi ~ Xi)2 ^ (Уп - хп? и хп< уп, l<i<n-l

X -< Y ]Г (yi - х{)2 < (уп - хп)2 их„< уп.

1<г<п-1

Эти отношения транзитивны, и ^ рефлексивно. Хорошо известно, что модальные логики К4 = К + 0()р —> 0р, S4 = К4 + р —0р характеризуются классом всех транзитивных и классом всех транзитивных рефлексивных шкал соответственно. Таким образом, L(R", -<) Э К4 и

L(Rn, :<) Э S4. Точная аксиоматизация логик причинного будущего была дана в работах Р. Голдблатта и В.Б. Шехтмана. Было показано, что возникающие логики — это S4 и её хорошо известные расширения

S4.1 = S4 + □ Ор -н. О Dp, S4.2 = S4 + <>□р ПО РА именно, что для п > 2, L(Rn, ■<) = S4.2 [18]; кроме того, для области V в R2, ограниченной регулярной кривой, L(V, :<) = S4, L(CV, = S4.1, где CV обозначает замыкание V [43].

В диссертации доказаны аналогичные результаты для отношения -<. В отмеченной выше работе Р. Голдблатта было замечено, что свойство 2-плогпности yx\fyiWy2(xRyi A xRy2 —> 3z(xRz A zRyx A zRy2)), которым обладает отношение -< в Жп, выражается модальной аксиомой

ADens2 = 0Pl А 0Р2 0(0pi А 0р2). Для 2-плотиых логик lmi = к4 + ADens2 + от, LM2 = LMi + ODp ПОР, lm3 = k4 + ADens2 + от 0d1, в диссертации доказаны следующие результаты: ТЕОРЕМА 2.23. Для п > 2, L(M", -<) = Ш2.

ТЕОРЕМА 2.25. Пусть V — область в М2, ограниченная регулярной кривой.

Тогда

• L(V, -<) = LMi,

• L(CV, -<) С LM3,

• ЦСУ, -<) = LM3, если V выпукла.

Для доказательства этих теорем используется модификация метода из работ Р. Голдблатта и В.Б. Шехтмапа. Существенным при этом является финитная аппроксимируемость исследуемых логик. Хорошо известно, что логика S4 и рассмотренные выше её расширения S4.1, S4.2 обладают этим свойством: для этих логик (как и для многих других) применим метод "эпи-фильтраций" Леммона-Сегерберга. Однако в случае логик, содержащих аксиому ADens2, этот метод неприменим непосредственно, так как фильтрации такого рода не сохраняют свойство 2-плотности. Таким образом, именно доказательство финитной аппроксимируемости (теоремы 2.12—2.14) представляло принципиальную сложность при исследовании логик LM]— LM3 и при получении изложенных выше теорем. Требуемый результат был получен при использовании метода селективной фильтрации в сочетании с методом максимальных точек в канонической модели.

В параграфах 2.6 и 2.7, на основании результатов, полученных в параграфах 2.1—2.5, строятся аксиоматики модальных логик регионов в действительном пространстве.

Компактное множество U С R" называется регионом в R", или п-регионом, если U является замыканием непустой области.

Примерами множеств регионов в Rn являются:

7Zegn — множество всех п-рсгионов;

Corivn — множество всех выпуклых п-регионов;

Вп — множество всех шаров; мерных параллелепипедов.

Для множества n-регионов W пусть W0 обозначает расширение W всеми одноэлементными множествами: W° — WU {{AT} | X G Ш.п}.

Определим отношение компактного включения (ё: для множеств множество всех п

U,V cr положим

UtsV&CUCIV; Ш>=<ё~\ где IV и CV обозначают внутренность и замыкание V соответственно.

Для функции f:V->W пусть : 2V 2W, где /*(£/) = {/(ж) \x£U} для U CV.

Определение 2.30. Множество n-регионов W называется насыщенным, если

Vu € 3v е W (и С v), (1)

VueWV£>03veW (u<svCB(u,e)), (2) и е W Ve > 0 3v 6 W (-В(-и,е) СуШи), (3) и кроме того, существует открытая непрерывная функция / : Rn —> R, такая что для R 6 {С, D, <£, В)},

Vw G Vs € Яе^ (/„(u)ifc =Ф 3w е W°(uRwkf,(w) = 5)). (4)

Заметим, что свойство (2.4) соответствует так называемому свойству поднятия отображения /# шкалы (W°,R) в шкалу (7Zeg\,R).)

В частности, насыщенными являются множество замкнутых шаров, множество n-мерных параллелепипедов, множество всех п-регионов; более того, всякое непустое множество выпуклых регионов, замкнутое относительно гомотетий Rn, является насыщенным (предложение 2.34).

ТЕОРЕМА 2.32. Пусть W — насыщенное множество n-регионов, п > 1, R £ {С, D, <е, 3)}. Тогда логики шкал (W, R) и (W°,R) описываются следующей таблицей:

Ш> Э (s с

W lmi S4 ьм2 S4.2

W0 lm3 S4.1 lm2 S4.2

В параграфе 2.8 рассматриваются логики отношений сравнимости и несравнимости по отношениям -< и ^ в Ш.п, а также логики регионов, упорядоченных отношениями сравнимости и несравнимости но включению и компактному включению. Для этих логик доказывается невозможность аксиоматизации никаким множеством формул с ограниченным числом переменных, и следовательно, невозможность конечной аксиоматизации (теоремы 2.39, 2.40).

На основании результатов, полученных в главе 2, опубликованы работы [40], [41], [39], [б].

В Главе 3 рассматриваются модальные логики шкал вида (W, R,W х W), то есть бимодальные логики, в которых вторая модальность интерпретируется универсальным отношением.

В параграфах 3.1 — 3.3 изучаются общие вопросы введения универсальной модальности для логик так называемых антинаправленных шкал. Дадим необходимые определения.

Для шкалы $ — (W,R) пусть обозначает шкалу с дополнительным универсальным отношением: = (W, R, W х W). Для класса шкал F положим Ти = | £ € .F}.

Аксиоматически, универсальная модальность может быть введена следующим образом [20]: для одномодальной логики L пусть LU обозначает наименьшую бимодальную логику содержащую L и формулы

АТг3 = 33р 3р, ARefl3 = р Зр, ASymm3 = р V3р;

Ас = Ор -> 3р вместо связок ОьОг и двойственным к ним ПьПг, используются связки 0,3 и двойственные к ним Q, V).

Шкала (W,R) называется антинаправленной, если она удовлетворяет свойству Mx\/y3z(zRx A zRy). Это свойство выражается формулой А^ в обогащенном бимодальном языке: А* - Зр А Зд 3(0р А Од). Для одномодальной логики L пусть = LU + А-1. Таким образом, если Т некоторый класс антинаправленных шкал и L = L(.F), то L(^ru) Э LU^.

В диссертации получено достаточное условие для равенства этих логик. Для п > 1 пусть €п = (Wn,Wn х Wn), где \Wn\ — п; кроме того, пусть Со = (W\,0). Для транзитивных шкал $ и (J5, пусть обозначает их порядковую сумму.

ТЕОРЕМА 3.13. Рассмотрим класс транзитивных шкал Т, такой что

• всякая шкала £ € Т обладает рефлексивным корнем;

• если $ € Т и х G то + Е J7, где обозначает кои?/с в шкале $ с корнем х.

Тогда ЦГ1) = L(jc-)Ui.

Следствие 3.14. Пусть L — одномодальная транзитивная полная логика, такая что если # — L-конус, то и + £ — L-конус. Тогда

• LU^ — полна;

• если L — финитно аппроксимируема, то и LU1 — финитно аппроксимируема;

• L и LU^ полиномиально эквивалентны.

Из этих результатов, в частности, следует, что если L — одна из логик S4, S4.1, S4.2, LMi, LM2, LM3, то логика LUj — полна по Крипке и финитно аппроксимируема.

В параграфе 3.4 описываются логики конкретных антинаправленных шкал:

ТЕОРЕМА 3.22. Для п > 2, L((Rn, di)u) — S4.2U-''; L((Mn, = LM2U1.

ТЕОРЕМА 3.24. Пусть W — насыщенное множество n-регионов, п > 1. Тогда

L((W, Э)и) = S4U1, L((W°, Э)и) = S4.1U1; L((W, З)и) = LM1U1, L{(W°, Ш>)и) = LMaU1.

В Главе 4 исследуется алгоритмическая сложность построенных логик.

Для логики L — ЬМ1,ЬМг,ЬМз показано, что L-выполпимость формулы сводится к выполнимости формулы на некоторой L-шкале ограниченного ветвления, толщины и высоты (леммы 4.4, 4.5).

Для шкал ^иб, пусть £и0 обозначает дизъюнктную сумму этих шкал.

Определение 4.6. Для п,к> 1 индуктивно определим шкалы и %пк■ Положим n,i = Со + Ъп,к+1 = %п, 1 + (0i U • • • U 0„) где 0 ь • • • 1 0п шкалы, изоморфные %п,к-Пусть — шкала, полученная из добавлением над каждым невырожденным сгустком п штук вырожденных сгустков, т.е. V + u • • •U Ufo u • •. u&O, где ., 0n — изоморфны &— изоморфны £0.

Лемма 4.7. Пусть |5г/6(Л)| = п. Тогда

1. А LMi-выполнима & А выполнима в корне Тп,п;

2. А ЬМг-выполнима А выполнима в корне ТП)П + Сп;

3. А ЬМз-выполиима А выполнима в корне п или в

Явным образом описаны алгоритмы верификации формул на таких шкалах, использующие полиномиальное относительно длины формулы количество памяти, тем самым показана принадлежность проблемы выполнимости (разрешимости) логик LMi,LM2,LM3 классу PSPACE (теорема 4.15).

В параграфе 4.3 доказывается PSPACE-трудность проблемы выполнимости для логик LMi,LM2,LM3. Для этого используется метод Р. Ладнера (см. сноску 2), сводящий проблему общезначимости булевой формулы с кванторами к проблеме выполнимости модальной формулы на шкалах Крипке определённого вида ("кванторных деревьях").

Из этого следует, что логики LMi, LM2, LM3 PSPACE-полны.

Из PSPACE-полноты LMi,LM2,LM3 и результатов главы 3 следует также PSPACE-полнота бимодальных логик, рассмотренных в теоремах 3.22 и 3.24.

В Заключении приведены основные результаты и выводы диссертационной работы.

В Приложении приведён алгоритм проверки условной выполнимости модальных формул на шкалах вида

Заключение диссертации по теме «Теоретические основы информатики», Шапировский, Илья Борисович

Заключение

Приведём основные результаты диссертационной работы.

1. Построены полные конечные системы аксиом модальных логик ряда пространственных структур: для отношений включения на так называемых насыщенных множествах регионов и для отношения хронологического будущего в действительных пространствах;

2. Полностью изучены алгоритмические свойства построенных модальных логик: показана финитная аппроксимируемость (следовательно, разрешимость) и PSPACE-полнота.

3. Для ряда модальных логик пространственных структур показано отсутствие конечной аксиоматизируемости.

4. Исследованы модальные логики с дополнительной универсальной модальностью: получены теоремы о сохранении свойств (полноты по Кринке, финитной аппроксимируемости, алгоритмической сложности) при добавлении универсальной модальности для логик транзитивных антинаправленных шкал.

5. Построена аксиоматика ряда модальных логик регионов и релятивистских модальных логик в языке с универсальной модальностью; показана PSPACE-полнота этих логик.

Таким образом, в работе построен ряд полных модальных аксиоматик пространственных отношений, обладающих относительно невысокой

PSPACE) алгоритмической сложностью, и приведены разрешающие алгоритмы для этих логик.

Список литературы диссертационного исследования кандидат физико-математических наук Шапировский, Илья Борисович, 2007 год

1. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. - Москва: МЦНМО, 2002.

2. Колмогоров А.Н., Драгалин А.Г. Математическая логика. — Москва: УРСС, 2004.

3. Расева Е., Сикорский Р. Математика Метаматематики. — Москва: Наука, 1972.

4. Шапировский И. Б. О модальных логиках некоторых геометрических структур // Проблемы передачи информации. — 2007. — Т. 43, N2 3. — С. 97-104.

5. Эрлих П., Бим Д. Глобальная лоренцева геометрия. — Москва: МИР, 1985.

6. Blackburn P., de Rijke М., Venema Y. Modal Logic. — Cambridge University Press, 2001.

7. Chagrov A., Rybakov M. How many variables does one need to prove PSPACE-hardness of modal logics // Advances in Modal Logic. — Vol. 4. — London: King's College Publications, 2003. Pp. 71-82.

8. Chagrov A., Zakharyaschev M. Modal logic. — Oxford University Press, 1997.

9. Clarke E., Emerson E. Design and synthesis of synchronization skeletons using branching-time temporal logic // Proceedings of the Workshop on Logic of Programs, Yorktown Heights.— Vol. 131.— Springer, 1981. — Pp. 52-71.

10. Emerson E., Halpern J. Decision procedures and expressiveness in the temporal logic of branching time // STOC '82: Proceedings of the fourteenth annual ACM symposium on Theory of computing. — ACM Press, 1982.— Pp. 169-180.

11. Emerson E., Halpern J. "Sometimes" and "Not Never" revisited: On branching versus linear time // Symposium on Principles of Programming Languages. 1983. - Pp. 127-140.

12. Emerson E., Jutla C. The complexity of tree automata and logics of programs // SIAM Journal on Computing. — 2000.— Vol. 29, no. 1,— Pp. 132-158.

13. Fine K. Logics containing K4. part II. // Journal of Symbolic Logic. — 1985. Vol. 50, no. 3. - Pp. 619-651.

14. Fischer M., Ladner R. Prepositional modal logic of programs (extended abstract) // STOC '77: Proceedings of the annual ACM symposium on Theory of computing. 1977. - Pp. 286-294.

15. Fischer M., Ladner R. Propositional dynamic logic of regular programs // Journal of Computer and System Sciences. — 1979. Vol. 18, no. 2. — Pp. 194-211.

16. Goldblatt R. Diodorean modality in Minkowski spacetime // Studia Logi-ca. 1980. - Vol. 39. - Pp. 219-236.

17. Goranko V., Montanari A., Sciavicco G. A road map on interval temporal logics and duration calculi // Journal of Applied Non- Classical Logics.— 2004. Vol. 14, no. 1. - Pp. 9-54.

18. Goranko V., Passy S. Using the universal modality: Gains and questions // Journal of Logic and Computation. — 1992. — Vol. 2, no. 1. — Pp. 5-30.

19. Halpern J., Shoham Y. A propositional modal logic of time intervals // Proceedings 1st Annual IEEE Syrnp. on Logic in Computer Science, LICS'86, Cambridge, MA, USA, 16-18 June 1986.- Washington, DC: IEEE Computer Society Press, 1986. Pp. 279-292.

20. Hemaspaandra E. The price of universality // Notre Dame Journal of Formal Logic. 1996. - Vol. 37, no. 2. - P. 174-203.

21. Hennessy M., Milner R. On observing nondeterminism and concurrency // Automata, Languages and Programming, 7th Colloquium, Noordweijker-hout, The Nethcrland, Proceedings. — Vol. 85 of Lecture Notes in Computer Science. — Springer, 1980. — Pp. 299-309.

22. Hennessy M., Milner R. Algebraic laws for nondeterminism and concurrency // Journal of the Association for Computing Machinery. — 1985. — Vol. 32.-Pp. 137-161.

23. Ladner R. The computational complexity of provability in systems of modal propositional logic // SIAM Journal on Computing. — 1977. — Vol. 6, no. 3. Pp. 467-480.

24. Lutz C., Wolter F. Modal logics of topological relations // Logical Methods in Computer Science. — 2006. — Vol. 2, no. 2. Paper 5.

25. Many-dimensional modal logics: theory and applications / D. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev. — Elsevier Science, 2003.

26. Milner R. Calculi for synchrony and asynchrony // Theoretical Computer Science. 1983. - Vol. 25. - Pp. 267-310.

27. On the temporal analysis of fairness / D. Gabbay, A. Pnueli, S. She-lah, J. Stavi // POPL '80: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages.— ACM Press, 1980. Pp. 163-173.

28. Pnueli A. The temporal logic of programs // Proceedings of the 18th IEEE Symposium on Foundations of Computer Science. — IEEE, 1977. — P. 46-57.

29. Pratt V. Semantical considerations on Floyd-Hoare logic // Proceedings 17th IEEE Symposium on Foundations of Computer Science. — Cambridge, USA: Massachusetts Institute of Technology, 1976.- Pp. 109-121.

30. Pratt V. A near-optimal method for reasoning about action // Journal of Computer and System Sciences. — 1980. — Vol. 20, no. 2. — Pp. 231-254.

31. Schmidt-Schauss M., Smolka G. Attributive concept descriptions with complements // Artificial Intelligence. — 1991. — Vol. 48. — Pp. 1-26.

32. Segerberg K. A completeness theorem in the modal logic of programs // Notices of the American Mathematical Society. 24:A-552. — 1977.

33. Shapirovsky I. PSPACE-decidability of modal logics via selective filtration // Proceedings of the 3-rd Moscow-Vienna Workshop on Logic and Computation. — Moscow: 2004. — P. 10.

34. Shapirovsky I. PSPACE-decision procedure for some transitive modal logics // Proceedings of the International Conference "AiML-2004: Advances in Modal Logic". University of Manchester, UK: 2004. - Pp. 331-343.

35. Shapirovsky I. On PSPACE-decidability in transitive modal logic // Advances in Modal Logic. — Vol. 5. — London: King's College Publications, 2005. Pp. 269-287.

36. Shapirovsky I. Downward-directed transitive frames with universal relations // Advances in Modal Logic. — Vol. 6. — London: College Publications, 2006. Pp. 413-428.

37. Shapirovsky I. Modal logics of closed domains on Minkowski plane // Journal of Applied Non-Classical Logics. — 2007.— Vol. 17, no. 3.— Pp. 283316.

38. Shapirovsky I., Shehtman V. Chronological future modality in Minkowski spacetime // Advances in Modal Logic. — Vol. 4. — London: King's College Publications, 2003. Pp. 437-459.

39. Shapirovsky I., Shehtman V. Modal logics of regions and Minkowski space-time // Journal of Logic and Computation. — 2005. — Vol. 15. — Pp. 559574.

40. Shapirovsky /., Shehtman V. RCC-relations and relativistic time // Proceedings of the international conference "Computer science applications of modal logic" / Independent University of Moscow. — Moscow: 2005. — P. 37.

41. Shehtman V. Modal logics of domains on the real plane // Studia Logica. — 1983.-Vol. 42.-Pp. 63-80.

42. Shehtman V. On some two-dimensional modal logics // 8th International Congress on Logic, Methodology, and Philosophy of Science. — Moscow: 1987. Pp. 326-330.

43. Stockmeyer L., Meyer A. Word problems requiring exponential time (preliminary report) // STOC '73: Proceedings of the fifth annual ACM symposium on Theory of computing.— New York, NY, USA: ACM Press, 1973. Pp. 1-9.1. Указатель терминов