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

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

Заключение

Список литературы диссертационного исследования кандидат физико-математических наук Хелемендик, Роман Викторович, 2005 год

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.