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

Актуальность темы

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

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

Как область математической логики, модальная логика возникла в середине прошлого века. В 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−22 003) и 'Геометрические модальные логики' (№ 06−01−72 555).

Публикации. По теме диссертации опубликованы работы [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.

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

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