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

Проблема распознавания выполнимости формул в логике имеет большое теоретическое значение и тесно связана с прикладными задачами. Если задача записывается в виде формулы, то выполнимость формулы означает существование решения задачи, а модель, в которой эта формула истинна, даёт решение задачи. Проблема распознавания выполнимости формул в логике высказываний разрешима, однако язык этой логики предоставляет весьма ограниченные выразительные возможности. В то же время в логике предикатов проблема распознавания выполнимости алгоритмически неразрешима, что было доказано Чёрчем [32]. Поиски других достаточно выразительных расширений языка логики высказываний привели к созданию модальных логик [31,38], получаемых путём добавления специальных операторов («модальностей») и расширения интерпретации пропозициональных переменных. Дальнейшее развитие и комбинирование модальных логик, связанные, в частности, с решением прикладных задач, рассмотрены в монографии [37]. Одной из модальных логик, ориентированных на изучение процессов, происходящих во времени, является так называемая логика ветвящегося времени, известная под названием Ctl — Computational tree logic [36].

В этой логике к пропозициональным связкам добавляются следующие временные: «О» — «в следующий момент», «?» — «во всякий момент», «О» — «в некоторый момент», «15» — «до тех пор, пока», а также кванторы «V» и «3», стоящие перед каждой временной связкой (и только перед ней). Истинность формулы определяется в модели: в вершинах связного ориентированного графа, в котором каждой вершине приписаны истинностные значения пропозициональных переменных. Формула называется выполнимой, если существует модель, в начальной вершине которой эта формула истинна. Формула называется общезначимой, если она истинна во всякой модели.

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

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

Таким образом, оставались актуальными вопросы создания детального табличного алгоритма, его обоснования и применения к решению прикладных задач. Кроме того, согласно работам Эмерсона [34,36], табличные графы имеют вообще говоря экспоненциальное число вершин, поэтому актуален вопрос: всегда ли для ответа на вопрос о выполнимости формулы необходимо полностью строить эту структуру, или существуют случаи, когда достаточно некоторого её фрагмента?

Система аксиом и правил вывода для логики ветвящегося времени вместе с доказательством её полноты приведены в работе [34]. Подстановка формул в эти аксиомы и использование правил вывода теоретически позволяют перечислить все возможные выводы общезначимых формул из аксиом. Однако такой путь практически не даёт вывода данной произвольной формулы из этих аксиом. В связи с этим для Си также возникает вопрос описания эффективного метода построения вывода всякой общезначимой формулы из аксиом.

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

По классификации А. А. Ляпунова и С. В. Яблонского [10,26] шахматная позиция является одной из управляющих систем (У.С.), обладающей структурой и функционированием. Таким образом, проблему нахождения решения шахматной задачи можно рассматривать как пример синтеза У.С. В качестве примера такой задачи нами выбран этюд К. Эберса [15], являющийся одной из самых сложных задач, относящихся к шахматной теории систем полей соотоветствия [24]. Условие этой задачи записано в виде конъюнкции трёх формул: формулы, соответствующей начальным положениям фигур, формулы, описывающей возможные ходы, и формулы-цели, достижение которой равносильно получению требуемого результата. Применение авторского алгоритма распознавания выполнимости к этой формуле дало модель, по которой получено полное решение данного этюда — первый ход и дальнейшие ответы на любой из ходов соперника в каждой из возникающих позиций.

Настоящая диссертация состоит из введения, трёх глав, разбитых на 11 параграфов, заключения и списка литературы.

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

1. Построен алгоритм, распознающий выполнимость формул логики ветвящегося времени и строящий для любой выполнимой формулы модель. Дано доказательство корректности и полноты этого алгоритма.

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

3. Сформулирован алгоритм эффективного построения вывода общезначимых формул из аксиом и доказана его полнота.

4. Приведён пример применения алгоритма к решению шахматной задачи. Условие задачи записано в виде формулы логики ветвящегося времени, выполнимость которой означает существование решения, и это решение получено по модели, построенной для формулы.

Заключение

.