автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Верификация распределенных систем с использованием аффинного представления данных, логик знаний и действий

Российская академия наук Сибирское отделение Институт систем информатики им. А.П.Ершова

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

Гаранина Наталья Олеговна

ВЕРИФИКАЦИЯ РАСПРЕДЕЛЕННЫХ СИСТЕМ С ИСПОЛЬЗОВАНИЕМ АФФИННОГО ПРЕДСТАВЛЕНИЯ ДАННЫХ, ЛОГИК ЗНАНИЙ И ДЕЙСТВИЙ

05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Автореферат

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

Новосибирск, 2004

Работа выполнена в Институте систем информатики Сибирского отделения Российской академии наук

Научный руководитель: Официальные оппоненты:

Ведущая организация:

кандидат физико-математических наук Шилов Н.В.

доктор физико-математических наук Пальчунов Д.Е.

кандидат физико-математических наук Соколов В.А.

Тверской государственный университет (г. Тверь)

Защита состоится 28 декабря 2004 года в 15 час. 00 мин. на заседании диссертационного совета К003.032.01 в Институте систем информатики им А. П. Ершова Сибирского отделения РАН по адресу:

630090, г.Новосибирск, пр. Лаврентьева, 6.

С диссертацией можно ознакомиться в читальном зале библиотеки ИСИ СО РАН (пр. Лаврентьева, 6).

Автореферат разослан

п

ноября 2004 г.

Ученый секретарь диссертационного совета К003.032.01 к.ф.-м.н.

Нг

Мурзин Ф.А.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

Разнообразие программных логик, используемых для спецификации систем, объясняется не только тем, что разные логики описывают принципиально разные свойства моделей, но и различной сложностью проверки на модели каждой из них. Поэтому так важно исследовать теоретически алгоритмические свойства различных логик. Традиционно программные логики включают динамические логики, временные логики и их варианты с неподвижными точками. Однако во многих программных системах, в силу связи между информацией и действием, естественно возникает понятие знания. Что робот должен знать, чтобы открыть сейф, и откуда он знает, достаточно ли он знает, чтобы открыть его? Перед пересылкой очередного сообщения, знает ли отправитель, что получатель получил предыдущее? Когда база данных может ответить

РОС НАЦИОНАЛЬНАЯ I БИБЛИОТЕКА I СПетерОмг ЛГ,1

■ ОЭ Ж fur J JJL

на вопрос "Я не знаю"? Поэтому часто бывает, что правильность функционирования программной системы зависит от "знаний" ее компонент. Поэтому не так давно в семейство программных логик были добавлены эпистемические логики, в частности, пропозициональная логика знаний для п агентов PLKn и пропозициональная логика общих знаний для П агентов PLCn. Они позволяют специфицировать такие системы, в которых необходимо проверять утверждения, касающиеся знаний параллельных процессов, которых принято называть агентами. С помощью логик знаний особенно удобно описывать свойства систем, в которых действия распределенных параллельных процессов зависят от информации, которой они располагают. К таким программным системам относятся, коммуникационные протоколы, особенно в ненадежной среде, программы управления роботами, получающими информацию от окружающей среды и т.п. Проверка на модели систем, специфицированных эпистемическими логиками, позволяет исследовать в этих системах знания, основанные на неполной информации. Иными словами, можно, меняя доступность той или иной информации, проверять, как меняется у агента представление о мире и о других агентах. Например: достаточно ли процессу в системе с разделяемыми ресурсами наблюдать параметр занятости ресурса, чтобы знать, когда он освободится, или необходимо иметь доступ к локальной информации остальных процессов (например, к информации о состоянии вычислений). Однако особенно полезными оказываются комбинации логик знаний с темпоральными логиками или динамическими логиками действий с неподвижными точками, поскольку они позволяют описывать эволюцию знаний агентов во времени или их изменение в результате каких-либо действий. При рассмотрении временных аспектов знаний возникают системы, различающиеся "разумностью" агентов, действующих в системах. Например, часто рассматриваются забывающие агенты, которые не помнят историю развития событий в системе, а имеют лишь информацию о ее текущем состоянии. В противоположность им можно определить агентов с абсолютной памятью, различающих состояния системы, основываясь на запомненных ими истории данных. Кроме того, могут быть синхронные агенты, помнящие, "который час" и асинхронные, не знающие времени. Агенты, чьи знания не зависят от времени, называются обычными агентами. Свойства различных комбинированных логик в системах с разнообразными агентами изучаются в течении последних двадцати лет. Например, в 1986 г. Дж.Хальперном и М.Варди изучена задача разрешимости для

комбинаций временных логик ЬТЬ и CTL с логиками PLKn и PLCn в (а)синхронных системах как забывающих, так и с абсолютной памятью. В 1998 г. Р.ван дер Мейденом исследована задача проверки на модели формул РЬСп в (а)синхронных системах с абсолютной памятью. В 1999 г. Р.ван дер Мейденом и Н.В.Шиловым была изучена задача проверки на модели для комбинаций РЬКп и РЬСп с ЬТЬ в синхронных системах с абсолютной памятью. В этой работе были предложены древовидные структуры данных для проверки на модели логики линейного времени и знаний с ограниченной глубиной знаний. Однако перечисленные работы исследуют комбинации только темпоральных логик с логиками знаний. Комбинации же с динамической логикой с неподвижными точками позволяют выразить более широкий спектр свойств мульти-агентных систем. Например, при проверке на модели свойства существования выигрышной стратегии, можно узнать, какой минимальной информацией должен располагать агент, чтобы выиграть в конечной игре. Что касается практической стороны, то в 2003 году в Австралии под руководством Р.ван дер Мейдена был разработан прототип системы проверки на моделях МСК, проверяющий модели, специфицированные формулами некоторых комбинаций пропозициональных логик знаний и времени. Его недостатком является то, что используются опять-таки только темпоральные комбинации логик знаний и почти не реализована проверка самых интересных систем, а именно — синхронных с агентами с абсолютной памятью.

Вторая составляющая проверки на модели — алгоритмы проверки выполнимости спецификации — представлена большим разнообразием методов. Особенно важны алгоритмы проверки на модели формул ц-исчисления, как наиболее выразительной из пропозициональных программных логик. Однако даже самые эффективные из них экспоненциальны относительно размера формулы, поэтому целесообразно рассматривать фрагменты ц-исчисления, имеющие полиномиальную сложность проверки на модели. В 1993 г. А. Эмерсон, С. Джатла и П. Систла впервые определили фрагмент ц-исчисления, который допускает полиномиальную проверку на конечных моделях.

Основной недостаток метода проверки на модели — это "комбинаторный взрыв" в пространстве состояний, который возникает, когда система состоит из компонентов, переходы в которых выполняются параллельно. В 1987 г. К.МакМиллан показал, что, используя символьное представление графа переходов как двоичных разрешающих диа-

грамм (OBDD) Бриана — структур данных для представления булевых функций — можно верифицировать очень сложные системы. Применяя алгоритм Кларка-Эмерсона проверки на модели формул CTL и новое представление графов переходов, можно провести верификацию некоторых систем, содержащих более 10 20 состояний. Однако неявное представление в виде OBDD вполне подходит для моделирования последовательных схем и протоколов, состояния которых кодируются булевскими переменными, но для систем с целочисленными состояниями такое представление оказывается не совсем естественным. Для таких систем более эффективными оказываются представления, существенно использующие при кодировании тот факт, что элементами пространства состояний являются целые числа. В 1994 г. Б. Бугло и П. Волпер предложили периодические множества для представления множеств состояний. Основным недостатком такого представления является то, что оно не допускает полностью символической проверки на моделях. В 1999 г. Т. Бултан, Р. Гербер и В. Пух разработали систему для символической проверки бесконечных моделей, представляя множества состояний формулами арифметики Пресбургера. К достоинствам такого способа представления данных относится то, что можно проверять сколь угодно большие и даже бесконечные модели, но недостатком является тот факт, что сложность оперирования формулами Пресбургера вычислительно дорога: она экспоненциально зависит от размера формул.

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

Цель диссертации состоит в разработке эффективных методов верификации моделей мультиагентных систем. Достижение цели связано с решением следующих задач:

— теоретическое исследование проблемы проверки моделей для новых, более выразительных, комбинаций логик знаний и действий;

— теоретическое исследование нового эффективного аппроксимаци-онного алгоритма проверки на модели формул ^-исчисления;

— теоретическое исследование новых, более эффективных, символи-

ческих форматов представлений данных для логик действий и знаний;

