автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Алгоритмические свойства модальных логик информационных систем

На правах рукописи

Шапировский Илья Борисович

Алгоритмические свойства модальных логик информационных систем

05 13 17 - теоретические основы информатики, 01 01 06 - математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

□□3 174195

Москва 2007

003174195

Работа выполнена в Институте проблем передачи информации им А А Харкевича РАН

Научный руководитель:

Официальные оппоненты:

доктор физико-математических наук, профессор В Б Шехтман

доктор физико-математических наук, профессор М Р Пентус

кандидат физико-математических наук, доцент М Н Рыбаков

Ведущая организация:

Математический институт им В А Стеклова РАН

Защита диссертации состоится «_» _ 2007 года в_часов на

заседании диссертационного совета Д 002 077 01 при Институте проблем передачи информации им А А Харкевича РАН по адресу 127994, г Москва, ГСП-4, Большой Каретный пер , д 19

С диссертацией можно ознакомиться в библиотеке Института проблем передачи информации им А А Харкевича РАН

Автореферат разослан «28» сентября 2007 года

Ученый секретарь

диссертационного совета Д 002 077 01, доктор физико-математических наук

И И Цитович

Общая характеристика работы

Актуальность темы. При построении и анализе сложных информационных

систем во многих случаях оказывается невозможным оперировать с

точным численным описанием системы это может быть связано как с

недоступностью такого описания, так и с практической невозможностью его

обработки В таких случаях возникает задача описания системы средствами

формальных языков Используемый при этом формальный язык должен

быть, с одной стороны, достаточно выразительным для отражения

содержательных свойств системы, с другой стороны — предлагаемое

описание должно быть приемлемым с алгоритмической точки зрения

Удобным формализмом для такого (качественного) описания оказываются

пропозициональные модальные логики

С точки зрения математической логики, модальные логики являются

логиками второго порядка, и потому в них могут быть описаны

свойства, невыразимые в классических первопорядковых логиках

Кроме того, для модальных логик характерна относительно невысокая

алгоритмическая сложность, что оказывается принципиальным для их

реальных приложений

Как область математической логики, модальная логика возникла в

середине прошлого века В 1960—1970 гг были развиты математические

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

финитной аппроксимируемости, разрешимости, и др1 Было начато

исследование алгоритмической сложности модальных логик2 В конце

70-х годов 20-го века начался новый этап — появляются многочисленные

приложения модальных логик в информатике, такие как динамические

логики вычислимости3, логики параллельности4,5, логики алгебр

процессов6 В задачах искусственного интеллекта активно используются

хСм , например, Blackburn Р, de Rijke М, Venema Y Modal Logic — Cambridge University Press, 2001

2Ladner R The computational complexity of provability m systems of modal prepositional logic // SIAM J Comput - 1977 - Vol 6, no 3 - Pp 467-480

3 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 109121

iPnuelt A The temporal logic of programs // Proceedings of the 18th IEEE Symposium on Foundations of Computer Science — IEEE, 1977 — Pp 46-57

5 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

6ffennessy M, Miner R On observing nondetermmism and concurrency // Automata, Languages and

модальные логики представления знаний7, в том числе так называемые пространственные модальные логики, предназначенные для качественного анализа пространственной информации8 Таким образом, в настоящее время модальная логика оформилась как самостоятельная дисциплина на стыке информатики и математической логики с широким кругом приложений

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

В модальных логиках подобный подход для решения задач информатики впервые был описан в работе Халперна и Шохема, где введены модальные логики временных интервалов9 Предложенный подход оказался эффективным при решении задач верификации моделей программ, спецификации систем реального времени, компьютерной лингвистики10 Как было замечено позднее11, подход Халперна и Шохема естественным образом обобщается на многомерный случай для решения задач представления пространственной информации аналогом интервалов являются регионы в действительном (или ином топологическом или метрическом) пространстве Однако на этом пути был получен ряд отрицательных результатов оказалось, что различные многомодальные логики регионов являются неразрешимыми или даже неперечислимыми12 Таким образом, возникает задача построения модальных логик регионов, с одной стороны, достаточно выразительных, с другой — разрешимых

