Алгоритм распознавания выполнимости формул логики ветвящегося времени и его применение тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

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

Хелемендик Роман Викторович

АЛГОРИТМ РАСПОЗНАВАНИЯ ВЫПОЛНИМОСТИ ФОРМУЛ ЛОГИКИ ВЕТВЯЩЕГОСЯ ВРЕМЕНИ И ЕГО ПРИМЕНЕНИЕ

01.01.09-дискретная математика и математическая кибернетика

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук

Москва - 2005

Работа выполнена в Институте прикладной математики им. М.В.Келдыша РАН

Научный рукодогель: доктор физико-математических наук Янов Юрий Иванович

Официальные оппоненты: доктор физико-математических наук, профессор, Мошков Михаил Юрьевич

кандидат физико-математических наук, Мадатян Хикар Асилбекович

Ведущая организация: Московский государственный университет им. М.В .Ломоносова

Защита состоится " 2005 г. в /5" час. на заседании

Диссертационного совета Д 002.017.02 при Вычислительном центре им.

А.А.Дородницына Российской академии наук по адресу: 119991, Москва, ул. Вавилова, д. 40.

С диссертацией можно ознакомиться в библиотеке Вычислительного центра им. А.А.Дородницына Российской академии наук.

Автореферат разослан " " ЯН^вЛЯ 2005 г.

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

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

В В Рязанов

ém^L W93G

m

Актуальность темы. Проблема распознавания выполнимости формул в логике имеет большое теоретическое значение и тесно связана с прикладными задачами. Если задача записывается в виде формулы, то выполнимость формулы означает существование решения задачи, а модель, в которой эта формула истинна, даёт решение задачи. Проблема распознавания выполнимости формул в логике высказываний разрешима, однако язык этой логики предоставляет весьма ограниченные выразительные возможности. В то же время в логике предикатов проблема распознавания выполнимости алгоритмически неразрешима, что было доказано Чёрчем1. Поиски других достаточно выразительных расширений языка логики высказываний привели к созданию модальных логик, получаемых путём добавления к классической логике специальных операторов ("модальностей"). Дальнейшее развитие и комбинирование модальных логик, связанные, в частности, с решением прикладных задач, рассмотрены в многочисленных статьях и монографиях2. Одной из модальных логик, ориентированных на изучение процессов, происходящих во времени, является так называемая логика ветвящегося времени, известная под названием Ctl - Computational tree logic3.

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

1А.СЬшсЬ A note on the Entscheidungsproblem. - J. Symbolic Logic, 1936, 1, pp. 40-41, 101-102.

'D.M.Gabbay, A-Kurucz, P.Wolter, M.Zakharyaschev, Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic and Foundations of Mathematics, 148. Elsevier, North-Holland, 2003.

'Emerson E.A. Automated temporal reasoning about reactive systems // Logics for

concurrency. Lecture Notes in Computer Science, V. 1043. Berlin: Springer, 1996. P. 41-101. _]_

РОС НАЦИОНАЛЬНАЯ ЬИЬЛИОПКА

С ílcrcpÓJDI

200jP К í

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

Табличный подход основан на методе семантических таблиц, впервые предложенном Бетом6, и для разрешимых модальных логик изложен в работе7. Табличный метод в схематическом виде для Ctl был впервые изложен в работе4. Несколько подробнее табличный метод для Ctl был опубликован в работе3. Этот метод состоит из построения по формуле конечного табличного графа, его анализа и построения по нему модели в случае выполнимости. Отметим, что в работах3'4 на граф в модели наложено ограничение в виде тотальности: каждая вершина графа должна иметь сына. Кроме того, некоторые случаи, возникающие, в частности, при построении новых вершин в графе, удалении вершин, проверки подтверждённости так называемых формул-обещаний, в этих работах не рассмотрены. Доказательства корректности, полноты и оценки сложности также даны в виде наброска. В связи с этим использование данного алгоритма, включая построение модели в случае выполнимости, а также доказательство

4Emerson Е.А., and Halpern J Y., Decision Procedure and Expressiveness in the Temporal Logic of Branching Time, Journal of Computer and System Sciences, vol.30, no.l, pp.1-24, Feb.85.

5Vardi M. and Wolper P., Automata Theoretic Techniques for Modal Logics of Programs, STOC 84; journal version in JCSS, vol. 32, pp. 183-221, 1986.

6Beth E.W., The foundations of mathematics, Amsterdam, 1959; выдержки даны в русском переводе: Математическая теория логического вывода. М.: Наука, 1967. С. 191-199.

