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

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

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

Гаранина Наталья Олеговна ВЕРИФИКАЦИЯ РАСПРЕДЕЛЕННЫХ СИСТЕМ С ИСПОЛЬЗОВАНИЕМ АФФИННОГО ПРЕДСТАВЛЕНИЯ ДАННЫХ, ЛОГИК ЗНАНИЙ И ДЕЙСТВИЙ 05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

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

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

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

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

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

Ведущая организация: Тверской государственный университет (г. Тверь)

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

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

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

Автореферат разослан “ ” ноября 2004 г.

Ученый секретарь диссертационного совета K003.032. к.ф.-м.н. Мурзин Ф.А.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2) с синхронными агентами с абсолютной памятью, спе цифицированных формулами логики CTL, расширенной действиями в комбинации с логикой знаний 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 Ap plied Mathematics, (ICAM-2002), Tomsk, Russia, 2002;

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

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

5. International Workshop on Concurrency, Specication and Program ming (CSP 2004), Caputh, Germany, 2004.

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

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

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

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

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

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

В пропозициональной логике общих знаний для n агентов PLCn сим волы отношений являются группами символов агентов, т.е. подмноже ствами множества {1,..., n}, а интерпретация этих отношений являет ся рефлексивно-транзитивным замыканием отношений неразличимости агентов из группы, и, значит, тоже эквивалентностью. В элементарной пропозициональной динамической логике EPDL символы отношений — это символы действий с интерпретацией без каких-либо ограничений.

Во временной логике на деревьях с действиями Act-CTL используются другие модальности: в следующем состоянии, всегда, когда-нибудь и по ка. Так как это ветвящаяся логика, к синтаксису модальностей добавля ются кванторы на каждом пути и на некотором пути, где под путем понимается последовательность состояний, получающаяся в результате повторений некоторого действия. Act-CTL с единственным действием равна известной логике CTL. Пропозициональное µ-исчисление µC — это EPDL, синтаксически расширенная конструкциями неподвижных точек формул, определяющих монотонное преобразование. Показано, что: PLCn — расширение PLKn ;

Act-CTL является расширением EPDL;

µC — расширение Act-CTL. Определено понятие абстракции для поли модальных логик. Оно позволяет формализовать тот факт, что выпол нимость некоторого множества формул (не обязательно тавтологий) со храняется при переходе от конкретной модели к абстрактной. Оказыва ется полезным ввести новое понятие аффинной модели программной си стемы как конечной модели, состояния которой определяются целочис ленными переменными. Кроме того, в описании модели не допускается перемножение этих переменных (умножение на константу допустимо), а все равенства, неравенства и переходы зависят от одной переменной.

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

Во второй главе рассматриваются алгоритмические проблемы ком бинированных логик действий и знаний в различных мультиагентных системах. Для мультиагентных систем общего вида исследуется: 1) срав нительная выразительная сила этих логик;

2) задача проверки на мо дели;

3) разрешимость. Для мультиагентных систем с асинхронными забывающими агентами исследуются те же задачи. Для мультиагент ных систем с синхронными агентами с абсолютной памятью исследуется задача проверки на модели. Более подробно: в разд. 2.1 на основе базо вых логик определяются исследуемые комбинированные логики µPLCn, µPLKn, Act-CTL-Cn, Act-CTL-Kn, EPDL-Cn и EPDL-Kn как синтакси ческая комбинация соответствующих динамических логик и логик зна ний с прежней семантикой, определенной в мультиагентной среде, явля ющейся сочетанием моделей для логик знаний и динамических логик.

В утверждении 4 доказано, что сравнительная выразительная сила логик удовлетворяет следующим неравенствам: EPDL-Kn EPDL-Cn, Act-CTL-Kn Act-CTL-Cn, µPLKn = µPLCn, EPDL-Kn Act-CTL Kn µPLKn и EPDL-Cn Act-CTL-Cn µPLCn.

Алгоритмические проблемы для этих логик в средах, т.е. системах с агентами общего вида, исследуются в разд. 2.2. В утверждении 5 оце нивается сложность задачи проверки на модели: относительно размера модели и формулы она 1) линейна для формул логик EPDL-Kn, EPDL Cn, Act-CTL-Kn, и Act-CTL-Cn и 2) экспоненциальна для формул ло гик µPLKn и µPLCn. Утверждение 6 о проблеме разрешимости: она P SP ACE-полна для EPDL-Kn и EXP T IM E-полна для EPDL-Cn, Act CTL-Kn, Act-CTL-Cn, µPLKn, и µPLCn. Теорема 1 об алгоритмиче ских свойствах изучаемых логик формально объединяет эти утвержде ния. Утверждение 7 конструктивно доказывает возможность исполь зования методов проверки на модели формул µ-исчисления для провер ки формул комбинированных логик.

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

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

утверждение 11 показывает возможность симуляции выполнимости формул слабой логики второго порядка с единственной функцией следования W S(1)S.

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

Разд. 2.5 посвящен проверке на модели комбинированных логик в синхронных системах с абсолютной памятью. В утверждении доказано, что задача проверки на модели при всех n 1: для EPDL Cn — P SP ACE-полна;

для Act-CTL-Kn — разрешима с неэлементар ной верхней и нижней границей;

для Act-CTL-Cn, µPLKn, и µPLCn — неразрешима.