Programming, 7th Colloqmum, Noordweijkerhout, The Netherland, Proceedmgs — Vol 85 of Lecture Notes tn Computer Science — Springer, 1980 — Pp 299-309

7Schmidt-Schauss M, Smolka G Attributive concept descriptions with complemente // Artificial Intelh-gence — 1991 — Vol 48 — Pp 1-26

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

9Halpern J, Shoham Y A propositional modal Iogic of time mtervals // Proceedmgs lst Annual IEEE Symp on Logic m Computer Science, LICS'86, Cambridge, MA, USA, 16-18 June 1986 — Washington, DC IEEE Computer Society Press, 1986 - Pp 279-292

10См , например, обзорную работу Goranko V, Montarían A , Scumcco G A road тар on mterval temporal logics and duration calculi // Journal of Applied Non-Classtcal Logtcs — 2004 — Vol 14, no 1 — Pp 9-54

xlLutz С, Wolter F Modal logics of topological relations // Logical Methods гп Computer Science — 2006 — Vol 2, no 2 —Paper 5

12 См там же

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

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

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

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

— о разрешимости и PSPACE-полноте

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

В работе В Б Шехтмана14 было замечено, что изучение свойств релятивистских модальных логик может быть использовано при исследовании модальных логик интервалов В диссертации эта взаимосвязь распространяется на многомерный случай Постановка задачи о релятивистских модальных логиках принадлежит А Прайору15 Первые конкретные примеры таких логик — для отношения причинного будущего

— были построены Р Голдблаттом16 и В Б Шехтманом17 Вопрос о модальной аксиоматизации отношения хронологического будущего долгое время оставался открытым, его решение излагается в диссертации

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

13См там же

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

15Prior A Past, Present and B\iture — Oxford University Press, 1967

16 GoldblattR Diodorean modality in mmkowski spacetime // Studia Lógica — 1980 — Vol 39 — Pp 219236

17Shehtman V Modal logics of domains on the real plane // Studia Lógica — 1983 — Vol 42 — Pp 63-80

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

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

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

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

Публикации. По теме диссертации опубликовано десять работ, из них три — совместно с В Б Шехтманом

Структура диссертации Диссертация состоит из введения, четырех глав, заключения, приложения, списка литературы и указателя терминов Общий объем диссертации —112 страниц Диссертация содержит 14 рисунков и 2 таблицы Список литературы содержит 45 наименований

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

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

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

Множество п-модальных формул FM{Oi, , Оп) строится из счетного множества пропозициональных переменных PV = {pi,p2, }> пропозициональной константы _1_ (ложь), двуместной связки —> (импликация), и одноместных связок Оъ , 0« (модальности типа "возможно") следующим образом

• ±,Р!,Р2, формулы,

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

• Если А — формула, то 0гА — формула, г = 1, ,п

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

ОгА = -iO«-1 А (модальности типа "неодходимо")

Для формулы А пусть Sub(A) обозначает множество всех ее подформул

п-модальной логикой называется множество те-модальных формул L С FM( Oi, , О«), такое что

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

• L содержит формулы г = 1, , п,

• L содержит формулы 0г(рх V р2) OzPi V 0гр2, г = 1, ,п,

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

Мопг А В е L 0гА 0гВ е L

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

Для п-модальной логики Ь и множества формул Ф С РМ(Ох, , 0П), Ь + Ф обозначает наименьшую п-модальную логику, содержащую ЬиФ п-модальная логика Ь называется конечно аксиоматизируемой, если Ь = К„ + Ф для некоторого конечного Ф Если Ф = {А}, то пишем Ь + А вместо Ь + {А} Ь I-А обозначает А е Ь

п-модалъной шкалой Крипке (или просто п-шкалой) $ называется кортеж (И7, К\, , Кп), где }¥ — непустое множество и /?х, , Нп С \¥ х\¥ Оценкой на шкале $ называется отображение

в ру —э.