7A.Chagrov, M.Zakharyaschev, Modal Logic, volume 35 of Oxford Logic Guides. Clarendon Press, Oxford, 1997.

невыполнимости, наталкивается на серьёзные трудности.

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

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

Целью работы является создание, детальное изложение алгоритма распознавания выполнимости формул в логике ветвящегося времени и иллюстрация возможностей его применения.

Методика исследования. При получении основных результатов диссертации использовались метод семантических таблиц, метод эквивалентных преобразований, аксиоматический метод.

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

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

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

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

щезначимых формул из аксиом и доказана его полнота.

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

Научная новизна. Созданный алгоритм распознавания выполнимости формул логики ветвящегося времени использует новую конструкцию - схему модели, существенно упрощающую процесс построения моделей. Остальные результаты являются новыми.

Теоретическая и практическая ценность. Диссертация носит теоретический характер. Описанные алгоритмы могут быть использованы: (1) для распознавания выполнимости формул логики ветвящегося времени; (2) для построения моделей в случае выполнимых формул; (3) для эффективного построения выводов общезначимых формул из аксиом; (4) для решения прикладных задач, условия которых записаны формулами логики ветвящегося времени.

Апробация работы. Результаты, представленные в работе, докладывались на XII и XIII Международных конференциях "Проблемы теоретической кибернетики" (Нижний Новгород, май 1999 г., и Казань, май 2002 г., соответственно), на II, III и V Международных конференциях "Дискретные модели в теории управляющих систем" (Красновидово, июнь 1997 г., Красновидово, июнь 1998 г., Ратмино, май 2003 г., соответственно), на семинаре по математическим вопросам кибернетики под руководством академика РАН профессора О.Б.Лупанова (механико-математический факультет МГУ).

Публикации. По теме диссертации имеется 7 публикаций, список которых приводится в конце автореферата.

Структура и объем работы. Диссертация состоит из введения, 3 глав, разбитых на 11 параграфов, заключения и списка литературы. Объем работы - 155 страниц. Список литературы содержит 42 наименования.

Содержание работы

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

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

В §1 вводятся основные понятия и обозначения для логики ветвящегося времени, в частности, понятия формулы, модели, истинности формулы в модели.

• Каждая пропозициональная переменная есть формула.