— экспериментальная реализация новой системы проверки моделей для комбинированных логик знаний и действий на моделях.

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

Научная новизна состоит в следующем.

• Определены новые комбинации пропозициональных логик знаний и действий. Для них исследованы их относительная выразительная сила, сложности задачи проверки на модели и разрешимости в мультиа-гентных системах общего вида и с асинхронными забывающими агентами. В синхронных системах с агентами с абсолютной памятью исследована задача проверки на модели.

• Предложен полиномиальный алгоритм проверки на модели для фрагмента ^.-исчисления, вычисляющий верхнюю и нижнюю аппроксимацию семантики формулы.

• Для кодировки множеств состояний и переходов проверяемой модели предлагается использовать новые форматы представления данных, а именно: аффинные множества, векторно-аффинные множества и, для кодировки моделей, чьими состояниями являются деревья — векторно-аффинные деревья.

• По результатам теоретических исследований был выполнен машинный эксперимент: реализована программа Экзаменатор — прототип системы проверки моделей 1) с асинхронными забывающими агентами, специфицированных формулами ^-исчисления в комбинации с логикой знаний РЬКп; 2) с синхронными агентами с абсолютной памятью, специфицированных формулами логики СТЬ, расширенной действиями в комбинации с логикой знаний PLKn.

Практическая ценность заключается в том, что в разработанном методе проверки моделей, специфицированных формулами комбинированных логик знаний и действий, имеются следующие достоинства: 1) за счет новых комбинаций логик можно описывать и проверять более богатый спектр свойств мультиагентных моделей; 2) предложенный полиномиальный аппроксимационный алгоритм позволяет эффективно проверить иные, чем раньше, формулы ^.-исчисления, а значит и комбинированных логик знаний и действий; 3) предложенная кодировка состояний и переходов моделей позволяет эффективно проверять большие распределенные системы специального широкого класса.

Апробация работы. Основные научные результаты подробно обсуждались на объединенном семинаре ИСИ СО РАН и кафедры программирования НГУ "Теоретическое и экспериментальное программирование", докладывались на следующих научных конференциях и совещаниях:

1. International Workshop on Fixed Points in Computer Science (FICS 2002), Copenhagen, Denmark, 2002;

2. 4th International Conference of Computer-aided Technologies in Applied Mathematics, (ICAM-2002), Tomsk, Russia, 2002;

3. 5th International Conference of Perspectives of System Informatics (PSI2003), Novosibirsk, Russia, 2003;

4. Конференция-конкурс Технологии Microsoft в Информатике и Программировании, Новосибирск, Россия, 2004;

5. International Workshop on Concurrency, Specification and Programming (CSP 2004), Caputh, Germany, 2004.

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

Структура работы. Диссертация состоит из введения, пяти глав, заключения, списка литературы из 53 наименований и приложения. Объем основной части работы — 139 страниц, приложения — 26 страниц. Работа включает 15 иллюстраций и 10 таблиц.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

В первой главе даются основные определения, понятия, результаты и примеры, используемые в диссертации. В разд. 1.1 определены синтаксис и семантика базовых пропозициональных логик, как частных случаев и расширений пропозициональной полимодальной логики наиболее общего вида, формулы которой строятся из символов пропозициональных констант и символов отношений с помощью стандартных булевских связок и модальностей возможности и необходимости. Семантика данных логик определена в терминах выполнимости на моделях Крипке. Модель Крипке включает множество состояний, интерпретации символов отношений и символов пропозициональных констант и может рассматриваться как помеченный ориентированный граф с вершинами и ребрами, помеченными множествами пропози-

циональных констант и символами отношений, соответственно. В этой главе определяются следующие логики. В пропозициональной логике знаний для п агентов PLKn символы отношений являются символами агентов, занумерованных от 1 до п, причем интерпретация этих отношений неразличимости должна быть отношением эквивалентности. В пропозициональной логике общих знаний для п агентов PLCn символы отношений являются группами символов агентов, т.е. подмножествами множества {1,..., п}, а интерпретация этих отношений является рефлексивно-транзитивным замыканием отношений неразличимости агентов из группы, и, значит, тоже эквивалентностью. В элементарной пропозициональной динамической логике EPDL символы отношений — это символы действий с интерпретацией без каких-либо ограничений. Во временной логике на деревьях с действиями Act-CTL используются другие модальности: в следующем состоянии, всегда, когда-нибудь и пока. Так как это ветвящаяся логика, к синтаксису модальностей добавляются кванторы на каждом пути и на некотором пути, где под путем понимается последовательность состояний, получающаяся в результате повторений некоторого действия. Act-CTL с единственным действием равна известной логике С^. Пропозициональное л-исчисление лС — это EPDL, синтаксически расширенная конструкциями неподвижных точек формул, определяющих монотонное преобразование. Показано, что: PLCn — расширение PLKn; АЛ-СГЬ является расширением EPDL; ¡С — расширение Act-CTL. Определено понятие абстракции для полимодальных логик. Оно позволяет формализовать тот факт, что выполнимость некоторого множества формул (не обязательно тавтологий) сохраняется при переходе от конкретной модели к абстрактной. Оказывается полезным ввести новое понятие аффинной модели программной системы как конечной модели, состояния которой определяются целочисленными переменными. Кроме того, в описании модели не допускается перемножение этих переменных (умножение на константу допустимо), а все равенства, неравенства и переходы зависят от одной переменной.

В разд. 1.2 описаны примеры, иллюстрирующие выразительные возможности комбинации логик знаний и действий. В разд. 1.2.1 — задача о монетках, состоящая в определении фальшивой монеты среди настоящих посредством ограниченного числа взвешиваний на чашечных весах. Для этой головоломки построена ее формальная модель с единственным агентом, который "помнит" все свои действия и их результаты, т.е. обладает абсолютной памятью. Он вычисляет фальши-

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

Во второй главе рассматриваются алгоритмические проблемы комбинированных логик действий и знаний в различных мультиагентных системах. Для мультиагентных систем общего вида исследуется: 1) сравнительная выразительная сила этих логик; 2) задача проверки на модели; 3) разрешимость. Для мультиагентных систем с асинхронными забывающими агентами исследуются те же задачи. Для мультиагент-ных систем с синхронными агентами с абсолютной памятью исследуется задача проверки на модели. Более подробно: в разд. 2.1 на основе базовых логик определяются исследуемые комбинированные логики ,иРЬСп, ,иРЬКп, Лег-СТЬ-Сп, Лег-СТЬ-К„ БРБЬ-Сп и EPDL-Kn как синтаксическая комбинация соответствующих динамических логик и логик знаний с прежней семантикой, определенной в мультиагентной среде, являющейся сочетанием моделей для логик знаний и динамических логик. В утверждении 4 доказано, что сравнительная выразительная сила логик удовлетворяет следующим неравенствам: EPDL-Kn < EPDL-Cn,

ла-С1Ъ-кп < л^-сть-с,, ^РЬКп = ^РЬСп, ербь-кп < лость-

Кп < ^Кп и EPDL-Cn < Ла-С1Ъ-Сп < ^РЬСп.

Алгоритмические проблемы для этих логик в средах, т.е. системах с агентами общего вида, исследуются в разд. 2.2. В утверждении 5 оценивается сложность задачи проверки на модели: относительно размера модели и формулы она 1) линейна для формул логик EPDL-Kn, EPDL-Сп, А^-СП-Кп, и Л^-СП-Сп и 2) экспоненциальна для формул логик ^РЬКп и ,иРЬСп. Утверждение 6 о проблеме разрешимости: она PSPACE-полна для EPDL-Kn и EXPTME-полна для EPDL-Cn, Ла-

СТЬ-К^, Ла-СТЬ-Сп, цРЕКп, и ,иРЬСп. Теорема 1 об алгоритмических свойствах изучаемых логик формально объединяет эти утверждения. Утверждение 7 конструктивно доказывает возможность использования методов проверки на модели формул ц-исчисления для проверки формул комбинированных логик.

