RUS ENG

17.11.2009 15:00 Давность: 9 yrs
Категория: Семинар

Верификация моделей для комбинированных логик знаний, времени и действий

Шилов Н.В. (Институт систем информатики им. А.П. Ершова, Новосибирск)


Доклад дает обзор современного состояния исследований по проблеме проверки (верификации) для комбинаций пропозициональных программных логик и логик знаний в моделях. Философское изучение логик знаний (или, как их еще называют, эпистимических логик) начато было в трудах выдающегося современного специалиста по философской логике Дж. Хинтикка в 1950-х годах. Трудом, который заложил методологические основы использования логик знаний в комбинации с логиками действий и/или времени для анализа распределенных систем, стала монография Fagin R., Halpern J.Y., Moses Y., Vardi M.Y.  Reasoning about Knowledge (MIT Press, 1995). Однако в этой фундаментальной методологической работе практически не уделено внимание алгоритмическим проблемам для комбинированных логик в целом, и проблеме верификации моделей в частности. Первая работа, в которой изучалась проблема проверки формул "чистых" логик знаний в синхронных и асинхронных средах - это журнальная статья van der Meyden R. Common Knowledge and Update in Finite Environments (Information and Computation, Vol. 140(2), 1998).  Эта работа вдохновила и подсказала пути для изучения проблемы проверки формул комбинированных логик в синхронных средах с абсолютной памятью.  Математические результаты, представленные в данном обзоре, можно считать распространением результатов и подхода цитируемой работы на комбинации логик действий и ветвящегося времени с логиками знаний. Кратко эти результаты можно суммировать следующим образом: проблема верификации моделей для комбинированных логик знаний, времени и действий разрешима, но ... с неэлементарной нижней оценкой сложности. Естественно возникает проблема экспериментальной проверки практичности полученных математических результатов. Экспериментальные исследования по этой теме начались 2002-04 г., поэтому в докладе будет рассказано о некоторых полученных экспериментальных результатах.