• Если (р, ф формулы, то в, являющаяся одним из 12 выражений ((рАф), (<рУф), (<р ф), ЧО<р, ЗО<р, УП<р, 3а<р, УО<р, 30<р, \/(<рПф), 3(у> Ц ф), тоже называется формулой.

• Других формул нет.

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

Истинность формулы в в вершине щ модели М (обозначим это М,щ\= в) определяется индуктивно.

• Если в есть пропозициональная переменная р, то М, щ |= в р £

Ь(щ).

• Если в есть (<р А ф) [(у V ф)], то М, и, (= в <=>- М,иг \= <р и [или] М,и% \= ф.

• Если в есть (9? —¥ ф), то М, иг в М,щ (= ф или М, и, (р (т.е. неверно, что М, щ |= <р).

• Если в есть (р, то М, и,\= в <^==> М, щ ^ (р.

• Если в есть УО(р, то М,и, (= в для каждого сына и} вершины щ верно М, и3 (= <р\ либо вершина и% сыновей не имеет.

• Если в есть ЗОуэ, то М,иг \= в <=> существует хотя бы один сын щ вершины щ, и верно М,и} |= <р.

• Если в есть то М, и, (= в для каждого полного пути в графе с началом в вершине и, в каждой его вершине верно М, и} |=

• Если в есть ЗП<£>, то М,щ 0 <*==>• существует полный путь в графе с началом в вершине щ, в каждой вершине и3 которого верно

М, щ Н у?.

• Если 9 есть УО^, то А/, иг |= 9 для каждого полного пути в графе с началом в вершине иг найдётся вершина этого пути, для которой верно М, и})=

• Если 0 есть ЭО<р, то Л/, иг |= 0 существует полный путь в графе с началом в вершине щ, в котором найдётся вершина и}, для которой верно М, щ (= <р.

• Если 9 есть У(<р 15 -ф), то М, иг |= в для каждого полного пути в графе с началом в вершине иг найдётся вершина и3 этого пути, для которой верно М,и3 |= а в каждой вершине и^ этого пути, из которой достижима и3, отличной от и3 и достижимой из и,, верно М,ик \=ч>.

• Если в есть 13 ф), то М,иг 9 существует полный путь в графе с началом в вершине и1: для которого найдётся вершина и} этого пути, для которой верно М,и} ф, а в каждой вершине и* этого пути, из которой достижима и}, отличной от и3 и достижимой из иг, верно М, ик \= <Р-

Формула 9 истинна в модели М, если она истинна в начальной вершине щ этой модели. Модель, в которой истинна формула 9, называется моделью для формулы 98. Формула 9 выполнима, если она истинна в некоторой модели. Формула 9 не выполнима, если для неё не существует модели. Формула 9 общезначима, если она истинна в каждой модели.

Понятия истинности формулы, выполнимости и невыполнимости иллюстрируются примерами.

Алгоритм распознавания выполнимости формулируется в §§2-4. В §2 даётся определение схемы модели и формулируется первая часть алгоритма - построение размеченной и завершённой схем моделей.

Схема модели - это конечный связный ориентированный граф С?, удовлетворяющий следующим условиям.

1. Множество вершин и дуг графа 6? либо пусто (в этом случае схему модели будем называть пустой), либо в С выделена вершина, назы-

8Такнм образок, следует отличать модель вообще от модели для формулы.

ваемая начальной и обозначаемая символом Д).

2. Вершины графа б? обозначаются символами Ва,В\,... и делятся на два вида: основные, обозначаемые символами Со, ■ ■и временные, обозначаемые символами Од, Х>2,____

3. В графе б сыном основной вершины может быть только временная, а сыном временной - только основная. При этом каждая временная вершина имеет хотя бы одного сына. Основная вершина, не имеющая сыновей, называется концевой.

4. В графе б? каждой вершине В; приписано конечное множество 5г+ формул, называемых положительными, и конечное множество В~ формул, называемых отрицательными. К некоторым формулам из этих множеств в основных вершинах приписывается справа символ *9.

Введём для схемы модели С? некоторые обозначения. Если вершина В, содержит не помеченные символом * формулы, то формулой Хв, обозначается конъюнкция всех таких положительных, а также отрицаний отрицательных формул. В противном случае формулой Хв, является формула Т, которая означает сокращение для формулы (р\/->р). Формула хв, называется характеристической формулой (х.ф.) вершины Вг. Некоторым вершинам приписывается верхний индекс [либо Т]. Такие вершины называются ±-помеченными [Т-помечен-ными], что содержательно означает невыполнимость [выполнимость] х.ф. данной вершины. Если вершина В, ±-помечена или Т-помечена, то она называется помеченной. Вершина В{ называется Л-свободно [Т-свободно] достижимой, если в С? существует цепь, ведущая из начальной вершины в вершину Bi, каждая вершина которой не является ^-помеченной [Т-помеченной]. Вершина Вг, которая ^-свободно и Т-свободно достижима, называется свободно достижимой.

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

9Этот символ приписывается в точности к тем формулам, которые оказались разобранными путём применения перечисленных ниже б правил

Схема модели называется ^-размеченной [Т-размеченной], если её начальная вершина ±-помечена [Т-помечена]. Схема модели С? называется размеченной, если она 1) ±-размечена; либо 2) Т-размечена; или 3) каждая концевая вершина в С? помечена или не является свободно достижимой. Построение размеченной схемы модели начинается со схемы модели, состоящей из вершин Д>> Со, и дуги (£>о,Со), где Ид — {0}, Г>о = 0, Со — {0}, С0~ = 0. Оно состоит в применении перечисляемых ниже б правил в порядке их следования. Каждое правило применяется к некоторой непомеченной концевой свободно достижимой основной вершине Сг и даёт новую схему модели. Правила построения размеченной схемы модели следующие: правило противоречия, правило завершения, правило эквивалентности, правило линейности, правило ветвления и правило построения новых вершин.

Завершённой схемой модели называется схема модели, полученная из размеченной схемы модели приведением, т.е. удалением всех не ^-свободно достижимых вершин, затем удалением не Т-свободно достижимых вершин без Т-пометки, а также всех входящих и выходящих из них дут.

Если завершённая схема модели оказалась пустой, то алгоритм распознавания выполнимости даёт ответ, что исходная формула 0 не выполнима. Если в завершённой схеме модели начальная вершина оказалась Т-помеченной, то алгоритм распознавания выполнимости даёт ответ, что исходная формула 0 выполнима и строит модель, в которой 0 истинна (§4, п.4.1). Если же завершённая схема модели не пуста и её начальная вершина не является Т-помеченной, то следующей частью исследования формулы 0 на выполнимость является фильтрование завершённой схемы модели.