Моделью (Крипке) ЗЛ над шкалой $ называется пара (£, где в — оценка на # Для всякой модальной формулы А £ РМ(Ох, , 0П) индуктивно определяется истинность формулы А в точке х модели Ш (обозначение

- Ж, х И А)

Ш,х & ±,

ал,х Ир о х е в(р),

2Л, ж I= А^ В ал, X У А или Ж, X \= в,

аЛ, х 1= ()гА -фф- для некоторого у имеем хР^у и £Ш:, у И А

Формула А называется истинной в модели ЗЛ (обозначение ЭЛ 1= А), если она истинна во всех точках этой модели Формула А называется общезначимой в шкале # (обозначение Л), если она истинна в любой модели над $ А называется общезначимой в классе шкал Т (обозначение ^ N А), если А общезначима в любой шкале # € 3- Множество всех формул, общезначимых в классе Т будем обозначать через Ь(^)

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

Хорошо известно, что если Т - класс п-шкал, то является п-

модальной логикой Логика Ь называется полной относительно класса шкал О-, если Ь = Ь называется полной (по Крипке), если она

полна относительно некоторого класса шкал Ь называется финитно

аппроксимируемой, если она полна относительно некоторого класса конечных шкал

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

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

X < V <£> (Уг~ Хг)2 ^ (уп ~ Хп)2 и Хп < уп,

1<г<те-1

X (Уг~ Хг)2 < (уп - Хп)2 и Хп<уп

1<г<п-1