В разд. 2.6 проводится более детальное исследование задачи про верки на модели для формул логики Act-CTL-Kn с ограниченной глу биной знаний. Целями этого исследования являются определение более точных границ задачи проверки на модели для данной логики, а также конструктивный подход к этому методу проверки. В связи с этим опре деляется глубина знаний формулы k как максимальная вложенность модальностей знаний. Новая модификация древовидных структур дан ных — k-деревьев знаний — порождаемых синхронными системами с аб солютной памятью, иллюстрируется на примере задачи об угадывании числа. В утверждении 13 подсчитывается количество k-деревьев над системой и максимальное количество вершин в таких деревьях — они сравнимы с башней экспонент высоты k. Определяются деревья знаний агентов на последовательности состояний как деревья знаний, зави сящие от всех состояний этой последовательности и переходов между ними. Эти деревья отражают знания, приобретенные агентами к по следнему состоянию последовательности. Для k-деревьев определяется функция обновления знаний в результате действий. В утверждении 14 обосновывается корректность функции обновления знаний, т.е. по казано, что деревья знаний агентов на последовательности состояний могут быть получены последовательным применением функция обнов ления знаний к дереву знаний, соответствующему исходному элементу данной последовательности. В утверждении 15 показано, что логи ки Act-CTL-Kn и Act-CTL имеют одинаковую выразительную силу в синхронных системах с абсолютной памятью. С помощью функций об новления знаний определяется класс ассоциированных с синхронными системами с абсолютной памятью конечных моделей Крипке, базирую щихся на k-деревьях. Из утверждения 17 следует возможность про верки формул Act-CTL-Kn с семантикой в бесконечных синхронных си стемах с абсолютной памятью на ассоциированных с ними конечных моделях. Утверждение 18, вследствие учета размера и количества k-деревьев в ассоциированных моделях Крипке, более точно оценива ет сложность задачи проверки на моделях для формул Act-CTL-Kn и вместе с утверждением 12 приводит к теореме 3 об оценке сложно сти задачи проверки на модели комбинированных логик в синхронных системах с абсолютной памятью.

Одним из главных выводов второй главы является то, что провер ка мультиагентных систем, специфицированных формулами комбини рованных логик знаний и действий, так или иначе, сводится к проверке формул µ-исчисления в конечных моделях. Поэтому в третьей гла ве предлагается аппроксимационный алгоритм для вычисления семан тики формул нового фрагмента µ-исчисления, имеющий полиномиаль ную оценку сложности, и обосновывается его корректность. Сначала в разд. 3.1 обсуждаются параметры сложности задачи проверки на модели формул µ-исчисления. Затем в разд. 3.2 вводится специаль ная префиксная форма формулы µ-исчисления, приемлемая для алго ритма проверки, и в утверждениях 19 и 20 показано, что всякую формулу µ-исчисления можно привести к такому виду. Далее в разд.

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

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

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

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

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

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

4.2.4 содержит алгоритм проверки включения множеств и утвержде ние 27 о его корректности и сложности.

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

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

Разд. 4.5 посвящен аффинной проверке на моделях комбинирован ных логик. В подразд. 4.5.1 синтаксис языка описания аффинных мо делей дополнен конструкциями, позволяющими вводить агентов, свя зывая с ними множества наблюдаемых переменных модели. Здесь же определена семантика этих дополнений и среда, ассоциированная с опи санием мультиагентной аффинной модели, чья корректность относи тельно описания среды показана в утверждении 31. Отметим, что из утверждения 7 следует, что свойства мультиагентных сред с обычны ми и забывающими (в силу теоремы 2) агентами, специфицированными в логике µPLCN (и менее выразительных логиках), можно проверять, используя алгоритмы проверки на модели для µ-исчисления. Поэтому в подразд. 4.5.2 определяется векторно-аффинный переход по знани ям, представляющий отношения неразличимости обычных и забываю щих агентов, с использованием понятия наблюдаемых переменных, а именно: переход по знаниям некоторого агента из состояния w возмо жен в те состояния, где значения наблюдаемых переменных совпадают с их значениями в w. В утверждении 32 показана корректность это го представления. В подразд. 4.5.3 рассмотрены новые представления данных для проверки формул Act-CTL-Kn в синхронных системах с аб солютной памятью — векторно-аффинные деревья. Они являются обоб щением векторно-аффинных множеств для кодировки моделей, чьими состояниями являются деревья знаний. Эти структуры — деревья с вер шинами, помеченными аффинными векторами, представляющими мно жество состояний, и ребрами, помеченными агентами. В подразд. 4.5. предлагается метод кодирования с помощью векторно-аффинных дере вьев пропозициональных констант и действий моделей на деревьях, по рожденных аффинными моделями с синхронными агентами с абсолют ной памятью, и в утверждении 33 доказывается его корректность.

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

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

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

В разд. 5.1 описаны входные данные программы: аффинные модели с единственным агентом, со свойствами, специфицированными формула ми логики µC+PLK1, и с указанием типа агента — забывающего или с абсолютной памятью. Также описана структура программы, состо ящая из следующих блоков: обработка входного файла, трансляция в аффинные структуры данных, манипуляция данными, алгоритм про верки и вывод. Выходными данными являются: константа true (f alse), означающая, что спецификации удовлетворяют все (ни одно) состояния модели, либо множество состояний в которых формула спецификации выполняется. В разд. 5.2 описаны интерфейс и параметры программы.

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

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

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

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

2) задача проверки на модели разрешима в синхронных средах с абсолютной памятью для Act-CTL-K.

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

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ 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(II) — С. 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 xpoints // Proc. Int. Workshop on Concurrency, Specication and Programming — Caputh, Germany, 2004. — v.2, p.351– 357.

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

Гаранина Наталья Олеговна ВЕРИФИКАЦИЯ РАСПРЕДЕЛЕННЫХ СИСТЕМ С ИСПОЛЬЗОВАНИЕМ АФФИННОГО ПРЕДСТАВЛЕНИЯ ДАННЫХ, ЛОГИК ЗНАНИЙ И ДЕЙСТВИЙ Подписано в печать 19.11.04 Объем 1,1 уч.-изд.л.

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

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