Фильтрование схемы модели, содержащееся в §3, состоит в выполнении процедуры фильтрования, выделяющей в схеме модели вершины, которые, как и ранее в правиле противоречия §2, становятся ±-помечснными. Однако, если в правиле противоречия, применяемом к основной вершине, противоречие, вызывающее _1_-помеченностъ вершин, является явным - зависящим только от положительных и отрицательных формул в этой вершине, то теперь оно связано с так называемой неподтверждённостью обещания.

Обещанием, содержащимся в вершине С, (Д), будем называть формулу в в одном из 6 случаев (пометки * здесь и ниже опускаются): а) в = ЭО^ е С+, Ь) в = МОг\> е С+, с) в = ЗОт/. € С,", а) б = УП^ € СГ, е) 9 = 3(<р 15ф)е С+, {) в = У(<р У ф) е С,+.

Будем говорить, что в случаях а),с!),е) обещание в имеет тип В, а в случаях Ь),с),1:) - тип V.

Для каждого из шести видов обещаний в вводятся понятия исполнения обещания, отложенного обещания и полного обещания. В процессе построения размеченной схемы модели обещания по правилу эквивалентности заменяются полными обещаниями, и эквивалентность такой замены основывается на лемме 5.1 (§5, п.5.1). Однако, при таком подходе вопрос выполнимости х.ф. вершины, содержащей обещания, может сводиться к вопросу выполнимости х.ф. последующих вершин, содержащих эти обещания, и оставаться на этапе построения завершённой схемы модели без ответа. Требуемый ответ будет получен, если для каждого обещания и содержащей его основной вершины мы проанализируем специальные подграфы, порождённые этой вершиной, которые состоят из определённых множеств вершин, достижимых из данной. В п.3.2 вводятся определения таких подграфов: определение основного ациклического подграфа' (а.п.) и определение усечённого а.п., порождённых основной вершиной Сг. В п.3.3 даётся определение подтверждённости обещаний. Подтвсржденность обещания 9 типа V заключается в существовании соответствующего основного а.п., а подтверждейность обещания в типа 3 заключается в существовании соответствующего усечённого а.п.

Процедура фильтрования выполняется для завершённой или размеченной схем моделей. Она состоит в просмотре всех основных ±-свободно достижимых вершин графа <2, нахождении среди них таких, которые содержат хотя бы одно неподтверждённое обещание, и выполнении для этих вершин процедуры Л_-разметки из правила противоречия. Схема модели, получающаяся после фильтрования завершённой (или размеченной) схемы модели, называется повторно размеченной. После фильтрования схемы модели выполняется приведение повторно размеченной схемы модели к новой схеме модели, которую будем называть заключительной. Это приведение выполняется в точ-

ности так же, как и описанное выше приведение размеченной схемы модели к завершённой. Таким образом, заключительная схема модели либо пуста, либо не содержит ±-помеченных вершин и в каждой основной вершине всякое обещание подтверждено.

Если заключительная схема модели пуста, то алгоритм распознавания выполнимости даёт для исходной формулы ответ "© не выполнима". Если заключительная схема модели не пуста, то алгоритм распознавания выполнимости даёт для исходной формулы ответ "0 выполнима" и строит для неё модель.

В §4 формулируется третья часть алгоритма распознавания выполнимости - построение модели. Построение модели для формулы 0 производится в случае ответа "0 выполнима". Этот ответ даётся либо по окончании первой части алгоритма в случае завершённой Т-помеченной схемы модели, либо по окончании второй части в случае непустой заключительной схемы модели.

В первом случае модель для формулы 0 получается из специального подграфа завершённой Т-помеченной схемы модели путём удаления временных вершин, а также соответствующего переименования основных вершин и определения функции означивания Ь.

Во втором случае даётся построение модели выполняется для формулы хв,, где Вг - произвольная вершина в заключительной схеме модели С. Отсюда, в частности, получается и модель для формулы 0, так как по построению формулы 0 и Хоа совпадают. Если Вг -основная вершина С,, то модель строится для формулы Хс,> а если В, - временная вершина Д, то она имеет некоторого сына С„ и моделью для формулы хв, объявляется модель, которая строится для формулы хс,- Таким образом, построение модели для формулы Хв, сводится к построению модели для формулы хс,- Принципиальная трудность построения модели во втором случае состоит в том, что в графе С? могут встретиться основные вершины, содержащие несколько обещаний, которые одновременно не могут быть подтверждены ни в каком подграфе заключительной схемы модели, по которому получается модель в первом случае. Для разрешения этой проблемы мы "удлиняем" модель таким образом, чтобы в ней для каждого обещания, содержащегося в основной вершине заключительной схемы моде-

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

