Алгоритм распознавания выполнимости формул логики ветвящегося времени и его применение

• Автор: Хелемендик, Роман Викторович
• Шифр специальности: 01.01.09
• Научная степень: Кандидатская
• Год защиты: 2005
• Место защиты: Москва
• Количество страниц: 155 с.

Глава 1. Формулировка алгоритма

§1. Логика ветвящегося времени. Основные понятия

§2. Построение схемы модели

§3. Фильтрование схемы модели

§4. Построение модели

Глава 2. Обоснование алгоритма

§5. Свойства правил алгоритма

§6. Завершаемость алгоритма

§7. Корректность алгоритма

§8. Полнота алгоритма

§9. Схемы моделей и суммарные схемы моделей

Глава 3. Применение алгоритма
§10. Построение вывода общезначимых формул из аксиом
§11. Пример применения алгоритма к решению шахматной
задачи
Заключение
Литература

Проблема распознавания выполнимости формул в логике имеет большое теоретическое значение и тесно связана с прикладными задачами. Если задача записывается в виде формулы, то выполнимость формулы означает существование решения задачи, а модель, в которой эта формула истинна, даёт решение задачи. Проблема распознавания выполнимости формул в логике высказываний разрешима, однако язык этой логики предоставляет весьма ограниченные выразительные возможности. В то же время в логике предикатов проблема распознавания выполнимости алгоритмически неразрешима, что было доказано Чёрчем [32]. Поиски других достаточно выразительных расширений языка логики высказываний привели к созданию модальных логик [31,38], получаемых путём добавления специальных операторов (“модальностей”) и расширения интерпретации пропозициональных переменных. Дальнейшее развитие и комбинирование модальных логик, связанные, в частности, с решением прикладных задач, рассмотрены в монографии [37]. Одной из модальных логик, ориентированных на изучение процессов, происходящих во времени, является так называемая логика ветвящегося времени, известная под названием Ctl - Computational tree logic [36].
В этой логике к пропозициональным связкам добавляются следующие временные: “О” - “в следующий момент”, - “во всякий момент”, “О” - “в некоторый момент”, “75” - “до тех пор, пока”, а также кванторы “V” и “3”, стоящие перед каждой временной связкой (и только перед ней). Истинность формулы определяется в модели: в вершинах связного ориентированного графа, в котором каждой вершине приписаны истинностные значения пропозициональных переменных. Формула называется выполнимой, если существует модель, в начальной вершине которой эта формула истинна. Формула называется общезначимой, если она истинна во всякой модели.
Разрешимость проблемы распознавания выполнимости формул в Ctl доказана в работе [34] путём построения для формулы конечной

структуры (структуры Хинтикки) и её анализа, после которого даётся ответ о выполнимости этой формулы. К распознаванию выполнимости формулы Си сформировались два подхода: автоматный и табличный. В первом подходе по формуле строится автомат специального вида, и выполнимость формулы сводится к существованию непустого языка, принимаемого этим автоматом [41]. При таком подходе, однако, не проявляется связь разбора формулы с содержанием задачи, которое отражено в структуре формулы. При табличном подходе применение каждого правила имеет простой содержательный смысл. Наш алгоритм относится ко второму подходу.
Табличный подход основан на методе семантических таблиц, впервые предложенном Бетом [30], и для разрешимых модальных логик изложен в работе [31]. Табличный метод в схематическом виде для СИ был впервые изложен в работе [34]. Несколько подробнее табличный метод для СИ был опубликован в работе [36]. Этот метод состоит из построения по формуле конечного табличного графа, его анализа и построения по нему модели в случае выполнимости. Отметим, что в работах [34,36] на граф в модели наложено ограничение в виде тотальности: каждая вершина графа должна иметь сына. Кроме того, некоторые случаи, возникающие, в частности, при построении новых вершин в графе, удалении вершин, проверки подтверждённости так называемых формул-обещаний, в этих работах не рассмотрены. Доказательства корректности, полноты и оценки сложности также даны в виде наброска. В связи с этим использование данного алгоритма, включая построение модели в случае выполнимости, а также доказательство невыполнимости, наталкивается на серьёзные трудности.
Таким образом, оставались актуальными вопросы создания детального табличного алгоритма, его обоснования и применения к решению прикладных задач. Кроме того, согласно работам Эмерсона [34,36], табличные графы имеют вообще говоря экспоненциальное число вершин, поэтому актуален вопрос: всегда ли для ответа на вопрос о выполнимости формулы необходимо полностью строить эту структуру, или существуют случаи, когда достаточно некоторого её

общезначима; здесь Хс, есть х.ф. вершины С,-т после применения к ней правил 3-5, Су - вершина, добавленная в правиле 5, и х'с, ~ ес
т 'та
х.ф. после применения этого правила к вершине С,т. Рассмотрим 3 случая:
Случай 1 — правило 3. Если вводимая в этом правиле формула О' уже содержалась до применения этого правила в соответствующем множестве формул в вершине С,т, то х'с совпадает с Хс1т и тогда из общезначимости по лемме 5.3 формул хс,-га = Хс,т и Хс,т = Хс,т следует общезначимость формулы Хс,т = Хс, ) что Даёт общезначимость и формулы ха = (хс,ч V... V Хс,га V... V хс,,)- Иначе Хс,т есть Хс,т Л фр. Тогда повторяя рассуждения из случая 1 доказательства леммы 5.2 получаем общезначимость формулы фд = фд<. Так как фд является конъюнктивным членом формулы Хс 5 либо совпадает с ней, то формула (Хс,т Фв)I а, следовательно, и формула (хс,- Фв') общезначимы. Последнее даёт общезначимость формулы (Хс,т ~^ (Хс,т ^Фв1)), т.е. формулы (хс,га -> Хс1т)- Поскольку формула (хс,т -> Хс,т)> Т-е-формула ((хс,га А фв') -> Хс1т), общезначима, то формула Хс,т = Хс,га> а, следовательно, и формула хс,т = Хс, общезначимы. Отсюда и из индукционного предположения следует общезначимость формулы
ХА = (Хс.ч V ... V Хс,т V ... V хс,,)-
Случай 2 - правило 4: а) 0+ = Т+, Ь) в~ = ±~, с) 0+ = (<рЛф)+, <4) в~ — (<р V ф)~, е) в~ = —» V1)-) 0 $+ = -,¥>+> ё) В случае
а) формула хс, имеет вид Хс, А Т, а в случае Ь) - Хс, А ->Т, поэтому в обоих случаях общезначимость формулы хс, = Хс, очевидна. В случаях Г) и g) общезначимость формулы хс( = Хс, устанавливается путём повторения рассуждений из случая 1 этой леммы и случаев ^ и g) в случае 2 в доказательстве леммы 5.2. Если рассматриваемые в случае 2 с)-е) в этом доказательстве формулы в[ и 0'2, положительность и отрицательность которых определена в упомянутом доказательстве, уже содержались до применения правила 4 в соответствующих множествах формул в вершине С{гп, то Хс,т совпадает с Хс и тогда из общезначимости по лемме 5.3 формул хс. = Хс и
•ш т 1щ
Хс,т = Хс, следует общезначимость формулы хс,га = Хс, • Иначе в