В разд. 2.3 асинхронные системы с забывающими агентами определяются как модели, порождаемые мультиагентными средами, чьими состояниями являются все последовательности состояний порождающей среды, а агенты таких моделей "видят" только последнее состояние последовательностей, "забывая" предыдущие состояния. Заметим, что количество состояний в этих системах бесконечно. Асинхронные системы с забывающими агентами в определенном смысле сводятся к мультиагентным средам. Чтобы показать это, определяется отображение непустых конечных последовательностей состояний в последний элемент этой последовательности и обратное ему отношение. В утверждении 8 показано, что формулы комбинированных логик выполняются на непустой конечной последовательности состояний в забывающей асинхронной среде тогда и только тогда, когда они выполняются в последнем состоянии последовательности в исходной среде. Это влечет утверждение 9 о том, что асинхронные системы с забывающими агентами являются абстракцией мультиагентных сред относительно формул исследуемых комбинированных логик, т.е. все формулы выполнимые в некотором состоянии порождаемой асинхронной системы с забывающими агентами, выполняются в соответствующем состоянии порождающей системы. Отсюда следует теорема 2 об эквивалентности алгоритмических свойств комбинированных логик в асинхронных средах с забывающими агентами соответствующим свойствам в мульти-агентных средах. Следовательно, интересующая нас задача проверки на моделях формул этих логик в бесконечных забывающих асинхронных средах сводится к той же задаче в конечных мультиагентных средах.

В разд. 2.4 определяются синхронные системы с абсолютной памятью как модели, порождаемые мультиагентными средами, чьими состояниями являются последовательности пар (состояние, действие) порождающей системы и агенты таких моделей "видят" всю последовательность целиком. Эти системы также имеют бесконечное множество состояний. Приведен пример такой модели на основе задачи об угадывании числа. Далее показаны симуляционные возможности синхронных систем с абсолютной памятью: утверждение 10 доказывает,

что можно симулировать вычисления машин Тьюринга; утверждение 11 показывает возможность симуляции выполнимости формул слабой логики второго порядка с единственной функцией следования WS( 1)S. Эти симуляционные свойства синхронных систем с абсолютной памятью используются в исследовании задачи проверки комбинированных логик в таких системах.

Разд. 2.5 посвящен проверке на модели комбинированных логик в синхронных системах с абсолютной памятью. В утверждении 12 доказано, что задача проверки на модели при всех п > 1: для ЕРБЬ-Сп — PSPACE-полна; для Лс£-СТЬ-Кп — разрешима с неэлементарной верхней и нижней границей; для Act-CTL-Cn, ц.РЬКп, и цРЬСп — неразрешима.

В разд. 2.6 проводится более детальное исследование задачи проверки на модели для формул логики Лй-СТЬ-К с ограниченной глубиной знаний. Целями этого исследования являются определение более точных границ задачи проверки на модели для данной логики, а также конструктивный подход к этому методу проверки. В связи с этим определяется глубина знаний формулы к как максимальная вложенность модальностей знаний. Новая модификация древовидных структур данных — к-деревъев знаний — порождаемых синхронными системами с абсолютной памятью, иллюстрируется на примере задачи об угадывании числа. В утверждении 13 подсчитывается количество А;-деревьев над системой и максимальное количество вершин в таких деревьях — они сравнимы с башней экспонент высоты к. Определяются деревья знаний агентов на последовательности состояний как деревья знаний, зависящие от всех состояний этой последовательности и переходов между ними. Эти деревья отражают знания, приобретенные агентами к последнему состоянию последовательности. Для к-деревьев определяется функция обновления знаний в результате действий. В утверждении 14 обосновывается корректность функции обновления знаний, т.е. показано, что деревья знаний агентов на последовательности состояний могут быть получены последовательным применением функция обновления знаний к дереву знаний, соответствующему исходному элементу данной последовательности. В утверждении 15 показано, что логики Лй-СТЬ-Кп и Лй-СТЬ имеют одинаковую выразительную силу в синхронных системах с абсолютной памятью. С помощью функций обновления знаний определяется класс ассоциированных с синхронными системами с абсолютной памятью конечных моделей Крипке, базирую-

щихся на к-деревьях. Из утверждения 17 следует возможность проверки формул .ЛсьСТЬ-К с семантикой в бесконечных синхронных системах с абсолютной памятью на ассоциированных с ними конечных моделях. Утверждение 18, вследствие учета размера и количества к-деревьев в ассоциированных моделях Крипке, более точно оценивает сложность задачи проверки на моделях для формул Лй-СТЬ-К и вместе с утверждением 12 приводит к теореме 3 об оценке сложности задачи проверки на модели комбинированных логик в синхронных системах с абсолютной памятью.

Одним из главных выводов второй главы является то, что проверка мультиагентных систем, специфицированных формулами комбинированных логик знаний и действий, так или иначе, сводится к проверке формул ^.-исчисления в конечных моделях. Поэтому в третьей главе предлагается апироксимационный алгоритм для вычисления семантики формул нового фрагмента ^.-исчисления, имеющий полиномиальную оценку сложности, и обосновывается его корректность. Сначала в разд. 3.1 обсуждаются параметры сложности задачи проверки на модели формул ц.-исчисления. Затем в разд. 3.2 вводится специальная префиксная форма формулы ^.-исчисления, приемлемая для алгоритма проверки, и в утверждениях 19 и 20 показано, что всякую формулу ^-исчисления можно привести к такому виду. Далее в разд. 3.3 — собственно алгоритм, полиномиальность которого основана на полиномиальной оценке вычислений независимых неподвижных точек, как показано в утверждении 21 о корректности алгоритма. Там же утверждается, что этот алгоритм вычисляет верхнюю и нижнюю аппроксимации семантики формулы ^.-исчисления. Следствием утверждения 21 является теорема 4 о том, что совпадающие аппроксимации равны точной семантике формулы. Показано, что формула, выражающая справедливость, принадлежит новому фрагменту, но не фрагменту Эмерсона-Джатлы-Систлы, также имеющего полиномиальную сложность проверки на модели. Доказано важное утверждение 22 о том, что данный алгоритм вычисляет точную семантику формул Act-CTL.

В четвертой главе предлагаются новые символические представления данных для алгоритмов символической проверки на моделях формул ^-исчисления и комбинированной логики действий и знаний Act-СТЬ-Кп — аффинные представления. Также описаны методы манипуляции с ними, необходимые для символической проверки на моделях, а именно: объединение множеств, их пересечение и вычисление предусло-

вий действий, а так же проверка множеств на включение.

В разд. 4.1 изложены синтаксис и семантика языка описания моделей, для которых возможны аффинные представления, а именно — аффинных моделей. В подразд. 4.1.1 определяется синтаксис, а в под-разд. 4.1.2 — семантика языка и ассоциированная с ней модель Крип-ке, чья корректность относительно описания модели показана в утверждении 24. В подразд. 4.1.3 описан переход от аффинных моделей с нечисловыми типами переменных к аффинным моделям с целочисленными переменными. В подразд. 4.1.4 приведен простой пример описания аффинной модели игры в числа.

Разд. 4.2 посвящен описанию ограниченных аффинных множеств, которые являются множествами, определяемыми конечным набором аффинных атомов — линейных двучленов с целыми коэффициентами, каждый из которых определен на отрезке целых чисел. С их помощью можно кодировать аффинные модели с единственной переменной. В подразд. 4.2.1 предлагается метод кодирования с помощью аффинных множеств пропозициональных констант и действий таких моделей и в утверждении 25 доказана его корректность. В подразд. 4.2.2 описаны алгоритмы манипуляции с аффинными множествами. Объединение аффинных множеств является простым объединением множеств. Для вычисления пересечения необходимо определить совпадающие значения аффинных множеств посредством решения линейных диофанто-вых уравнений. Вычисление предусловий детерминированных переходов сводится к вычислению значений аффинных множеств, из которых возможен детерминированный переход в данное аффинное множество, для чего также используются решения линейных диофантовых уравнений. Предусловия недетерминированных действий вычисляются относительно их контекста в проверяемой формуле с использованием предусловий детерминированных переходов, из которых они состоят. Корректность этих алгоритмов показана в утверждении 26, там же оценена их сложность. В подразд. 4.2.3 изложены идеи оптимизации ограниченных аффинных множеств, необходимой, поскольку объединение множеств может привести к дублированию элементов. Подразд. 4.2.4 содержит алгоритм проверки включения множеств и утверждение 27 о его корректности и сложности.

В разд. 4.3 представлены векторно-аффинныемножества, обобщающие понятие аффинных множеств для возможности кодирования аффинных моделей с несколькими переменными. Здесь идея состоит в