В главе 2 доказывается ряд теорем об алгоритме распознавания выполнимости формул из главы 1. В §5 устанавливаются свойства правил алгоритма для х.ф. вершин, к которым эти правила применяются. В §6 доказывается теорема о завершаемости работы алгоритма за конечное число шагов. В §7 доказывается теорема о корректности работы алгоритма (теорема 7.3). Эта теорема утверждает, что в найденной алгоритмом модели для исследуемой формулы эта формула истинна. Отсюда следует, что если для формулы © алгоритм даёт ответ "0 выполнима", то этот ответ всегда является верным.

В §8 доказывается, что для исследуемой формулы 0 ответ алгоритма "0 не выполнима" также всегда является верным, т.е. в этом случае формула 0 действительно не выполнима в соответствии с определениями §1. С учётом теоремы о завершаемости работы алгоритма отсюда получается доказательство теоремы о полноте алгоритма (теоремы 8.3), утверждающей, что если формула 0 выполнима, то некоторая модель, в которой эта формула истинна, будет найдена алгоритмом. Из теорем о корректности и полноте алгоритма получается следствие (следствие 8.1), которое заключается в том, что если формула истинна в некоторой бесконечной модели, то она истинна и в некоторой конечной модели.

Наконец, в §9 устанавливается в определённом смысле единственность схемы модели и суммарной схемы модели, введённой в §2 п.2.6 и соответствующей табличному графу в работе Эмерсона3. Также в этом параграфе доказывается нестрогое включение первой из схем моделей во вторую и приводятся примеры классов формул, для которых это включение строгое. Отсюда следует, что алгоритм распознавания выполнимости формул из главы 1, основанный на построении схемы модели, работает либо быстрее, либо за то же число шагов, что и алгоритм Эмерсона, основанный на построении табличного графа.

В главе 3 рассматривается теоретическое и практическое применение сформулированного в главе 1 алгоритма. В §10 рассматривается теоретическое применение - формулируется эффективный алгоритм построения вывода общезначимых формул из аксиом.

Следующие формулы называются аксимомами логики ветвящегося времени10.

• (Axl) всякая корректная и полная система аксиом логики высказываний11

• (Ах2) 30<р = 3(Т 15 <р)12

• (АхЗ) VO<? е= V(T U <р)

• (Ах4) VD <р = i3О-чр

• (Ах5) 3U<p гг ->VO-iy>

• (Ахб) Щ<р Уф) = (30<^ V 30ф)

• (Ах7) УО<р = --ЭО

• (Ах8) 3(<р U ф) = (ф V (<р Л 303(<р U ф)))

• (Ах9) V(p 15ф) = (фУ ((ip Л VOV(<p 15 ф)) Л ЗОТ))

• (AxlO) VOT

Правила вывода в логике ветвящегося времени следующие.

• (R1) (<р ф) I- (30ip ЗОф)

• (R2) \ipx Л ЗО^)) h -»• U ipt))

• (R3) {<рх (-трз Л VO fa V U <р2)))) Н (<Pi -3(V> U yj))

• (R4) Правило (MP): <р, (¡р V>) Ь ф

Формула 0 называется выводимой, что обозначается h 8, если существует такая конечная последовательность формул, заканчивающаяся формулой 0, в которой каждая формула является подстановкой в одну из аксиом (т.е. аксиомой) или следует из предыдущих по одному из правил вывода. Эта последовательность называется выводом формулы 0 из аксиом.

Для этой системы аксиом и правил вывода нами введены девять

l0Emerson Е.А., Halpern J.I. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time // Journal of Computer and System Sciences, vol. 30, no 1, pp. 1-24, Feb. 85.

UB качестве такой системы взята Гильбертовская система аксиом - си. Мендельсон Э. Введение в математическую логику: Пер с англ. //Под ред. С.И.Адяна. - 3-е ИЗД. - М.: Наука. Главная редакция физико-математической литературы, 1984.

17tp = ф означает сокращение для формулы ((tp -+ ф) Л (ф -» у)) ■

