ПРОГРАММИРОВАНИЕ, 2012, No 6, с. 20-31
= ВОСЬМАЯ ЕРШОВСКАЯ КОНФЕРЕНЦИЯ ПО ИНФОРМАТИКЕ (ПСИ'11) =
УДК 681.3.06
ЭКСПОНЕНЦИАЛЬНОЕ УЛУЧШЕНИЕ ВРЕМЕННОЙ СЛОЖНОСТИ ПРОВЕРКИ МОДЕЛЕЙ ДЛЯ МУЛЬТИАГЕНТНЫХ СИСТЕМ С АБСОЛЮТНОЙ ПАМЯТЬЮ *
© 2012 г. Н.О. Гаранина
Институт систем информатики им. А.П. Ершова СО РАН 630090 Новосибирск, пр. Лаврентьева, 6 E-mail: garanina@iis.nsk.su Поступила в редакцию 01.12.2011
В данной работе пересматривается алгоритм проверки моделей для комбинации логики деревьев вычислений CTL и пропозициональной логики знаний PLK в конечных мультиагентных системах с абсолютной памятью. Новый подход основан на структурах данных, которые имеют экспоненциально меньший размер, чем структуры, использовавшиеся в предыдущей версии этого алгоритма проверки. Таким образом, временная сложность данного алгоритма экспоненциально снижается.
1. ВВЕДЕНИЕ
Комбинации традиционных программных логик [13, 6, 18] с эпистимическими логиками [7, 17] являются хорошо известным формализмом для выражения свойств мультиагентных систем [10]. Многие исследования направлены на разработку техники проверки моделей для мультиагентных систем, специфицированных формулами этих комбинированных логик [2, 5, 11, 14, 15].
Мы исследуем задачу проверки моделей для следовых синхронных мультиагентных систем с абсолютной памятью и различных комбинаций логик знаний с логиками времени и действий. В таких системах у агентов есть память: их знания зависят от пройденных состояний системы и от предыдущих действий. Мы можем описывать агентов такого типа благодаря тому, что семантика знаний определена на следах, т.е. конечных последовательностях состояний и действий, и каждый агент может отличать следы, содержащие различные
* Исследование поддержано Российским фондом фундаментальных исследований (грант 10-01-00532-а) и Интеграционным грантом № 2/12 Сибирского отделения Российской академии наук.
последовательности доступной ему информации. Каждый элемент следа представляет состояние и действие системы в некоторый момент времени.
Задача проверки моделей для таких систем рассматривалась в следующих работах [9], [19], [20]. В работе [9] было показано, что данная задача неразрешима для комбинированных логик знаний и действий АсЬ-СТЬ-Сп, ^РЬКга, и ^РЬСга (где п > 1), но разрешима для АсЬ-СТЬ-КП (с неэлементарной нижней границей). Статья [19] представляет прямолинейный алгоритм проверки на модели логики АсЬ-СТЬ-Кп в синхронных мультиагентных средах с абсолютной памятью. Этот алгоритм проверяет формулы в специальной модели ТКк (Е), элементами которой являются деревья "знаний". Эта модель и деревья имеют неэлементарно экспоненциальный размер. В работе [20] демонстрируется, что модель ТКк(Е), снабженная специальным частичным порядком на деревьях, образует хорошо структурированную помеченную систему переходов [1, 8], в которой каждое свойство, выразимое формулой логики ^-исчисления, может быть охарактеризовано конечным вычислимым множеством максимальных деревьев,
в которых данное свойство выполняется. Эта особенность модели на деревьях позволяет снизить верхнюю временную границу алгоритма проверки моделей, но она все еще остается высокой.
Однако есть другой способ снизить размер состояний модели на деревьях и размер самой модели. В данной статье предложен новый вид деревьев знаний — подрезанные деревья, которые соответствуют структуре проверяемой формулы. Эти деревья экспоненциально меньше, чем обычные деревья знаний. В работе доказано, что семантика каждой формулы комбинированной логики Act-CTL-Kn в модели на деревьях эквивалентна семантике этой формулы в модели на подрезанных деревьях. Более того, мы показываем, что модель на подрезанных деревьях также является хорошо структурированной системой, что приводит к тому, что временная сложность алгоритма проверки моделей может снижаться дополнительно.
2. БАЗОВЫЕ ЛОГИКИ И МОДЕЛИ
Сначала коротко напомним определения комбинированной пропозициональной логики знаний и деревьев вычислений с действиями Act-CTL-Kn из [20]. Эта логика является комбинацией пропозициональной логики знаний PLK [7] и логики деревьев вычислений CTL [6, 3, 4], расширенной символами действий. Семантика Act-CTL-Kn определена в терминах отношения выполнимости |= в средах, которые являются специальным видом помеченных систем переходов.
Пусть {true, false} — булевские константы, Prp и Act — непересекающиеся конечные алфавиты пропозициональных переменных и символов действий, а конечное множество натуральных чисел [1..n] представляет имена агентов (n е N).
Определение 1. (Среда)
Среда это набор E = (D, ~,..,I,V), где
• домен D — непустое множество состояний (миров);
• для каждого агента i е [1..n] отношение
i
неразличимости является отношением
эквивалентности на множестве состояний [1..n] ^ 2DxD;
• интерпретация действий I — всюду определенное отображение I : Act ^ 2DxD ;
• означивание пропозициональных переменных V — всюду определенное тотальное отображение V : Prp ^ 2D.
Для каждого действия a е Act a-пробег — это максимальная последовательность состояний ws = si... sj sj+i... таких, что (sj, sj+i) е I (a) для всех j > 0.
Каждое отношение неразличимости, не являющееся равенством, выражает тот факт, что агент имеет неполную информацию о состояниях системы.
Для иллюстрации некоторых понятий и определений данной работы рассмотрим небольшой пример, называющийся Встреча. Пусть Алиса из Амстердама, Берта из Берлина и Карл из Копенгагена решили встретиться в Париже однажды вечером. Чтобы встреча состоялась, они должны договориться о месте (Эйфелева башня или Монмартр) и о времени встречи (6 или 7 часов вечера). Пусть Place = {E,M} и Time = {6, 7} — это множества мест и моментов времени.
В этом примере средой будет набор Em = (Dm , ~, B ,<CC ,Im ,Vm ). Домен — это множество пятерок Dm = {(p,t,a,b,c) | p е Place,t е Time,a,b,c е {0,1}}, где булевские переменные a, b и c предназначены, чтобы отражать тот факт, что соответствующие агенты проводили или не проводили переговоры друг с другом. Обозначим множество состояний, в которых у Алисы не было переговоров, как Ao = {d е Dm | a = 0}, и множество состояний, в которых у Алисы переговоры были, как Ai = {d е Dm | a = 1}. Множества наличия переговоров для Берты и Карла Bo, Bi, Co, и Ci определяются аналогично.
Отношения неразличимости основаны на том факте, что агент не различает место и время в том и только том случае, если он не вел никаких переговоров. Для агента Алисы эти отношения описываются следующим образом:
• d ~ dd & d,d' е Ao;
• (p, t, 1, b, c) ~ (p, t, 1, b', c'), где p £ Place, t £ Time,b,c,b',c' £ {0,1}.
Отношения неразличимости для Берты и Карла определяются аналогично.
В данной среде агенты могут договариваться о месте p и времени t следующим образом. Пусть множество действий состоит из переговоров Алисы и Берты — AB(p,t), Алисы и Карла — AC(p,t) и Берты и Карла — BC(p,t), где p £ Place, t £ Time. Кроме того, множество действий включает действие talk, которое является недетерминированным выбором из всех возможных переговоров: talk =
U replace,terime AB(p,t) U AC (p,t) U BC (p,t). Например, действие системы AB(p,t) переводит
всякое состояние системы в какое-либо состояние
из множества (p,t, 1,1,c), где c £ {0,1}. Это
означает, что Алиса и Берта договорились
о месте p и времени t, а Карл при этом
мог разговаривать с кем-то из них до того,
либо мог не разговаривать. Формально,
Im(AB(p,t)) = {(d, (p,t, 1,1,c)) | d £ Dm,p £
Place, t £ Time, c £ {0, 1}}. Переговоры AC(p, t)
и BC(p, t) определяются аналогично.
Пусть множеством пропозициональных констант будет {pm,tj}. Пропозициональная переменная pM = {d £ DM | p = M} означает, что место встречи — Монмартр, а пропозициональная переменная tj = {d £ Dm | t = 7} означает, что время встречи — 7 часов вечера.
Определение 2. (Синтаксис Act-CTL-Kn) Синтаксис логики Act-CTL-Kn состоит из формул, стандартным образом построенных из булевских констант, пропозициональных переменных, связок —, Л, V, и следующих модальностей. Пусть i £ [1..n], a £ Act, p и ф будут формулами. Тогда формулами с модальностями являются
• для модальностей знаний1: Kip и Sip;
• для модальностей действий2: AXap, EXap, AGap, EGap, AFap, EFap, Ариаф, и EpUa^.
Синтаксис АсЬ-СТЬ-Кп комбинирует модальности логики знаний РЬК [7] и логики деревьев вычислений СТЬ [6, 3, 4], расширенной символами действий. Семантика Ас£-СТЬ-Кп наследует семантику этих логик.
Определение 3. (Семантика Act-CTL-Kn) Отношение выполнимости = между моделями, состояниями и формулами определено индуктивно согласно структуре формулы. Для булевских констант, пропозициональных переменных и связок отношение выполнимости стандартно. Для модальностей действий это отношение почти такое же, как и для обычных СТЬ-модальностей, но определяется для а-пробегов. Для модальностей знаний выполнимость определяется следующим образом. Пусть ш £ Б, г £ [1..и], р — формула, тогда
w =e (KM) &
для каждого w': w ~ w' влечет w'
w =e (Sip) &
для некоторого w': w ~ w' и w'
--e p;
--E p.
Читается как 'агент г знает' и 'агент г предполагает'.
2Читается как А — 'для всякого будущего', Е — 'для некоторого будущего', X — 'на следующем шаге', О — 'всегда', Е — 'когда-нибудь', и — 'пока', и надстрочный индекс а — 'на а-пробеге'.
Семантика формулы р в среде Е — это множество всех состояний Е, в котором выполняется данная формула:
Е(р) = {ш | ш \=е р}.
Далее в статье мы будем рассматривать только нормальные формулы Ас£-СТЬ-Кп, т.е. формулы, в которых отрицание применяется только к пропозициональным переменным. Всякая формула АсЬ-СТЬ-Кп эквивалентна некоторой нормальной формуле АсЬ-СТЬ-Кп в силу законов Де Моргана и их аналогов.
В нашем примере "Встреча" мы хотели бы проверить следующее утверждение, которое может быть выражено формулой Ас£-СТЬ-Кп. Возможно ли, что в процессе переговоров всех агентов со всеми когда-нибудь выполнится следующий факт: Алиса знает, что Берта знает, что они встретятся на Монмартре, и что Карл предполагает, что время встречи 7 часов; в то время, как Берта предполагает, что Алиса зн
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.