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

• Автор: Гаранина, Наталья Олеговна
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Новосибирск
• Количество страниц: 165 с.

Оглавление
Введение

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

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

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

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

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

1.1 Логики
1.2 Примеры

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

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

2 Алгоритмические проблемы комбинированных логик
2.1 Комбинирование знаний и неподвижных точек.
2.2 Алгоритмические проблемы для комбинированных логик
2.3 Асинхронные системы с забывающими агентами
2.4 Синхронные системы с абсолютной памятью.
2.5 Проверка па модели приобретения знаний
2.0 Формулы с ограниченной глубиной знаний
3 Апироксимационный алгоритм для дисчисления
3.1 Проверка на модели для дисчисления.
3.2 Специальная префиксная форма
3.3 Полиномиальная проверка на модели.
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 Векторноаффинные множества v .
4.5 Аффинная проверка на моделях комбинированных логик
4.5.1 Агенты в описании моделей.
4.5.2 Агенты и забывающие агенты
4.5.3 Агенты с абсолютной памятью.
4.5.4 Представление пропозициональных констант и действий 3 4.5.5 Операции на аффинных деревьях5
4.5. Оптимизация.
4.5.7 Проверка включения
5 На пути к реализации
5.1 Система проверки на модели Экзаменатор
5.2 Интерфейс и параметры программы.
5.3 Эксперимент.
щ Заключение
Комбинированные логики.
Э Апнроксимационная проверка па модели.
Аффинные представления данных.
Аффинная проверка на модели для комбинированных логик.
Литература


Недавно в семейство программных логик добавились эпистемические логики [], в частности, пропозициональная логика знаний для п агентов PLK„ (Prepositional Logic of Knowledge) и пропозициональная логика общих знаний для п агентов PLCn (Prepositional Logic of Common Knowledge). Они позволяют специфицировать такие системы, в которых необходимо проверять утверждения, касающиеся знаний параллельных процессов, которых принято называть агентами. К таким программным системам относятся, например, коммуникационные протоколы [], особенно и ненадёжной среде, и программы управления роботами, получающими информацию от окружающей среды []. Проверка на модели систем, специфицированных эпистем и вескими логиками, позволяет исследовать в этих системах знания, основанные на неполной информации. Иными словами, можно, меняя доступность той или иной информации, проверять как меняется у агента представление о мире и о других агентах. Например: достаточно ли процессу в системе с разделяемыми ресурсами наблюдать параметр занятости ресурса, чтобы знать, когда он освободится, или необходимо иметь доступ к локальной информации остальных процессов (например, к информации о состоянии вычислений). Примером коммерческих систем проверки на моделях, в спецификациях которых используются логики знаний, могут служить программы компании Типс-Иоусг [5*1], чьим клиентом является, например, МАБ А. Однако особенно полезными оказывается комбинации логик знаний с темпоральными логиками или динамическими логиками действий с неподвижными точками, поскольку они позволяют описывать эволюцию знаний агентов во времени или их изменение в результате каких-либо действий. При рассмотрении временных аспектов знаний возникают системы, различающиеся "разумностью" агентов, действующих в системах. Например, часто рассматриваются забывающие агенты, которые не помнят историю развития событий в системе, а имеют лишь информацию о её текущем состоянии. В противоположность им можно определить агентов с абсолютной памятью, различающих состояния системы, основываясь на запомненных ими истории данных. Кроме того, могут быть синхронные агенты, помнящие, "который -час" и асинхронные, не знающие времени. Агенты, чьи знания не зависят от времени, называются обычными агентами. Подробный обзор состояния теории и практики "классической" проверки моделей программ на конец -х годов можно найти в [, ], а теории логик знаний — в []. Свойства различных комбинированных логик в системах с разнообразными агентами изучаются в течение последних двадцати лет. Например, в г. Дж. Халыюрном и М. Варди изучена задача разрешимости для комбинации временных логик ЬТЬ и СТЬ с логиками РЬК„ и РЬС„ в (а)синхронных системах как забывающих, так и с абсолютной памятью. В [] в г. В работе [] в г. Р.ван дер Мейденом и Н. В.Шиловым была изучена’ задача проверки на модели для комбинаций PLK,t и PLC,, с LTL в синхронных системах с абсолютной памятью. LTL-C2. В статье [] были предложены древовидные структуры данных для проверки на модели логики линейного времени и знаний с ограниченной глубиной знаний. Эти структуры данных очень удобны для представления эволюции и обновления знаний. В статье [3-1] продемонстрировано, что задача проверки на модели для LTL-Kn в синхронной семантике абсолютной памяти может быть сведена к задаче пустоты автоматов Бюхн с входами, являющимися бесконечными последовательностями таких деревьев. Однако перечисленные работы исследуют комбинации только темпоральных логик с логиками знаний. Комбинации же динамической логики с неподвижными точками позволяют выразить более широкий спектр свойств муль-тнагентных систем. Например, при проверке на модели свойства существования выигрышной стратегии2, можно узнать какой минимальной информацией должен располагать агент, чтобы выиграть в конечной игре. Алгоритмические свойства именно таких комбинаций и изучаются в диссертации. С практической точки зрения интересен вопрос: возможна ли автоматическая проверка на модели для LTL-Kn? Некоторый опыт с древовидными структурами данных описан автором диссертации в []. SMV — верификатор формул LTL в моделях с конечным числом состояний [8, ]. В году в Австралии под руководством Р. Мейдена был раз-, работай прототип системы проверки на моделях МСК [].