расширений аксиом и правил вывода. Использование данных вспомогательных аксиом и правил вывода всегда может быть заменено их выводами из Axl-AxlO, (R1)-(R4), изложенными в im.10.2-10.ll. Построение вывода общезначимой формулы из аксиом происходит следующим образом. Для данной общезначимой формулы рассматривается задача распознавания выполнимости её отрицания. Попытка построить для такой формулы модель приводит к неудаче, однако накопленная в построенной схеме модели информация используется для вывода двойного отрицания исходной формулы с помощью расширенных аксиом и правил вывода. Этот процесс начинается с вывода отрицаний х.ф. концевых вершин, а также отрицаний х.ф. вершин, содержащих неподтверждённые обещания, и продолжается "снизу вверх" вплоть до вывода отрицания х.ф. начальной вершины, совпадающей с двойным отрицанием данной общезначимой формулы. Паконец, из вывода двойного отрицания исходной общезначимой формулы получается вывод её самой. Для данного эффективного алгоритма построения вывода общезначимых формул из аксиом доказывается теорема о полноте (теорема 10.1): если формула 0 общезначима, то она выводима, а также теорема о корректности (теорема 10.2): если формула 0 выводима, то она общезначима. С использованием этих теорем получается второе доказательство теоремы о полноте (теоремы 8.3) для алгоритма распознавания выполнимости формул.

В §11 рассматривается практическое применение алгоритма, со стоящее в записи прикладной задачи в виде формулы и построении модели, по которой получается решение задачи. По классификации

A.А.Ляпунова и С.В.Яблонского13 шахматная позиция является одной из управляющих систем (У.С.), обладающей структурой и функционированием. Таким образом, проблему нахождения решения шахматной задачи можно рассматривать как пример синтеза У.С. В качестве примера такой задачи нами выбран следующий этюд К.Эберса14, яв-

13Ляпунов A.A., Яблонский C.B. Теоретические проблемы кибернетики. "Проблемы кибернетики", 9, M , Физматгиз, 1963 С. 5-22. Избранные труды С.В.Яблонского/ Отв. ред

B.Б.Алексеев, В.И.Дмитриев. - М.: МАКС Пресс, 2004 С. 550-581.

14Портнш Л., Шаркози Б. 600 окончаний: Пер. с венг. А.Лилиенталя. - М.: Физкультура и спорт, 1979, с. 19-20.

ляющийся одной из самых сложных задан, относящихся к шахматной теории систем полей соотоветствия15. Белые: король - сЗ, пешки - 66, d4, еЗ, /¡.2; чёрные: король - h7, пешки - 67, ¿6, <f5, е4, h4, h3. В этюде Эберса ход белых: могут ли они сделать ничью, и если могут, то как им для этого надо играть? По этой задаче выписана формула 0, имеющая вид: Init A Rules A Aim, где формула Init соответствует начальной позиции, формула Rules соответствует правилам игры, а формула Aim соответствует цели (белых), заключающейся в данном этюде в контролировании ключевых полей 66 и /3, достижение которой равносильно решению задачи. Путём применения алгоритма распознавания выполнимости из главы 1 установлено, что формула 0 выполнима, построена модель М (таблицы 11.1 и 11.2) и доказано, что формула 0 истинна в этой модели. В построенной модели М для формулы 0 вершины соответствуют позициям, начальная вершина -начальной позиции. Дуга из одной вершины в другую соответствует изменению позиции вследствие сделанного хода, который однозначно получается по отличию истинных пропозициональных переменных в этих вершинах. В модели М вершины, соответствующие позициям, в которых ходят белые, и вершины, соответствующие позициям, в которых ходят чёрные, чередуются. Причём из первых выходит ровно одна дуга, а из вторых - число дуг, равное числу возможных ходов чёрных в возникшей позиции. Таким образом, все вершины первого вида с учётом изменений переменных в сыне каждой из них дают полное решение задачи - все пары: (встречающаяся позиция) - ход белых, которое выписано в п.11.7. В п.11.8 показывается трудность нахождения чисто шахматного решения и трудоёмкость обнаружения ошибочности неправильного хода белых. Наконец, в п.11.9 указывается метод построения по шахматной задаче и формуле 0 формулы 0' (называемой двойственной к формуле 0), выполнимость которой равносильна невозможности достижения нами требуемого результат та. При этом по модели, в которой формула 0' истинна, аналогично п. 11.7 находится стратегия противника, которая не позволяет достичь цели ни при какой нашей игре. Таким образом, исследование

"Шахматные окончания: Пешечные. - 2-е изд , доп./Под ред. Ю.Л.Авербаха. - М.: Физкультура и спорт, 1983, С. 288, 269-298.

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

Публикации по теме диссертации

1. Хелемендик Р.В. Применение временных логик к анализу логических игр и головоломок.// Труды III Международной конференции "Дискретные модели в теории управляющих систем" (22-27 июня 1998 г.) - М.: Диалог-МГУ, 1998, с. 112-114.