том, чтобы каждое множество состояний модели описать набором аффинных векторов, компонентами которых являются аффинные атомы, соответствующие значениям переменных модели. Аналогично предыдущему разделу в подразд. 4.3.1 предлагается метод кодирования с помощью векторно-аффинных множеств пропозициональных констант как множеств массивов аффинных атомов, и действий аффинных моделей с помощью векторных действий — как множеств массивов аффинных переходов. В утверждении 28 доказывается корректность этого представления. В подразд. 4.3.2 описаны алгоритмы манипуляции, необходимые для символической проверки с использованием векторно-аффинного представления. Поскольку векторно-аффинные множества расширяют понятие аффинного множества, а векторное действие — понятие аффинного действия, то эти алгоритмы основаны на аналогичных алгоритмах для аффинных множеств. В утверждении 29 показана корректность алгоритмов и подсчитана их сложность. В подразд. 4.3.3 изложен простой алгоритм оптимизации векторно-аффинных множеств с целью исключения дублирующих друг друга элементов представления, а подразд. 4.3.4 содержит алгоритм проверки включения множеств и утверждение 30 о его корректности и сложности.

В разд. 4.4 на простом примере показана эффективность нового представления для моделей определенного класса по сравнению с популярным символическим представлением данных как упорядоченных бинарных разрешающих диаграмм (OBDD). Вычислены векторно-аффинная кодировка и BDD-кодировка системы переходов с 20 состояниями. В частности, векторно-аффинная кодировка переходов — это целочисленная таблица размера 2 х 4, а дерево BDD-кодировки переходов содержит 72 вершины и 144 ребра. Процесс трансляции модели в векторно-аффинную кодировку происходит существенно быстрее.

Разд. 4.5 посвящен аффинной проверке на моделях комбинированных логик. В подразд. 4.5.1 синтаксис языка описания аффинных моделей дополнен конструкциями, позволяющими вводить агентов, связывая с ними множества наблюдаемых переменных модели. Здесь же определена семантика этих дополнений и среда, ассоциированная с описанием мультиагентной аффинной модели, чья корректность относительно описания среды показана в утверждении 31. Отметим, что из утверждения 7 следует, что свойства мультиагентных сред с обычными и забывающими (в силу теоремы 2) агентами, специфицированными в логике л РЬСК( и менее выразительных логиках), можно проверять,

используя алгоритмы проверки на модели для ц-исчисления. Поэтому в подразд. 4.5.2 определяется векторно-аффинный переход по знаниям, представляющий отношения неразличимости обычных и забываю -щих агентов, с использованием понятия наблюдаемых переменных, а именно: переход по знаниям некоторого агента из состояния w возможен в те состояния, где значения наблюдаемых переменных совпадают с их значениями в w. В утверждении 32 показана корректность этого представления. В подразд. 4.5.3 рассмотрены новые представления данных для проверки формул Ай-СТЬ-К в синхронных системах с абсолютной памятью — векторно-аффинные деревья. Они являются обобщением векторно-аффинных множеств для кодировки моделей, чьими состояниями являются деревья знаний. Эти структуры — деревья с вершинами, помеченными аффинными векторами, представляющими множество состояний, и ребрами, помеченными агентами. В подразд. 4.5.4 предлагается метод кодирования с помощью векторно-аффинных деревьев пропозициональных констант и действий моделей на деревьях, порожденных аффинными моделями с синхронными агентами с абсолютной памятью, и в утверждении 33 доказывается его корректность. Векторно-аффинные деревья позволяют кодировать множества деревьев с мощностью порядка размера модели, при этом экспоненциально уменьшается количество вершин по сравнению с обычными деревьями. В подразд. 4.5.5 описаны алгоритмы манипуляции, необходимые для символической проверки с использованием векторно-аффинного представления деревьев знаний. Поскольку векторно-аффинные деревья являются обобщением векторно-аффинных множеств, то эти алгоритмы основаны на аналогичных алгоритмах для векторно-аффинных множеств. В утверждении 34 показана корректность алгоритмов и вычислена их сложность. В подразд. 4.5.5 изложен простой алгоритм оптимизации аффинных деревьев с целью исключения дублирующих друг друга элементов представления, а подразд. 4.5.6 содержит алгоритм проверки включения множеств аффинных деревьев и утверждение 35 о его корректности и сложности.

В пятой главе содержится краткое описание прототипа системы Экзаменатор для проверки на моделях формул комбинированных логик. В разд. 5.1 описаны входные данные программы: аффинные модели с единственным агентом, со свойствами, специфицированными формулами логики цС+РЬК1; и с указанием типа агента — забывающего или с абсолютной памятью. Также описана структура программы, состо-

ящая из следующих блоков: обработка входного файла, трансляция в аффинные структуры данных, манипуляция данными, алгоритм проверки и вывод. Выходными данными являются: константа true (false), означающая, что спецификации удовлетворяют все (ни одно) состояния модели, либо множество состояний в которых формула спецификации выполняется. В разд. 5.2 описаны интерфейс и параметры программы. В разд. 5.3 приведен тест — задача об угадывании числа — на языке описания аффинных моделей и результаты тестирования для различных входных параметров задачи.

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

• В работе с теоретической точки зрения изучены выразительная сила, верхняя граница задачи проверки на модели и сложность разрешимости для пропозициональных программных логик EPDL-K, EPDL-C, Act-CTL-K, Act-CTL-C, ¡oPLK и ^PLC в средах общего вида, асинхронных забывающих средах и синхронных средах с абсолютной памятью. В частности, доказано, что 1) асинхронные среды с забывающими агентами являются абстракцией сред общего вида относительно множества всех формул вышеперечисленных логик; 2) задача проверки на модели разрешима в синхронных средах с абсолютной памятью для Act-CTL-K.

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

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

• Вышеизложенные результаты объединяются в методе аффинной проверки на модели для логик, представимых в ц.Р1Хп, в средах с асинхронными забывающими агентами и логик, представимых в Act-CTL-Кп, в средах с синхронными агентами с абсолютной памятью. На основе этого метода реализован прототип системы проверки моделей Экзаменатор и проведен эксперимент, показывающий эффективность метода.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Shilov N.V., Garanina N.O. Combining Knowledge And Fixpoints - Novosibirsk, 2002. - 50 p. - (Prepr./ Sib.Div. of RAS. IIS; N 98).

2. Shilov N.V., Garanina N.O. Model Checking Knowledge And Fixpoints // Proc. 4th Int. Workshop on Fixed Points on Computer Science

— Copenhagen, Denmark, 2002. — P. 25-39.

3. Shilov N.V., Garanina N.O. Model Checking Knowledge And Fixpoints // Тр. конф. Новые Информационные Технологии в Исследовании Сложных Структур — Вестник ТГУ. Материалы научных конференций, симпозиумов, школ, проводимых в ТГУ. — 2002. — N1(11) — С. 20-23.

4. Shilov N.V., Garanina N.O. A Polynomial Approximations for Model Checking // Proc. 5rd Int. Conf. Perspectives of System Informatics.

— Berlin etc.: Springer-Verlag, 2003. — P. 395—400. — (Lect. Notes Comput. Sci.; 2890).

5. Гаранина Н.О. Аффинная проверка моделей программ // Тр. конф. Технологии Microsoft в Информатике и Программировании — Новосибирск, НГУ, 2004. — С. 94-96.

6. Гаранина Н.О. Аффинное представление данных для проверки моделей программ — Новосибирск, 2004. — 48 с. — (Препр./ Сиб. отд-ние. РАН. ИСИ; N 116)

7. Shilov N.V., Garanina N.O., Kalinina N.A. Model checking knowledge, actions and fixpoints // Proc. Int. Workshop on Concurrency, Specification and Programming — Caputh, Germany, 2004. — v.2, p.351-357.

Личный вклад автора. Результаты, касающиеся теоретических исследований комбинированных логик знаний и действий, а также алгоритма проверки фрагмента ^.-исчисления, получены автором в сотрудничестве с научным руководителем Н.В.Шиловым. Вклад автора состоял в исследовании алгоритмических свойств асинхронных мульти-агентных систем, адаптации определений и утверждений, относящихся к k-деревьям, для проверки на модели формул логики знаний и действий в синхронных системах с абсолютной памятью, а также в доказательстве корректности аппроксимационного алгоритма проверки на модели формул ^-исчисления. Теоретическое исследование аффинных представлений данных и реализация прототипа системы проверки муль-тиагентных систем выполнены автором полностью самостоятельно.

Гаранина Наталья Олеговна

ВЕРИФИКАЦИЯ РАСПРЕДЕЛЕННЫХ СИСТЕМ С ИСПОЛЬЗОВАНИЕМ АФФИННОГО ПРЕДСТАВЛЕНИЯ ДАННЫХ, ЛОГИК ЗНАНИЙ И ДЕЙСТВИЙ

Подписано в печать 19.11.04 Объем 1,1 уч.-изд.л.

Фоомат бумаги 60x84 1/16 Тираж 100 экз.