Эти отношения транзитивны, и ^ рефлексивно Хорошо известно, что модальные логики К4 = К + 00Р —> 0Р, Б4 = Б + 00Р 0Р характеризуются классом всех транзитивных и классом всех транзитивных рефлексивных шкал соответственно Таким образом, Ь(М™, -<) Э К4 и Ь(Е", 2 Точная аксиоматизация логик причинного будущего была дана в работах Р Голдблатта и В Б Шехтмана Было показано, что возникающие логики — это Б4 и ее хорошо известные расширения

Э4 1 = Б4 + ПОр 0Пр, Б4 2 = Э4 + 0Цр ПОр

А именно, что для п ^ 2, Ь(К™, = 84 2 (Голдблатт, 1980, см сноску 16), кроме того, для области V в Ж2, ограниченной регулярной кривой, Ь(V, = Б4, Ь(С1/, = Б4 1, где СУ обозначает замыкание У (Шехтман, 1983, см сноску 17)

В диссертации доказаны аналогичные результаты для отношения -< В отмеченной выше работе Р Голдблатта было замечено, что свойство 2-плотности

УхУугУу2(хКу1 А хЯуъ —> Зг(хЯг А гВ,у\ А гДг/г)), которым обладает отношение -< в М™, выражается модальной аксиомой

АБе^ = Орг А 0р2 0(0рх А 0р2)

Для 2-плотных логик

ЬМ1 = К4 + АБепэг + ОТ, ЬМ2 = ЬМх + ОПр^ПОр, ЬМ3 = К4 + АБелвг + ОТ ОПТ,

в диссертации доказаны следующие результаты ТЕОРЕМА 2 23 Для п > 2, Ь(Ж", -<) = ЬМ2

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

• ВД -<) = ЬМь

• ЦСУ, -<) С ЬМ3,

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

Для доказательства этих теорем используется модификация метода из работ Р Голдблатта и В Б Шехтмана Существенным при этом является финитная аппроксимируемость исследуемых логик Хорошо известно, что логика Б4 и рассмотренные выше ее расширения Б4 1, Б4 2 обладают этим свойством для этих логик (как и для многих других) применим метод "эпи-фильтраций" Леммона-Сегерберга Однако в случае логик, содержащих аксиому АВепБг, этот метод неприменим непосредственно, так как фильтрации такого рода не сохраняют свойство 2-плотности Таким образом, именно доказательство финитной аппроксимируемости (теоремы 2 12—2 14) представляло принципиальную сложность при исследовании логик ЬМГ ТМ3 и при получении изложенных выше теорем Требуемый результат был получен при использовании метода селективной фильтрации в сочетании с методом максимальных точек в канонической модели

В параграфах 2 6 и 2 7, на основании результатов, полученных в параграфах 2 1—2 5, строятся аксиоматики модальных логик регионов в действительном пространстве

Компактное множество и С Ж™ называется регионом в Ж™, или п-регионом, если С/ является замыканием непустой области

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

TZegn — множество всех гг-регионов,

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

Вп — множество всех замкнутых шаров,

^■п = |п[агА] I [aii^i]> >[aii,bn] е ~~ множество всех п-мерных параллелепипедов

Для множества гг-регионов W пусть W° обозначает расширение W всеми одноэлементными множествами W° = W U {{X} | X € Мп}

Определим отношение компактного включения <ё для множеств U, V С Кп положим

и <ё V CU С IV, 5>=<ё-\ где IV и СУ обозначают внутренность и замыкание V соответственно

Для функции / V->W пусть /„ - 2W, где /.(17) = {/(х) | xeU} для и с V

Определение 2 30 Множество гг-регионов W называется насыщенным, если Vu 6 Вп 3v е W («Си), (1)

Vu € W Ve > 0 Эо е VT (и <Ш v С В(и, е)), (2)

VixGffVe>03t)eW (-B(-u,e) С v Ш и), (3)

и кроме того, существует открытая непрерывная функция / К™ —> К, такая что для R е {С, Э, <ш, э>},

V« еГУзе Яед\ (f*{u)Rs ^Згоб W°(uRw&f*{w) = в)) (4)

(Заметим, что свойство (4) соответствует так называемому свойству поднятия отображения /» шкалы (W°, R) в шкалу (IZegl, R) )

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

ТЕОРЕМА 2 32 Пусть W — насыщенное множество гг-регионов, п > 1, Тогда логики шкал (W,R) и (W°,i?) описываются

следующей таблицей

э> D <£ с

W lmx s4 lm2 s4 2

w° lm3 s4 1 lm2 s4 2

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

На основании результатов, полученных в главе 2, опубликованы работы

[1]. [6], Щ, [10]

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

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

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

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

АТгд = ЗЗр —> Зр, ARefig = р -> Зр, ASymm3 =р—> V3р, Ас = 0р Зр

(вместо связок Oi, Ог и двойственным к ним СЗьСЬ, используются связки 0,3 и двойственные к ним □, V)

Шкала (W,R) называется антинаправленной, если она удовлетворяет свойству ^x\/y3z{zRx A zRy) Это свойство выражается формулой А* в обогащенном бимодальном языке А* = Зр A 3q —> 3(0р A ()q) Для одномодальной логики L пусть LU* = LU + А* Таким образом, если J— некоторый класс антинаправленных шкал и L = L(.Т7), то ЦТ") 3 LU* В диссертации получено достаточное условие для равенства этих логик Для n ^ 1 пусть €п = (W„,Wn х Wn), где |W„| = п, кроме того, пусть

18 Goranko V, Passy S Using the universal modality Gams and questions //J Log Comput — 1992 — T 2, № 1 - С 5-30

Со = 0) Для транзитивных шкал # и ©, пусть $ + © обозначает их порядковую сумму

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

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

• если $ € 3- и х € то (£1 + £ 3-, где обозначает конус в шкале 3" с корнем х

Тогда ЦГ1) = Ц^и1

Следствие 3 14 Пусть Ь — одномодальная транзитивная полная логика, такая что если § — Ь-конус, то и £1 + $ — Ь-конус Тогда

• — полна,

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

• Ь и полиномиально эквивалентны

Из этих результатов, в частности, следует, что если Ь — одна из логик Б4, Б4 1, Б4 2, ЬМх, ЬМг, ЬМз, то логика — полна по Крипке и финитно аппроксимируема

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

ТЕОРЕМА 3 22 Для п 2, ь((кп, г<)и) = Б4 ги1, ь((жп, -<)и) = ьм2их

ТЕОРЕМА 3 24 Пусть Ш — насыщенное множество п-регионов, п '^1 Тогда

= 8411*, 2)") = Б4

з>) ) = ЬМхи1, з>)") = ЬМ3их

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