2. Хелемендик Р.В. Алгоритм распознавания выполнимости формул во временных логиках, моделирующий рассуждения человека.// Тезисы докладов XII Международной конференции "Проблемы теоретической кибернетики" (Нижний Новгород, 17-22 мая 1999 г., Часть II) - М.: Изд-во механико-математического факультета МГУ, 1999, с. 234.

3. Хелемендик Р.В. Приложения логик линейного и ветвящегося времени. Алгоритм распознавания выполнимости формул // Вестник Нижегородского государственного университета. Математическое моделирование и оптимальное управление. Нижний Новгород: Изд-во Нижегородского ун-та, 2000. Вып.1(22). С. 176-191.

4. Хелемендик Р.В. О корректности и полноте одного алгоритма распознавания выполнимости формул в логике ветвящегося времени.// Тезисы докладов XIII Международной конференции "Проблемы теоретической кибернетики" (Казань, 27-31 мая 2002 г., Часть II) -М.: Изд-во центра прикладных исследований при механико-математическом факультете МГУ, 2002, с. 183.

5. Хелемендик Р.В. О выводе общезначимых формул из аксиом в логике ветвящегося времени.// Труды V Международной конференции "Дискретные модели в теории управляющих систем" (Ратмино, 26-29 мал 2003 г.) - М.: Издательский отдел факультета ВМиК МГУ имени М.В.Ломоносова с. 88-89.

6. Хелемендик Р.В. О методе решения шахматных задач с помощью формул логики ветвящегося времени.// Алгебра, логика и

кибернетика: Материалы Международной конференции. - Иркутск, изд-во ГОУ ВПО "Иркутский государственный педагогический университет", 2004, с.215-216.

7. Хелемендик Р.В. Об использовании схем моделей при исследовании на выполнимость формул логики ветвящегося времени и построении вывода общезначимых формул из аксиом. //VI International congress on mathematical modeling/ Book of abstracts/ September 2026, 2004, Nizhny Novgorod, University of Nizhny Novgorod, p.388.

Подписано в печать 25.04.2005 г. Формат 60x90,1/16. Объем 1,0 п.л. Тираж 100 экз. Заказ №231

Отпечатано в ООО "Фирма Блок" 107140, г. Москва, ул. Краснопрудная, вл.13. т. 264-30-73 \vww.blok01 centre.narod.ru Изготовление брошюр, авторефератов, печать и переплет диссертаций.

О/.М-РШ

РНБ Русский фонд

2005-4 41936

19 МАЙ 2005

Введение

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

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

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

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

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

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

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

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

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

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

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

Глава 3. Применение алгоритма.

§10. Построение вывода общезначимых формул из аксиом

§11. Пример применения алгоритма к решению шахматной задачи

