Программные продукты и системы

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

Основной подход к их верификации основан на так называемом методе проверки на моделях (mo­del checking), который в настоящее время широко используется для верификации моделей с детерминированными и недетерминированными переходами. Верификация – это проверка (или вычисление вероятности) выполнимости некоторого свойства модели. При этом подходе спецификации свойств поведения ВМАС представляются формулами различных темпоральных логик.

В работах [1, 2] показано, как проблема верификации ВМАС в архитектуре IMPACT [3] может быть сведена к верификации конечных цепей Маркова.

В работе [4] описывается вероятностная система верификации PRISM, которая позволяет верифицировать такие модели, как дискретные цепи Маркова, цепи Маркова непрерывного времени, марковские процессы и др., на простом языке, основанном на состояниях.

Рассмотрим программную систему VMASTER [5], позволяющую создавать и редактировать ВМАС, пошагово моделировать их работу и верифицировать созданные системы.

Вероятностные агенты

ВМАС A состоит из набора интеллектуальных агентов {A1, …, AN} и каналов связи CH[i, j] между ними. У каждого агента Ai есть набор параметров {x1, …, xm} и почтовый ящик MsgBoxi, в котором хранятся сообщения, полученные им на текущем шаге от других агентов. Значения параметров и сообщения в почтовом ящике задают состояние агента. Работа агента Ai определяется его управляющей вероятностной программой Pri, которая в зависимости от состояния агента может изменять значения параметров Ai и посылать сообщения другим агентам.

Канал связи CH[i, j] между агентами Ai и Aj – это множество пар {(t1, msg1), …, (tr, …, msgr)}, где msgl – сообщение, отправленное агентом Ai агенту Aj tl шагов назад. Для каждого канала связи определена конечная функция распределения вероятности pCH[i, j](t) – вероятность доставки сообщения от агента Ai агенту Aj не более чем за t шагов. При maxt pCH[i, j](t)<1 возможна потеря сообщения с вероятностью 1–maxtpCH[i, j](t).

Таким образом, глобальное состояние ВМАС включает состояния ее агентов и всех каналов связи. Для ВМАС задается некоторое начальное состояние. Шаг работы ВМАС – это переход от одного состояния системы к другому с некоторой вероятностью.

На каждом шаге работы ВМАС выполняется следующая последовательность операций:

1) предварительное опустошение почтовых ящиков всех агентов;

2) увеличение времени хранения всех сообщений в каналах связи на единицу;

3) доставка сообщений из каналов связи агентам в соответствии с заданными вероятностями;

4) выполнение программ агентов Pr1, …, PrN, приводящее к изменению состояний агентов и помещению новых сообщений в каналы связи.

Язык описания программ агентов. Данный язык представляет собой процедурный Си-подоб­ный язык со следующими возможностями.

·      Три основных типа данных: целое, вещественное, строка.

·      Динамические массивы произвольной размерности.

·      Ссылки.

·      Операторы в выражениях:

а) арифметические: +, –, *, /, ^;

б) операции сравнения: >, <, >=, <=, ==, != ;

в) логические операции: && (и), || (или), !(не);

г) операторы преобразования типов.

·      Локальные и глобальные переменные.

·      Стандартные операторы цикла и условного перехода: while, for, if.

·      Специальные средства для моделирования выполнения вероятностных действий и рассылки сообщений между агентами.

Опишем более подробно специальные операторы для моделирования ВМАС.

1. Сообщения – это некоторые переменные целого типа, обозначающие, доставлено ли сообщение в почтовый ящик с данным именем на текущем шаге (если ее значение 1, то доставлено, если значение 0, то не доставлено). Сообщения могут иметь только те имена, которые использовались в функции message, то есть были посланы каким-либо из агентов.

Оператор отправки сообщения от одного агента другому имеет вид:

message("агент-отправитель", "агент-получа­тель", "сообщение");

Пример:

message("A", "B", "msg1"); // отправка сообщения msg1 от агента A агенту B.

if (msg1= =1) {k:=k+1;} // если сообщение msg1 есть в почтовом ящике, то выполняем какие-либо действия.

2. Вероятностный переход. Имеются три вида функции вероятностного перехода:

random(int n) – возвращает случайное целое число от 1 до n с вероятностью 1/n;

random(double d1, …, double dn) – возвращает случайное целое число k от 1 до n с вероятностью dk; для аргументов должно выполняться условие d1+...+dn=1.

random(double[] a) – возвращает случайное целое число k от 1 до длины массива с вероятностью a[k–1].

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

Пример:

int param1=1;                      // первый параметр агента

double param2=0.2;             // второй параметр агента

int f(int x) {return x^2;}      // некоторая функция

void step()                            // функция шага

{param1=f(param1);} // использование параметра агента

Проектирование ВМАС в программной системе VMASTER. При создании новой ВМАС создается проект, сохраняемый в формате xml. В нем описаны агенты, вероятности каналов связи, а также некоторые настройки.

Вкладка МАС служит редактором мультиагентной системы. Здесь задаются параметры и программы агентов, функции распределения вероятностей для каналов связи.

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

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

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

Пример ВМАС. Рассмотрим систему распределения ресурсов RES, которая включает агента-менеджера m, владеющего некоторым неограниченным ресурсом и распределяющего его среди четырех агентов-пользователей u1, u2, u3, u4, получая от них заказы на этот ресурс. Каждый из агентов-пользователей потребляет ресурс за один шаг. У каждого из них имеется собственная стратегия запросов ресурса:

–      u1 запрашивает ресурс в начальный момент времени, а затем повторяет запрос сразу же после потребления ресурса;

–      u2 запрашивает ресурс сразу после того, как его заказал u1;

–      u3 запрашивает ресурс сразу после того, как u1 получил ресурс от m;

–      u4 запрашивает ресурс на каждом шаге.

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

В таблице 1 показаны функции распределения вероятностей доставки сообщений по каналам связи.

Таблица 1

Отметим, что в канале CH[u1, m] есть вероятность потери сообщений.

Далее приведены программы агентов.

Программа агента m:

int[] Q = new int(4); // очередь

// добавить в очередь

void AddInQ(int agent_number /*=1,2,3,4*/) {

    int i;

    for(i = 0; i < length(Q); i ++)  {

        if(Q[i] == agent_number) {

            //игнорирование агента,

            // если он уже есть в очереди

            return;

        }

        if(Q[i] == 0) {

            // конец очереди

            Q[i] = agent_number;

            return;

        }

    }

}

// удалить из очереди

void DeleteInQ() {

    int i;

    for(i = 0; i < length(Q) - 1; i ++) {

        Q[i] = Q[i + 1];

    }   

    Q[length(Q) - 1] = 0;

}

// Функция шага

void m_Step() {

    // отправка ресурса

    if(Q[0] > 0) {

        if(Q[0] == 1) message("m", "u1", "ok1");

        else if(Q[0] == 2) message("m", "u2", "ok2");

        else if(Q[0] == 3) message("m", "u3", "ok3");

        else if(Q[0] == 4) message("m", "u4", "ok4");

        DeleteInQ();

    }

    // получение запроса на ресурс

    if(mes1) AddInQ(1);

    if(mes2) AddInQ(2);

    if(mes3) AddInQ(3);

    if(mes4) AddInQ(4);

}

Программа агента u1:

//- Параметры агента ******************************

int res1 = 0;

int start = 1;

//- Дополнительные процедуры *********************

void ResourceRequest1() {

    message("u1", "m", "mes1");

}

//- Функция шага

void u1_Step() {

    if(res1 == 1) {

        // потребление ресурса на каждом шаге

        res1=0;

        // повтор запроса сразу после потребления

        ResourceRequest1();

        // оповещение агента u2 о том, что u1 заказал ресурс

        message("u1", "u2", "request1");

    }   

    if(start == 1) {

        // запрос ресурса на первом шаге

        ResourceRequest1();

        // оповещение агента u2 о том, что u1 заказал ресурс

        message("u1", "u2", "request1");

        start = 0;

    }   

    if(ok1) {

        // получение ресурса от менеджера

        res1 = 1;

        // оповещение агента u3 о том, что u1 получил ресурс от менеджера

        message("u1", "u3", "get_resource1");

        return;

    }

}

Программа агента u2:

//- Параметры агента ******************************

int res2 = 0;

//- Дополнительные процедуры *********************

void RequestResource2() {   

    message("u2", "m", "mes2");

}

//- Функция шага

void u2_Step() {

    if(res2 == 1)  {

        // потребление ресурса на каждом шаге

        res2 = 0;

    }   

    if(request1) {

        //u2 запрашивает ресурс сразу после того, как его запросил u1

        RequestResource2();

    }   

    if(ok2) {       

        // получение ресурса от менеджера

        res2 = 1;

        return;

    }

}

Программа агента u3:

//- Параметры агента ******************************

int res3 = 0;

//- Дополнительные процедуры *********************

void RequestResource3() {

    message("u3", "m", "mes3");

}

//- Функция шага

void u3_Step() {

    if(res3 == 1) {

        // потребление ресурса на каждом шаге

        res3 = 0;

    }   

    if(get_resource1) {

        //u3 запрашивает ресурс сразу после того, как его получил u1

        RequestResource3();

    }   

    if(ok3) {       

        // получение ресурса от менеджера

        res3 = 1;

        return;

    }

}

Программа агента u4:

//- Параметры агента ******************************

int res4 = 0;

//- Дополнительные процедуры *********************

void RequestResource4() {

    message("u4", "m", "mes4");

}

//- Функция шага

void u4_Step() {

    if(res4 == 1) {

        // потребление ресурса на каждом шаге

        res4 = 0;

    }   

    if(ok4)  {

        // получение ресурса от менеджера

        res4 = 1;

    }   

    // запрашивает ресурс на каждом шаге

    RequestResource4();

}

Верификация ВМАС

Темпоральные логики. Состояния ВМАС и вероятностные переходы между ними образуют граф состояний, который может быть промоделирован цепью Маркова. Такую модель можно верифицировать: находить вероятность выполнения какого-либо свойства на состояниях, а также бесконечных траекториях графа состояний или выяснять, будет ли выполнено свойство с заданной вероятностью для всех путей из некоторого состояния. Свойства поведения ВМАС описываются формулами темпоральных логик линейного и ветвящегося времени [6, 7]. В системе VMASTER для верификации используются темпоральные логики PLTL (линейного времени) и PCTL (ветвящегося времени), а также их модификации, предлагаемые автором. Кратко опишем эти логики.

1. PLTL (Propositional Linear Temporal Logic). Это темпоральная логика линейного времени. Формулы PLTL  выражают свойства бесконечных траекторий графа состояний ВМАС:

Ф::=true|a| ФÙФ|ФÚФ|ØФ|X(Ф)|ФÈФ, где a – пропозициональная переменная; X(Ф) – оператор Next, который требует, чтобы свойство Ф выполнялось во втором состоянии пути; Ф1ÈФ2 – оператор Until; выполняется, если на пути имеется состояние, в котором соблюдается свойство Ф2 и в каждом предшествующем состоянии этого пути соблюдается свойство Ф1.

Кроме того, в формулах можно использовать дополнительные операторы:

F f≡trueÈf – оператор будущего;

G f≡ØF(Øf) – оператор инвариантности.

2. PCTL (Probabilistic Computation Tree Logic). Это темпоральная логика ветвящегося времени. Формулы PCTL выражают свойства деревьев вычислений:

Ф::=true|a|ФÙФ|ФÚФ|ØФ|[X(Ф)]Êp| [ФÈФ]Êp

Здесь ÊÎ{³, >}, pÎ[0; 1]; a – пропозициональная переменная.

В этой логике формула вида [X(Ф)] Êp выполнена, если с вероятностью Êp на следующем состоянии выполнена Ф, а формула вида [Ф1ÈФ2] Êp выполнена, если с вероятностью Êp существует путь, где на некотором его состоянии выполнена Ф2, а на всех предыдущих состояниях этого пути выполнена Ф1.

3. Ограниченный PLTL.

Это подмножество PLTL без оператора Until, но с оператором ограниченный Until:

Ф::=true|a|ФÙФ|ФÚФ|ØФ|X(Ф)|ΨÈ≤kΨ

Ψ::=true|a|ΨÙΨ|ΨÚΨ|ØΨ|X(Ψ)).