ЗАО РИЦ "Прайс-курьер" 630090, г. Новосибирск, пр. Акад. Лаврентьева, б, тел. (383-2) 34-22-02

1902

ы

Введение

Актуальность.

Метод верификации моделей программ.

Обзор смежных результатов

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

1 Базовые определения и результаты

1.1 Логики.

1.2 Примеры

1.2.1 Задача о монетках.

1.2.2 Угадывание числа.

2 Алгоритмические проблемы комбинированных логик

2.1 Комбинирование знании и неподвижных точек.

2.2 Алгоритмические проблемы для комбинированных логик

2.3 Асинхронные системы с забывающими агентами.4G

2.4 Синхронные системы с абсолютной памятью.

2.5 Проверка на модели приобретения знании.

2.G Формулы с ограниченной глубиной знаний.5G

3 Аппроксимационный алгоритм для //-исчисления

3.1 Проверка на модели для //-исчисления.G

3.2 Специальная префиксная форма.G

3.3 Полиномиальная проверка на модели.G

Ф 4 Аффинное представление данных

4.1 Модели

4.1.1 Синтаксис.

4.1.2 Семантика.

4.1.3 От нечисловых к числовым. ф 4.1.4 Пример: игра в числа.

4.2 Ограниченные аффинные множества

4.2.1 Представление пропозициональных констант и действий

4.2.2 Операции на аффинных множествах.

4.2.3 Оптимизация.

4.2.4 Проверка включения.

4.3 Векторно-аффинные множества.

4.3.1 Представление пропозициональных констант и действий

4.3.2 Операции на векторно-аффинных множествах.

4.3.3 Оптимизация.

4.3.4 Проверка включения.

4.4 Векторно-аффинные множества versus BDD

4.5 Аффинная проверка на моделях комбинированных логик

4.5.1 Агенты в описании моделей.

4.5.2 Агенты и забывающие агенты.

4.5.3 Агенты с абсолютной памятью.

4.5.4 Представление пропозициональных констант и действий 113 <'И» 4.5.5 Операции на аффинных деревьях.

4.5.G Оптимизация.

4.5.7 Проверка включения.

5 На пути к реализации

5.1 Система проверки на модели Экзаменатор.

5.2 Интерфейс и параметры программы.

5.3 Эксперимент.

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

Актуальность

На сегодняшний день в области создания систем передачи и обработки данных сложилась диспропорция темпов развития трёх её основных компонентов: микропроцессорной техники, средств телекоммуникации и разработки программного обеспечения. Согласно закономерности, замеченной основателем компании Intel Гордоном Муром, быстродействие микропроцессоров удваивается без изменения их стоимости каждые 18 месяцев, пропускная способность каналов передачи данных растёт на 75 % каждые 12 месяцев, и лишь в индустрии программного обеспечения скорость разработки программных систем растёт всего на 4-5 % в год. Это приводит к тому, что разрыв между техническими возможностями и технологиями обработки и передачи информации всё время увеличивается.

В значительной степени, это происходит из-за отсутствия удовлетворительного для промышленности решения проблемы проверки правильности программных систем и логических схем вычислительных устройств. Например, из практики разработки программного обеспечения хорошо известно, что примерно 2/3 времени, затрачиваемого на создание системы, приходится

Ъ на отладку, т.е. проверку её правильности. При создании алгоритма и выборе системы программирования можно руководствоваться многочисленными пособиями, справочниками и пр. Проверка синтаксической правильности программы и её трансляция в исполняемый машинный код осуществляется полностью автоматически. Но этан отладки программ, т.е. проверка семантической правильности, до сих пор плохо автоматизирован. Воспользуемся образным сравнением из [50]:

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

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

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

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

Во многих таких системах естественно возникает понятие знания в силу связи между знанием и действием. Что робот должен знать, чтобы открыть сейф, и откуда он знает, достаточно ли он знает, чтобы открыть его? Перед пересылкой очередного сообщения, знает ли отправитель, что получатель получил предыдущее? В какой момент экономический агент знает уже достаточно, чтобы остановить сбор информации и принять решение? Когда база данных может ответить на вопрос "Я не знаю"? Поэтому часто бывает, что правильность функционирования программной системы зависит от "знаний" её компонентов.

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

Метод верификации моделей программ

Техника верификации, получившая название проверки па модели, является одним из наиболее перспективных и широко используемых подходов к решению проблемы автоматизации отладки и проверки правильности программ. Она была разработана в 80-х гг. Кларком и Эмерсоном в США, а также независимо Квайлом и Сифакисом во Франции. Суть проверки на модели проста, и её этапы можно описать следующим образом:

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

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

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

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

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

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

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

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

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

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

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

Программные логики оказались полезным средством для выражения различных свойств параллельных систем. Традиционно они включают динамические логики, временные логики и их варианты с неподвижными точками [30, 14]. Разнообразие программных логик, используемых для спецификации систем, объясняется не -только тем, что разные логики описывают принципиально разные свойства моделей, но и различной сложностью проверки на модели каждой из них. Можно, конечно, избрать для спецификации свойств программы наиболее мощную по выразительной силе логику, но это грозит обернуться тем, что она может оказаться неразрешимой или её формулы невозможно проверить на модели. Поэтому так важно исследовать теоретически алгоритмические свойства различных логик. Смысл всякой формулы программной логики принято определять но отношению к размеченному графу переходов. Такие структуры называются моделями Крипке.

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

Темпоральные логики позволяют описывать порядок событий во времени без привлечения времени в явном виде. При всём многообразии изученных темпоральных логик, большинство из них содержит оператор вида G<£>, обращающийся в истину в настоящий момент времени, если ip всегда истинно в будущем. Чтобы заявить о том, что события е\ и С2 никогда не могут происходить одновременно, достаточно записать формулу G(->ei V ->е2). Темпоральные логики обычно классифицируются в соответствии с тем, является ли структура времени линейной (например, LTL — Linear Temporal Logic) или ветвящейся (например, CTL — Computational Tree Logic).

С изобретением в начале 80-х гг. Кларком и Эмерсоном алгоритмов проверки на модели для темпоральных логик использование этих логик для анализа поведения распределённых систем удалось автоматизировать. Алгоритм, разработанный Кларком и Эмерсоном для логики ветвящегося времени CTL, имел полиномиальную сложность как относительно размеров модели, определяемой рассматриваемой программой, так и относительно длины её спецификации в темпоральной логике. Позднее Кларк, Эмерсон и Систла предложили улучшенный вариант алгоритма, имеющий линейную сложность относительно произведения длины формулы на размер графа переходов. Алгоритм был реализован в системе верификации ЕМС, которая была широко распространена и использовалась для проверки ряда сетевых протоколов и последовательных схем. Сначала системы верификации моделей были способны проверять графы переходов, содержащие от 105 до 10е состояний со скоростью около 100 состояний в секунду для типичных формул. Несмотря на такие ограничения, верификаторы были успешно использованы для обнаружения ранее неизвестных ошибок в нескольких опубликованных электронных схемах.

Однако темпоральные логики обладают ограниченной выразительной силой: в этих логиках, например, невозможно выразить существование выигрышной стратегии в классе всех конечных игр, таких как параметризованные шахматы и шашки.

Наиболее мощная пропозициональная программная логика — это fi-исчисление с неподвижными точками (/лС) [29]. Свойства моделей программных систем, определимые в динамических или темпоральных логиках, легко выразить с помощью /z-исчисления.

Недавно в семейство программных логик добавились эпистемические логики [18], в частности, пропозициональная логика знаний для п агентов PLK„ (Propositional Logic of Knowledge) и пропозициональная логика общих знаний для п агентов PLCn (Propositional Logic of Common Knowledge). Они позволяют специфицировать такие системы, в которых необходимо проверять утверждения, касающиеся знаний параллельных процессов, которых принято называть агентами. С помощью логик знаний особенно удобно описывать свойства систем, в которых действия распределённых параллельных ироцессов зависят от информации, которой они располагают. К таким программным системам относятся, например, коммуникационные протоколы [23], особенно в ненадёжной среде, и программы управления роботами, получающими информацию от окружающей среды [16]. Проверка на модели систем, специфицированных эпистемическими логиками, позволяет исследовать в этих системах знания, основанные на неполной информации. Иными словами, можно, меняя доступность той или иной информации, проверять как меняется у агента представление о мире и о других агентах. Например: достаточно ли процессу в системе с разделяемыми ресурсами наблюдать параметр занятости ресурса, чтобы знать, когда он освободится, или необходимо иметь доступ к локальной информации остальных процессов (например, к информации о состоянии вычислений). Примером коммерческих систем проверки на моделях, в спецификациях которых используются логики знаний, могут служить программы компании Time-Rover [54], чьим клиентом является, например, NASA.