Для логики L = LMi, LM2, LM3 показано, что L-выполнимость формулы сводится к выполнимости формулы на некоторой L-шкале ограниченного ветвления, толщины и высоты (леммы 4 4, 4 5)

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

19

шкал

Определение 4 6 Для п, к ^ 1 индуктивно определим шкалы и 1* к Положим

= Со + + (<5i LI U <8n),

где , <&n — шкалы, изоморфные 1п,к

Пусть — шкала, полученная из добавлением над каждым

невырожденным сгустком п штук вырожденных сгустков, т е

= + (& U □ £!U+i = + (®i u " U0„U^iU LI&,), где (Si, , <5n — изоморфны Si, , — изоморфны Co

Лемма 4 7 Пусть \Sub(A) \ = те Тогда

1 A LMi-выполнима Л выполнима в корне ТП)П,

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

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

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

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

19 Определение понятия дизъюнктной суммы шкал может быть найдено в Chagrov Л , Za-kharyaschev М Modal logic — Oxford University Press, 1997

Из этого следует, что логики ЬМь ЬМ2, ЬМ3 РБРАСЕ-полны

Из РБРАСЕ-полноты ЬМ1; ЬМ-2, ЬМ3 и результатов главы 3 следует также РБРАСЕ-полнота бимодальных логик, рассмотренных в теоремах 3 22 и 3 24

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

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ И ВЫВОДЫ

Основными результатами диссертации являются следующие

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

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

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

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

5 Построена аксиоматика ряда модальных логик регионов и релятивистских модальных логик в языке с универсальной модальностью, показана РЯРАСЕ-полнота этих логик

Таким образом, в работе построен ряд полных модальных аксиоматик пространственных отношений, обладающих относительно невысокой (РБРАСЕ) алгоритмической сложностью, и приведены разрешающие алгоритмы для этих логик

СПИСОК РАБОТ, ОПУБЛИКОВАННЫХ ПО ТЕМЕ ДИССЕРТАЦИИ

[1] 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

В работе [1] В Б Шехтману принадлежит идея доказательства финитной аппроксимируемости, И Б Шапировскому принадлежит конструкция р-морфного отображения области пространства Минковского в бесконечное дерево

[2] Shapirovsky I PSPACE-decision procedure for some transitive modal logics // Proceedings of the International Conference "AiML-2004 Advances m Modal Logic" — University of Manchester, UK 2004 — Pp 331-343

[3] 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

[4] Shapirovsky I On PSPACE-decidability m transitive modal logic // Advances m Modal Logic — Vol 5 — London King's College Publications, 2005 - Pp 269-287

[5] Shapirovsky I, 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

[6] Shapirovsky I, Shehtman V Modal logics of regions and Minkowski spacetime // Journal of Logic and Computation — 2005 — Vol 15 — Pp 559574

В работах [5] и [6] В Б Шехтману принадлежит идея интерпретации регионов как типов информации в духе Колмогорова—Медведева, а также идея доказательства отстутствия конечной аксиоматики модальных логик регионов с помощью характеристических шкал, для конкретных логик такие шкалы были найдены И Б Шапировским, которому также принадлежат положительные результаты об аксиоматизации множеств регионов

[7] Shapirovsky I Downward-directed transitive frames with universal relations // Advances m Modal Logic — Vol 6 — London College Publications, 2006 - Pp 413-428

[8] Шапировский И Б О свойствах некоторых транзитивных логик с универсальной модальностью // Труды XXVIII Конференции молодых ученых механико-математического факультета МГУ — Москва 2006 — С 233-236

[9] Shapirovsky I Modal logics of closed domains on Minkowski plane // Journal of Applied Non-Classical Logics — 2007 — Vol 17, no 3 — Pp 283-316

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

Отпечатано в ООО «Диалог-Реклама» Подписано в печать 35 09 2004г Объем 1 п л Формат 60x90/16 Тираж 100 экз Заказ Ш25/09-ЗТ

105066, г Москва, ул Спартаковская, д 13

Введение

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) алгоритмической сложностью, и приведены разрешающие алгоритмы для этих логик.

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. Указатель терминов