Проблема распознавания выполнимости формул в логике имеет большое теоретическое значение и тесно связана с прикладными задачами. Если задача записывается в виде формулы, то выполнимость формулы означает существование решения задачи, а модель, в которой эта формула истинна, даёт решение задачи. Проблема распознавания выполнимости формул в логике высказываний разрешима, однако язык этой логики предоставляет весьма ограниченные выразительные возможности. В то же время в логике предикатов проблема распознавания выполнимости алгоритмически неразрешима, что было доказано Чёрчем [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. Приведён пример применения алгоритма к решению шахматной задачи. Условие задачи записано в виде формулы логики ветвящегося времени, выполнимость которой означает существование решения, и это решение получено по модели, построенной для формулы.

Заключение

1. Алексеев В.Б. Лекции по дискретной математике: Учебное пособие. - М.: Издательский отдел Факультета ВМиК МГУ им. М.В.Ломоносова, 2004.

2. Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М., Мир, 1979.

3. Ботвинник М.М. От шахматиста к машине М.: Физкультура и спорт, 1979.

4. Дж. Булос, Р.Джеффри. Вычислимость и логика. М.: Мир, 1994.

5. Гильберт Д., Бернайс П., Основания математики. Логические исчисления и формализация арифметики. М.: Наука, 1979.

6. Гэри М., Джонсон Д. Вычислительные машины и труднореша-емые задачи. М., Мир, 1982.

7. Дискретная математика и математические вопросы кибернетики// Под. ред. С.В.Яблонского и О.Б.Лупанова. М.: Наука, 1974 г.

8. Захаров В.А. Быстрые алгоритмы разрешения эквивалентности операторных программ на уравновешенных шкалах // Математические вопросы кибернетики. Вып. 7. М.: Наука, 1998. - С. 303-324.

9. Логический подход к искусственному интеллекту. От модальной логики к логике баз данных. М.: Мир, 1998. С. 222-313.

10. Ляпунов A.A., Яблонский C.B. Теоретические проблемы кибернетики. "Проблемы кибернетики", 9, М., Физматгиз, 1963. С. 5-22.

11. Мендельсон Э. Введение в математическую логику: Пер. с англ. //Под ред. С.И.Адяна. 3-е изд. - М.: Наука. Главная редакция физико-математической литературы, 1984.

12. Мошков М.Ю. Деревья решений. Теория и приложения. Нижний Новгород: Изд-во ННГУ, 1994.

13. Мошков М.Ю. Элементы математической теории тестов с приложениями к задачам дискретной оптимизации: Лекции. Нижний Новгород: Изд-во Нижегородского ун-та, 2001.

14. Оуэн Г. Теория игр. М.: Мир, 1971.

15. Портиш Л., Шаркози Б. 600 окончаний: Пер. с венг. А.Лили-енталя. М.: Физкультура и спорт, 1979, с. 19-20.

16. Справочная книга по математической логике: В 4-х частях/ Под ред. Дж.Барвайса. 4.1. Теория моделей: Пер. с англ. - М.: Наука. Главная редакция физико-математической литературы, 1982.

17. Хелемендик Р.В. Применение временных логик к анализу логических игр и головоломок.// Труды III Международной конференции "Дискретные модели в теории управляющих систем" (22-27 июня 1998 г.) М.: Диалог-МГУ, 1998, с. 112-114.

18. Чёрч А. Введение в математическую логику, том I. М.: ИЛ, 1961.

19. Шахматные окончания: Пешечные. 2-е изд., доп./Под ред. Ю.Л.Авербаха. - М.: Физкультура и спорт, 1983, С. 288, 269-298.

20. Яблонский С.В. Введение в дискретную математику. М.: Наука, 1986.

21. Избранные труды С.В.Яблонского/ Отв. ред. В.Б.Алексеев,

22. B.И.Дмитриев. М.: МАКС Пресс, 2004. С. 550-581.

23. Янов Ю.И. О локальных преобразованиях схем алгоритмов, Сб. "Проблемы кибернетики", 20, М., Физматгиз, 1968. С. 201-217.

24. Янов Ю.И. Метод сверток для разрешения формальных систем. М.: препринт Института Прикладной Математики N11 1977 г.

25. Янов Ю.И. Метод разрешения семантических свойств алгоритмов. Mathematical problems in computation theory Banach center publications, Volume 21, PWN-Polish scientific publishers Warsaw, 1988,1. C.585-597.

26. Beth E.W., The foundations of mathematics, Amsterdam, 1959; выдержки даны в русском переводе: Математическая теория логического вывода. М.: Наука, 1967. С. 191-199

27. A.Chagrov, M.Zakharyaschev, Modal Logic, volume 35 of Oxford Logic Guides. Clarendon Press, Oxford, 1997.

28. A.Church A note on the Entscheidungsproblem. J. Symbolic Logic, 1936, 1, pp. 40-41, 101-102.

29. Emerson E.A., Clark E.M. Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons // Science of Computer Programming, vol. 2, pp. 241-266, Dec. 1982.

30. Emerson E.A., Halpern J.I. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time // Journal of Computer and System Sciences, vol. 30, no 1, pp. 1-24, Feb. 85.

31. Emerson E.A.: Temporal and modal logic. Handbook of theoreticalcomputer science, Ed. By J.van Leeuwen, Elsevier Science Publishers, (1990) 997-1072

32. Emerson E.A. Automated temporal reasoning about reactive systems // Logics for concurrency. Lecture Notes in Computer Science, V. 1043. Berlin: Springer, 1996. P. 41-101.

33. Gabbay D.M., Kurucz A., Wolter F., Zakharyaschev M., Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic and Foundations of Mathematics, 148. Elsevier, North-Holland, 2003.

34. Goldblatt R. Logics of Time and Computation. Number 7 in CSLI Lecture Notes. CSLI Publications, Stanford, 1987.

35. Manna Z., Pnueli A. The Temporal Logics of Reactive and Concurrent Systems (Specifications). Springer-Verlag, Berlin, 1991.

36. Pnueli A. The temporal logic of programs // Proceedings of the Eighteenth Symposium on Foundations of Computer Science. Providence, RI. 1977. P. 46-57.

37. Vardi, M. and Wolper, P., Automata Theoretic Techniques for Modal Logics of Programs, STOC 84; journal version in JCSS, vol. 32, pp. 183-221, 1986.

38. Wolper P.: The tableau method for Temporal Logic: an overview. Logique et Anal., 28 (1985) 119-136.