Однако особенно полезными оказывается комбинаг^ии логик знаний с темпоральными логиками или динамическими логиками действий с неподвижными точками, поскольку они позволяют описывать эволюцию знаний агентов во времени или их изменение в результате каких-либо действий. При рассмотрении временных аспектов знаний возникают системы, различающиеся "разумностью" агентов, действующих в системах. Например, часто рассматриваются забывающие агенты, которые не помнят историю развития событий в системе, а имеют лишь информацию о её текущем состоянии. В противоположность им можно определить агентов с абсолютной памятью, различающих состояния системы, основываясь на запомненных ими истории данных. Кроме того, могут быть синхронные агенты, помнящие, "который час" н асинхронные, не знающие времени. Агенты, чьи знания не зависят от времени, называются обычными агентами.

Подробный обзор состояния теории и практики "классической" проверки моделей программ на конец 1990-х годов можно найти в [10, 50], а теории логик знаний — в [18].

Обзор смежных результатов

Свойства различных комбинированных логик в системах с разнообразными агентами изучаются в течение последних двадцати лет. Например, в 1986 г. в работе [22] Дж.Хальперном и М.Варди изучена задача разрешимости для комбинаций временных логик LTL и CTL с логиками PLKn и PLCn в (а)синхронных системах как забывающих, так и с абсолютной памятью. В частности, показана полнота задачи в данных классах временной сложности1:

CTL-Kn, п > 2 неэлементарное ЕХРТШЕ CTL-Ki = CTL-Ci двойная экспонента ЕХРТШЕ

В [33] в 1998 г. Р.ван дер Мейденом доказано, что задача проверки на модели формул PLCn в системах с абсолютной памятью

• PSPACE-nojum для синхронных систем и

• неразрешима для асинхронных системах.

В работе [34] в 1999 г. Р.ван дер Мейденом и Н.В.Шиловым была изучена задача проверки на модели для комбинаций PLKn и PLC„ с LTL в синхронных системах с абсолютной памятью. В статье показано, что проверка на модели для синхронных систем с абсолютной памятью в случае двух агентов

• является PSPACE-полной для LTL-C2 без UNTIL;

• верхняя и нижняя границы неэлементарны для LTL-K2;

• неразрешима для LTL-C2.

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

JPRS — синхронные системы с абсолютной памятью (Perfect Recall Synchronous Systems), FAS — асинхронные забивающие системы (Forgetful Asynchronous Systems)

PRS

CTL-C„, n > 2 П}

FAS

EXPTIME максимально» вложенности операторов знаний. В статье [34] продемонстрировано, что задача проверки на модели для LTL-Kn в синхронной семантике абсолютной памяти может быть сведена к задаче пустоты автоматов Бюхи с входами, являющимися бесконечными последовательностями таких деревьев.

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

С практической точки зрения интересен вопрос: возможна ли автоматическая проверка на модели для LTL-Kn? Некоторый опыт с древовидными структурами данных описан автором диссертации в [47]. В этом экспериментальном исследовании

• входная конечная среда специфицирована в языке Multi Agent System Language;

• входная LTL-Kn формула не должна иметь негативных/позитивных вхождений модальности знаний Ki/Si для любого агента г G [1 .п];

• инструментом проверки на модели стала программа SMV — верификатор формул LTL в моделях с конечным числом состояний [8, 10].

В 2003 году в Австралии под руководством Р.ван дер Мейдена был разработан прототип системы проверки на моделях МСК [53]. С его помощью можно проверить на модели

1. с асинхронными забывающими агентами формулы логик CTL и LTL в комбинации с логиками знаний PLKn и PLC„;

2. с синхронными забывающими агентами формулы подмножества логики

LTL, содержащее единственный оператор X, и подмножества логики

2нсвыразимос в CTL и LTL

CTL, содержащее операторы АХ и ЕХ, в комбинации с логикой знаний PLKn;

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

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

Вторая составляющая проверки на модели — алгоритмы проверки выполнимости спецификации — представлена большим разнообразием методов. Особенно важны алгоритмы проверки на модели формул //-исчисления, как наиболее выразительной из пропозициональных программных логик. Однако даже самые эффективные из них экспоненциальны относительно размера формулы [11], поэтому целесообразно рассматривать фрагменты //-исчисления, имеющие полиномиальную сложность проверки на модели. В 1993 г. А. Эмерсон, С. Джатла и П. Систла впервые изучили фрагмент //-исчисления, который допускает полиномиальную проверку на конечных моделях [15]. В настоящей работе предложен новый фрагмент, несравнимый по выразительной силе с фрагментом Эмерсона-Джатлы-Систлы.

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

Однако в конце 80-х гг. благодаря использованию двоичных разрешающих диаграмм — структур данных для представления булевых функций — размеры систем переходов, допускающих верификацию методом проверки на модели, поразительно возросли. Новые структуры данных позволили компактно представлять системы переходов и быстро осуществлять их преобразования. В 1987 г. К.МакМиллан показал, что, используя, символьное представление графа переходов, можно верифицировать очень сложные системы [31]. Новое символьное представление было основано на упорядоченных двоичных разрешающих диаграммах (OBDD) Бриана [4]. Представление в виде OBDD является канонической формой для булевых формул, обычно существенно более компактной, нежели конъюнктивные и дизъюнктивные нормальные формы. Для манипуляций с OBDD были разработаны эффективные алгоритмы. Применяя первоначальный вариант алгоритма Кларка и Эмерсона проверки на модели для CTL и новое представление графов переходов, можно провести верификацию некоторых систем, содержащих более 1020 состояний. С тех пор многочисленные улучшения, внесённые другими учёными в технологию верификации на основе OBDD, позволили выполнить ряд экспериментов с числом состояний, достигающим Ю120. Однако формат представления данных в виде OBDD не всегда оказывается эффективным (известны случаи, когда конъюнктивные нормальные формы являются всё-таки более эффективным представлением данных [32]).

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

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

В 1994 г. Б. Бугло и П. Волпер предложили периодические множества для представления множеств состояний [2]. В этой работе периодические множества используются только для вычисления множества достижимых состояний так, что они скорее предназначаются для комбинированного символически-явного подхода в проверке на моделях. Модели в [2] это машины с конечным числом состояний, параметризованных неограниченными целыми переменными, и со следующими операциями: присваивание константы, сложение константы с переменной и проверка пусковых линейных неравенств. Основным недостатком такого представления является то, что оно не допускает полностью символической проверки на моделях: вычисленное множество достижимых состояний может оказаться слишком большим для проверки спецификации модели во всех его элементах.

В 1999 г. Т. Бултан, Р. Гербер и В. Пух разработали систему для символической проверки бесконечных моделей, представляя множества состояний формулами арифметики Пресбургера [7]. Они использовали программу Omega Library [52] для символических манипуляций с формулами Пресбургера. Модели, проверяемые с помощью этой системы, также можно описать формулами арифметики Пресбургера. К достоинствам такого способа представления данных относится то, что можно проверять сколь угодно большие и даже бесконечные модели, но недостатком является тот факт, что сложность оперирования формулами Пресбургера вычислительно дорога: она экспоненциально зависит от размера формул. Кроме того, для некоторых бесконечных моделей алгоритм проверки спецификации может не завершаться.

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

Цели и основные результаты диссертации

Целями диссертации являются

• теоретическое исследование проблемы проверки моделей для новых, более выразительных, комбинаций логик знаний и действий;

• теоретическое исследование новых эффективных алгоритмов и новых, более эффективных, символических форматов представлений данных для логик действий и логик знаний;

• экспериментальная реализация новой системы проверки моделей для комбинированных логик знаний и действий на моделях.

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

1) элементарной динамической логики (EPDL),

2) временной логики на деревьях, расширенной действиями (Act-CTL),

3) //-исчисления (//С) с а) логикой знаний для п агентов (PLKn), b) логикой общих знаний для п агентов (PLCn).

Акцент сделан на задаче проверки на модели комбинированных логик в следовой семантике. Особо рассмотрены два крайних случая: асинхронные конечные системы с забывающими агентами и синхронные конечные системы с абсолютной памятью. В диссертации обобщены деревья знаний из [34]. Также показана возможность сведения задачи проверки на модели для логики Act-CTL-Kn к задаче проверки формул логики Act-CTL в моделях, где состояниями являются деревья знаний. Эти результаты расширяют результаты статьи [34] и тем самым вносят вклад в исследования задач проверки на модели. Ранее они были опубликованы в [38, 39, 40, 42].

