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

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

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

На сегодняшний день в области создания систем передачи и обработки данных сложилась диспропорция темпов развития трёх её основных компонентов: микропроцессорной техники, средств телекоммуникации и разработки программного обеспечения. Согласно закономерности, замеченной основателем компании 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 (.

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

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

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

Особенно нужно отметить векторно-аффинное представление деревьев знаний, используемых при проверке формул комбинированной логики знаний и действий 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).