4. Расширенный PCTL.

Расширяем PCTL, добавляя формулы вида

Ф::=[X(k, Ф) Êp|XOR(k, Ф)] Êp|[XAND(k, Ф)] Êp, (k≥1, целое)

ÊÎ{ ³, >}, p [0; 1], k≥1 – целое.

Эти формулы имеют следующий смысл:

[X(k, Ф)] Êp – выполнена, если с вероятностью Êp есть путь, точно на k-м состоянии которого выполнена Ф;

[XOR(k, Ф)] Êp – выполнена, если с вероятностью Êp существует путь, для которого существует такое 1≤i≤k, что на i-м состоянии этого пути выполнена Ф;

[XAND(k, Ф)] Êp – выполнена, если с вероятностью Êp существует путь, для которого для всех 1≤i≤k на i-м состоянии этого пути выполнена Ф.

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

1. CY – верификация формулы логики PLTL алгоритмом из [8] с некоторыми модификациями. Кроме стандартных темпоральных операторов X и U, в язык добавлены следующие операторы:

X(k, f) – оператор, эквивалентный Xk(f);

X_OR(k, f) – оператор, эквивалентный X(f)ÚX2(f)Ú … ÚXk(f);

X_AND(k, f) – оператор, эквивалентный X(f)ÙX2(f)Ù … Ù Xk(f) (k≥1 – целое число).

Отметим, что при верификации новые операторы X(k, f), X_OR(k, f) и X_AND(k, f) в формулах не раскрываются в соответствии с эквивалентностями (а), (б), (в), а обрабатываются специальным, более быстрым алгоритмом, имеющим линейную от k сложность.

2. k-find – поиск минимального числа шагов k, такого, что заданная формула f логики PLTL будет выполняться с заданной вероятностью ровно через k шагов. Заданная формула f верифицируется алгоритмом из [8], а число шагов k находится специально разработанным автором алгоритмом за линейное время от k.

3. GTP – верификация формулы ограниченной логики PLTL. Для этой логики разработан специальный алгоритм полиномиальной сложности от размера формулы и размера цепи Маркова. Он строит по цепи Маркова некоторый граф, позволяющий получить все траектории, на которых истинна верифицируемая формула, и определить вероятность ее выполнения.

4. CY+GTP – верификация с совместным использованием CY и GTP.

5. PCTL – верификация формул расширенной логики PCTL с помощью обобщенного алгоритма верификации. Для логики PCTL существует алгоритм верификации полиномиальной сложности от размера модели и размера формулы, представленный в [9]. Для расширенного PCTL автором был обобщен этот алгоритм, причем сохранены его оценки сложности: он является полиномиальным от размера модели, размера формулы и максимального k.

Верификация в программной системе VMAS­TER. Вкладка Верификация служит для верификации цепей Маркова, полученной по рассматриваемой ВМАС. На ней также можно просмотреть некоторую информацию о пространстве состояний системы.

Перед началом верификации спроектированная ВМАС транслируется в цепь Маркова командой меню Проект → Создать цепь Маркова. При успешном создании цепи Маркова информация о ней отображается в поле Построение цепи Маркова. Цепь Маркова можно сохранять и загружать независимо от проекта командами меню Файл → Загрузить цепь Маркова… и Файл → Сохранить цепь Маркова…

Формулу логики PLTL, которую требуется верифицировать, нужно вводить в поле Верификация формулы. В качестве параметров формулы могут использоваться имена параметров агентов, константы, имена сообщений. В формуле могут использоваться стандартные операторы, а также объявленные в программе ВМАС (в том числе и модулях) пользовательские функции (которые не меняют значение параметров, а лишь возвращают его). Выражение формулы должно возвращать значение типа int. Темпоральные операторы, которые могут быть использованы в формулах верификации, а также структуры таких формул зависят от выбранного режима верификации. Выбор режима осуществляется нажатием на одну из кнопок панели слева от ввода формулы. Результат верификации отображается в соответствующем поле.

Группа кнопок Пространство состояний внизу окна предоставляет возможность получить некоторую дополнительную информацию о состоянии модели.

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

МАС – просмотр состояний ВМАС и возможность просмотра допустимых переходов из любого состояния.