Далее, в диссертации описан полиномиальный алгоритм проверки на модели для фрагмента //-исчисления, вычисляющий верхнюю и нижнюю аппроксимацию семантики формулы. Ранее этот алгоритм был опубликован в (41].

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

По результатам теоретических исследований был выполнен машинный эксперимент: реализована программа Экзаменатор — прототип системы проверки моделей

1. с асинхронными забывающими агентами, специфицированными формулами //-исчисления в комбинации с логикой знаний PLKn;

2. с синхронными агентами с абсолютной памятью, специфицированными формулами логики CTL, расширенной действиями, в комбинации с логикой знаний PLK„.

Все полученные результаты являются новыми. Результаты, касающиеся теоретических исследований комбинированных логик знаний и действий, а также алгоритма проверки фрагмента формул /х-исчисления, получены автором в сотрудничестве с научным руководителем Н.В.Шиловым. Вклад автора состоял в исследовании алгоритмических свойств асинхронных муль-тиагентных систем, адаптации понятий, определений и утверждений, относящихся к ^-деревьям, для проверки на модели формул комбинированной логики знаний и действий в синхронных системах с абсолютной памятью, а также в доказательстве корректности апироксимационного алгоритма проверки на модели формул /i-исчисления. Теоретическое исследование новых аффинных представлений данных и реализация прототипа инструмента проверки мультиагентных систем выполнены автором полностью самостоятельно. В частности, но сравнению с упоминавшейся выше программой проверки МСК [53], Экзаменатор позволяет проверять более сложные свойства моделей, специфицированные с помощью более мощных логик.

Предполагается, что основные понятия, относящиеся к теории и практике проверки моделей программ, читателю известны.

Оставшаяся часть работы организована следующим образом.

В главе 1 даются определения и результаты, используемые в диссертации: в разд. 1.1 даются определения базовых логик, а разд. 1.2 посвящен поясняющим сквозным примерам.

Все последующие главы содержат только идеи или эскизы доказательств утверждений и теорем диссертации, а полные доказательства вынесены в приложение А.

В главе 2 рассматриваются алгоритмические проблемы комбинированных логик. В разд.2.1 определяются исследуемые комбинированные логики. Алгоритмические проблемы для комбинированных логик для систем общего вида исследуются в разд.2.2. В разд.2.3 изучаются асинхронные системы с забывающими агентами. В разд.2.4 определяются синхронные системы с абсолютной памятью и показаны их симуляционные возможности. Разд.2.5 посвящен проверке на модели комбинированных логик в этих системах. В разд.2.G более подробно исследуется задача проверки на модели для формул этих логик с ограниченной глубиной знаний.

В главе 3 обосновывается аппрокснмационный алгоритм для фрагмента //-исчисления: в разд.3.1 обсуждается сложность входных параметров задачи проверки на модели для //-исчисления, в разд.3.2 вводится специальная префиксная форма формул //-исчисления, а в разд.3.3 представлен собственно апироксимационный алгоритм.

В главе 4 предлагается аффинное представление данных. Синтаксис и семантика языка описания класса моделей, для которых возможны аффинные представления, изложены в разд.4.1 и там же приведён пример модели. В разд.4.2 описываются собственно аффинные множества: представление множеств состояний, переходов между ними и операции над множествами. Разд.4.3 иосвящён аналогичному описанию векторно-аффинных множеств. В разд.4.4 сравниваются два кодирования данных на примере простой модели — векторно-аффинное представление и BDD-иредставление. В разд.4.5 изложены идеи аффинной проверки на моделях комбинированных логик, в частности, определяются аффинные деревья знаний и манипуляции с ними.

В главе 5 содержится краткое описание прототипа системы проверки на моделях Экзаменатор формул комбинированных логик и небольшого экспериментального теста: задачи об угадывании числа для различных входных параметров.

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

Заключение

В этой главе представлены основные результаты и выводы, для удобства разбитые по категориям.

Комбинированные логики

В работе с теоретической точки зрения изучены алгоритмические проблемы для комбинаций пропозициональных программных логик EPDL-K, EPDL-C, Act-CTL-K, Act-CTL-C, //PLK и /zPLC в средах общего вида, асинхронных забывающих средах и синхронных средах с абсолютной памятью. Для случая общей среды доказана

Теорема 1 Выразительная сила (Е), верхняя граница задачи проверки па модели (М) и сложность разрешимости (D) комбинированных логик EPDL-К, EPDL-C, Act-CTL-K, Act-CTL-C, цРЬК и fiPLC в общем случае семантики удовлетворяют свойствам, представленным па рис.5.1.

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

EXPTIM Е-полная D

EPDL-Cn < Act-CTL-Cn < //PLC линейная М £ линейная М £ exp. М П

EPDL-Kn < Act-CTL-Kn < /iPLK

4 'V/ / ^ линейная М j; линейная М д exp. М

PSPACE-complete D

EXPTIME-полн D

Рис. 5.1: Алгоритмические результаты комбинации логик

Теорема 2 Выразительная сила, задача проверки па модели и разрешимость комбинированных логик EPDL-Kn, EPDL-Cn, Act-CTL-Kn, Act-CTL-' Cn, /iPLKn и fiPLCn в забывающих асинхронных средах эквивалентны выразительной силе, задаче проверки на модели и разрешимости этих логик в общем случае семантики, т.е. удовлетворяют свойствам па рис.5.1.

Ч.

Особое внимание уделено задаче проверки на модели в синхронной среде с абсолютной памятью для логик, комбинирующих знания, действия, и неподвижные точки. Она вносит вклад в исследования проверки на модели и расширяет результаты статьи [34], где задача проверки на модели в синхронной среде с абсолютной памятью исследовалась для комбинации логик PLK и PLC с пропозициональной логикой линейного времени. Доказана

Теорема 3 Для всех п > 1 и Act ф 0, задача проверки па модели для егш-^ хронпых конечно порождённых сред с абсолютной памятью

• является PSPACE-полной для EPDL-Cn;

• разрешимой для Act-CTL-Kn с неэлементарными верхней и ниэ/сией границами, линейно зависящими от размера формул и пеэлсментарно зависящими от числа состояний, агентов и глубины знаний;

• неразрешима для Act-CTL-Cn, цРЬКп, и цРЬСп.

Аппроксимационная проверка на модели

Для формул фрагмента пропозиционального /i-исчисления предложен полиномиальный аппроксимационный алгоритм проверки на модели, вычисляющий верхнюю М(<р) и нижнюю А£(<р) аппроксимацию семантики формул М((р) и доказана

Теорема 4 Для любой формулы tp пропозиционального /i-исчисления, для любой конечной модели М если МХф) — kl{ip), тогда

M(<p) = M(<p) = M(tp).

Аффинные представления данных

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

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

Особенно нужно отметить векторно-аффинное представление деревьев знаний, используемых при проверке формул комбинированной логики знаний и действий Act-СТЬ-Кдг с ограниченной глубиной знаний, равной натуральному числу к, на аффинных моделях. Одно векторно-аффинное дерево может представить множество обычных деревьев знаний мощности сопоставимой с размером модели, причём количество вершин в нём является константой 0(Nk+1), тогда как число вершин в обычном дереве знаний порядка 22 /\ Более того, экспоненциальный размер каждого дерева потенциально можно уменьшить до линейного относительно размера формулы, оставив в дереве лишь те ветви, которые соответствуют структуре вложенных операторов знания в проверяемой формуле. Тогда количество вершин в дереве будет равно количеству операторов знания в проверяемой формуле. Для аффинных систем это позволит снизить неэлементарную сложность проверки на модели формул Act-CTL-Кдг до линейной относительно размера формулы. Детальное исследование этой оптимизации является одной из тем дальнейшей работы.

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

Аффинная проверка на модели для комбинированных логик

Вышеизложенные результаты объединяются в методе аффинной проверки на модели для логик, представимых в //PLCn, в средах с асинхронными забывающими агентами и логик, представимых в Act-CTL-Kn, в средах с синхронными агентами с абсолютной памятью. Первый случай сводится к аффинной проверке на модели для формул /.(-исчисления, а во втором случае применяются аффинные деревья.