ГИП – отображение графа истинных траекторий, получаемого после верификации в режимах GTP или CY+GTP.

Параметры – отображение всевозможных значений параметров на всех состояниях цепи Маркова в виде списка.

Пример верификации. Рассмотрим верификацию определенной ранее ВМАС RES. Цепь Маркова, построенная по ней, имеет следующие характеристики: количество состояний – 124 841, количество переменных – 16, количество начальных состояний – 1, количество имен сообщений – 10, количество переходов – 1 483 620, минимальное число переходов из состояния – 2, максимальное число переходов из состояния – 64.

В таблице 2 приведены результаты верификации некоторых формул на полученной цепи Маркова. Верификация производилась на процессоре Intel(R) Core(TM) i7-2700K CPU @ 3.50GHz.

Как видно из таблицы 2, на скорость работы алгоритма CY существенно влияет число темпоральных операторов (например, формула F(res2 Ù X(res2)) с двумя темпоральными операторами верифицируется значительно дольше, чем формулы с одним). Последняя формула в таблице 2 U(30, 1, res2 && res3 && res4) содержит 30 темпоральных операторов, что дает еще большее время верификации, но, благодаря использованию полиномиального алгоритма GTP, это время гораздо меньше, чем время верификации эквивалентной формулы алгоритмом CY.

Автор благодарит М.И. Дехтяря за постановку задач и постоянную поддержку и М.К. Валиева за полезное обсуждение работы.

Литература

1.     Валиев М.К., Дехтярь М.И. О сложности верификации недетерминированных вероятностных мультиагентных систем // Моделирование и анализ информационных систем. 2010. Т. 17. № 4. С. 41–50.

2.     Dekhtyar M., Dikovsky A., Valiev M., LNCS, 2008, Vol. 4800, pp. 256–265.

3.     Subrahmanian V.S., Bonatti P., Dix J., Eiter T., Kraus S., Ozcan F. and Ross R., Heterogeneous Agent Systems, MIT Press, 2000.

4.     Kwiatkowska M., Proc. 18th IEEE Symp. «LICS'03», IEEE Computer Society Press, 2003, pp. 351–360.

5.     Лебедев П.В. Программа верификации вероятностных многоагентных систем // 12-я национальн. конф. по искусств. интел. с междунар. участ. 2010. Т. 4. С. 81–88.

6.     Baier C., Katoen J.-P., Principles of model checking, MIT Press, 2008.

7.     Clarke E.M., Grumberg O., Peled D.A., Model checking, MIT Press, 1999.

8.     Courcoubetis C., Yannakakis M., Jorn. ACM, 1995, Vol. 42, no. 4, pp. 857–907.

9.     Hansson H., Jonsson B., A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, no. 6(5), pp. 512–535.

References

1.  Valiev M.K., Dekhtyar M.I.,  Modelirovanie i  analiz in-formatsionnykh system  [Modeling and Analysis of Inform. Sys-tems], 2010, Vol. 17, no. 4, pp. 41 –50.

2.  Dekhtyar M., Dikovsky A., Valiev M.,  LNCS, 2008, no. 4800, pp. 256–265.

3.  Subrahmanian V.S., Bonatti P., Dix J.,  Eiter T., Kraus S., Ozcan F., Ross R., Heterogeneous Agent Systems, MIT Press, 2000.

4.  Kwiatkowska M.,  Proc. 18th IEEE LICS'03, IEEE Com-puter Society Press, 2003, pp. 351–360.

5.  Lebedev P.V.,  XII natsionalnaya konf. po iskusstvennomu intellectu s mezhdunar. uchast. [12th National Conf. on artificial in-telligence with int. participation], 2010, Vol. 4, pp. 81–88.

6.  Baier C., Katoen J.-P.,  Principles of model checking, MIT Press, 2008.

7.  Clarke E.M., Grumberg O., Peled D.A.,  Model checking, MIT Press, 1999.

8.  Courcoubetis C., Yannakakis M.,  JACM, 1995, Vol. 42, no. 4, pp. 857–907.

9.  Hansson H., Jonsson B.,  Formal Aspects of Computing, 1994, no. 6(5), pp. 512–535.