Описанный выше метод находится в стадии первичной реализации, выполненной на языке Cjf в среде VisualStudio.NET. На данный момент входными данными являются аффинные модели, описанные в текстовом файле на языке Agent-VEC (4.1,4.5.1) с единственным агентом, асинхронным забывающим или синхронным с абсолютной памятью. Их свойства специфицированы формулами комбинированной логики /гС+PLKi. Выходом является точная семантика формулы или её аппроксимации. Проведён эксперимент с задачей об угадывании числа GN(N, S, М) для различных N, S, М (максимальное N = 15).

1. B. Boigelot and P. Wolper. Symbolic Verification with Periodic Sets // Lect. Notes Comput.Sci. Berlin etc., 1994. — Vol. 818. — P. 55-G7.

2. Borger E., Gnidel E., Gurevich Yu. The Classical Decision Problem. — Berlin etc.: Springer, 1997. 482 p.

3. Bryant R.E. Symbolic boolean manipulation with ordered binary decision diagrams // IEEE Trans. Computers 1986. - Vol. C-35, N 8 - P. 293-318.'

4. Biichi J.R. On a decision method in restricted second order arithmetic // Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science. — Stanford Univ. Press, Stanford, 1960. P. 1-11.

5. Bull R.A., Segerberg K. Basic Modal Logic. — Handbook of Philosophical Logic. — Vol.11. — Reidel Publishing Company, 1984 (1-st ed.). — Kluwer Academic Publishers, 1994 (2-nd ed.). — P. 1-88.

6. Bultan Т., Gerber R., and Pugh W. Model Checking Concurrent Systems With Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results // ACM Trans. Progr. Lang, and Systems 1999. - Vol. 21, N 4 - P. 747-789.

7. Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J.

8. Cleaveland R., Klain M., Steffen B. Faster Model-Checking for Mu

9. Calculus. // Lect. Notes Comput.Sci. — Berlin etc., 1993. Vol.663. — P.410-422.

10. Cousot P., Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints // Proc. of 4-th PoPL. ACM Press, 1977. - P.238-252.

11. Cousot P., Cousot R. Temporal Abstract Interpretation // Proc. of 27-th PoPL. ACM Press, 2000. - P. 12-25.

12. Emerson E.A. Temporal and Modal Logic. — Handbook of Theoretical Computer Science. — Vol.B. — Elsevier, London: The MIT Press, 1990. — P.995-1072.

13. Emerson E.A., Jutla C.S., Sistla A.P. On model-checking for fragments of Mu-Calculus // Lect. Notes Comput. Sci. — 1993. Vol.697. - P.385-396.

14. Engelhardt K., van der Meyden R., Moses Y. A Program Refinement Framework Supporting Reasoning about Knowledge and Time // Lect. Notes Comput. Sci. 2000. - Vol.1784. - P.114-129.

15. Fagin R. Generalized First-Order Spectra and Polynomial-Time Recognizable Sets // Complexity of Computations — SIAM-AMS Proc. — 1974. Vol.7. - P.43-73.

16. Fagin R., Halpern J.Y., Moses Y., Vardi M.Y. Reasoning about Knowledge. London: MIT Press, 1995. — 477 p.ф 19. Fisher M.J. Ladner R.E. Propositional dynamic logic of regular programs

17. J. Comput. System Sci. 1979. - Vol.18, N 2. - P.194-211.

18. Гаранина Н.О. Experiments with Model Checking Knowledge and Time // Ms. Thesis. Mechanics and Mathematics Department of Novosibirsk State. University, 2001 (in Russian).

19. Чеблаков Б.Г. Система разработки математического обеспечения языковыми средствами высокого уровня: Дис. канд. физ.-мат. наук: 01.01.10.- Новоси-бирск, 1980. 121 с.

20. Harel D. First-Order Dynamic Logic // Lect. Notes Comput. Sci. — 1979.- Vol.68.

21. Halpern J.Y., Vardi M.Y. The complexity of Reasoning About Knowledge and Time // Proc. of Symp. on STOC. 1986. - P.304-315.

22. J.Y. Halpern, L.D.Zuck A Little Knowledge Goes a Long Way: Knowledge-Based Derivatons and Correctness for a Family of Protocols.// J. Assoc. Computing Machinery — 1992. Vol. 39, N 3 - P. 449-478.

23. Harel D. First-Order Dynamic Logic. — Berlin etc.: Springer, 1979. — 133 p. — (Lect. Notes Comput. Sci.; 68).

24. Harel D. Dynamic Logic. — Handbook of Philosophical Logic. — Vol.11. — Kluwer Academic Publishers, 1994 (2-nd ed.). P.498-604.

25. Harel D., Kozen D., Tiuryn J. Dynamic Logic. — London: MIT Press, 2000. 459 p.

26. Immerman N. Descriptive Complexity: A Logician's Approach to Computation // Notices of the American Mathematical Society. — 1995.- Vol.42, N 10. P.1127-1133.

27. Immerman I. Descriptive Complexity. — Berlin etc.: Springer, 1999. — 268 Р

28. Kozen D. Results on the Propositional Mu-Calciilus // Theoretical Computer Sci. 1983. - Vol. 27, N 3 - P. 333-354.

29. Kozen D., Tiuryn J. Logics of Programs. — Handbook of Theoretical Computer Science. — Vol.B. — Elsevier, London: The MIT Press, 1990. — P.789-840.

30. McMillan K.L. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993. — 21G p.

31. Meyer A.R.The inherent complexity of theories of ordered sets // Proc. of the Int. Congress of Math., Vancouver. — Vol.2. — Canadian Mathematical Congress, 1974. P.477-482

32. Rabin M.O. Decidability of second order theories and automata on infinite trees // Trans. Ainer. Math. Soc. 1969. - Vol.141. - P.l-35.

33. Rabin M.O. Decidable Theories // Handbook of Mathematical Logic. — ed. Barwise J. and Keisler H.J.- North-Holland Pub. Co., 1977. P.595-630.

34. Shilov N.V., Garanina N.O. Combining Knowledge And Fixpoints // Preprint Novosibirsk, 2002. — 98. - 50 p.

35. Shilov N.V., Garanina N.O. Model Checking Knowledge And Fixpoints // Proc. 4th Int. Workshop on Fixed Points on Computer Science — Copenhagen, Denmark, 2002. — P. 25-39.

36. Shilov N.V., Garanina N.O. Model Checking Knowledge And Fixpoints // Вестник ТГУ. Приложение. Материалы научных конференций, симпозиумов, школ, проводимых в ТГУ. — 2002. — N1(11) — С. 20-23.

37. Shilov N.V., Garanina N.O. A Polynomial Approximations for Model Checking // Lect. Notes Comput.Sci. Berlin etc., 2003. - Vol. 2890. - P. 395-400.

38. Shilov N.V., Garanina N.O., Kalinina N.A. Model checking knowledge, actions and fixpoints // Proc. Int. Workshop on Concurrency, Specification and Programming — Caputh, Germany, 2004. — v.2, p.351-357.

39. Shilov N.V., Yi K. How to find a coin: иронозициональн program logics made easy. // The Bulletin of the European Association for Theoretical' Computer Science 2001. - Vol.75 - P. 127-151.

40. Tarski A. A lattice-theoretical fixpoint theorem and its applications // Pacific J. Math. 1955. - Vol.5. - P.285-309.

41. Thomas W. Infinite trees and automaton-definable relations over o;-words // Theoretical Comput. Sci. 1992. - Vol.103. - P.143-159.4G. Vardi M.Y. Reasoning about the past with two-way automata' // Lect. Notes Comput. Sci. 1998. - Vol.1443. - P.628-G41.

42. Гаранина H.O. Метод проверки моделей для систем, специфицированных в логике знаний и времени. Дне.магистра мат. ио напр. "прикладная математика и информатика— Новосибирск, 2001. — 58 с.

43. Гаранина Н.О. Аффинная проверка моделей программ // Тр. коне]). Технологии Microsoft в Информатике и Программировании — Новосибирск, НГУ, 2004. С. 94-9G.

44. Гаранина Н.О. Аффинное представление данных для проверки моделей программ — Новосибирск, 2004. — 48 с. — (Препр./ Сиб. отд-ние. РАН. ИСИ; N 116)

45. Грамберг О., Кларк Э., Пелед Д. Верификация моделей программ: Пер. с англ. / Под ред. М.А.Захарова. — М.: МЦНМО, 2002. — 41G с.

46. Шилов Н.В., Бодин Е.В., Ии К. О программных логиках — просто. // Теория и методология программирования. — Н.: Наука, 2002.— C.20G-249.52. http://www.cs.iimd.edii/projects/omega/53. http://www.cse.unsw.edu.au/mck/54. http://www.time-rover.com/