zaeto.ru

4. Практическая часть

Другое
Экономика
Финансы
Маркетинг
Астрономия
География
Туризм
Биология
История
Информатика
Культура
Математика
Физика
Философия
Химия
Банк
Право
Военное дело
Бухгалтерия
Журналистика
Спорт
Психология
Литература
Музыка
Медицина
добавить свой файл
 

 
страница 1 страница 2 ... страница 8 страница 9




САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ

УНИВЕРСИТЕТ

Математико-механический факультет

Кафедра системного программирования

Логический подход к спецификации мультиагентных систем с вероятностным поведением

Дипломная работа студента 545 группы Сынтульского Сергея


Научный руководитель, ____________ Игорь Павлович Соловьев

кфмн
Рецензент, ____________



1. Введение 4

1.1. Темпоральные логики 4

1.1.1. Представление времени в логиках 5

1.1.2. Темпоральные логики 7

1.1.3. Вероятностные темпоральные логики 10

1.2. Символьная реализация алгоритмов проверки модели 12

1.3. Представление вероятностных моделей с использованием языка PRISM 13

1.4. Оптимизация на основе марковской модели 16

2. Классы задач 18

2.1. Задачи мультиагентных систем 18

2.2. Задачи логик с альтернирующим временем 19

2.3. Задачи вероятностных логик 20

2.4. Области приложений PTATL 21

3. Вероятностная логика с альтернирующим временем и явными временными ограничениями 22

3.1. Вероятностная структура параллельной игры 22

3.1.1. Представление PCGS с помощью PRISM 23

3.1.2. Пример модели рынка 24

3.2. Внутренний язык 27

3.2.1. Синтаксис 27

3.2.2. Семантика 27

3.3. Синтаксис PTATL 28

3.3.1. Квантор возможности 30

3.3.2. Дополнительные операторы 31

3.4. Семантика PTATL 31

3.4.1. Стратегии и выходы 31

3.4.2. Семантика PTATLs 32

3.4.3. Время в PTATLc 33

3.4.4. Семантика PTATLc 34

4. Практическая часть. Методы проверки модели 35

4.1. Метод проверки модели для PTATLc 35

4.1.1. Проверка модели для формул, образованных нетемпоральными операторами 36

4.1.2. Проверка модели для утверждений о следующем состоянии 36

4.1.3. Проверка модели для формул, образованных оператором U 37

4.1.4. Проверка модели для формул, образованных оператором W 39

4.2. Алгоритм проверки модели для PTATLs 39

4.2.1. Преобразование PCGS в MDP 40

4.2.2. Пример преобразования PCGS в MDP 42

4.2.3. Служебные функции 44

4.2.4. Проверка модели для утверждений о следующем состоянии 45

4.2.5. Проверка модели для ограниченного оператора Until 46

5. Приложения 47

5.1. Моделирование производственных систем 47

5.2. Приложения в области финансов 50

5.2.1. Задача вывода инвестиций из разоряющегося предприятия 50

5.2.2. Оценка контрактов 52

5.3. Приложения в области медицины 56

6. Заключение 57

7. Литература 58

7.1. Моделирование производственных систем 60

7.2. Формально-логические подходы в медицине 60

7.3. Финансовая математика 61

  1. Введение


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

В данной работе предлагается логический подход к спецификации систем, состоящих из нескольких агентов, действия которых могут оказывать недетерминированный (вероятностный) эффект на состояние системы в целом. А именно, автором предлагается логика PTATL (Probabilistic Timed Temporal Logic), позволяющая для модели системы описывать способность различных групп агентов повлиять на ее состояние.

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

Изложение имеет следующий план. Во введении описываются темпоральные логики, а также ключевые аспекты реализации инструментов проверки моделей. Глава 2 содержит описания ряда прикладных областей, для решения задач которых могла бы быть применена предлагаемая в данной работе логика PTATL. В главе 3 приводится описание синтаксиса и семантики PTATL. В главе 4 описываются алгоритмы проверки моделей. В заключительной главе 5 рассматриваются примеры решения конкретных задач некоторых из предложенных в главе 2 областей.


    1. Темпоральные логики


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

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

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

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

Структуры Крипке предназначены для описания последовательных систем. Для моделирования параллельных мультиагентных систем вводят аналогичные модели – структуры параллельных игр (Concurrent Game Structure, CGS) и системы с альтернирующими переходами (Alternating Transitions System, ATS). Эти модели отличаются от структур Крипке тем, что в каждом состоянии выбор следующего состояния является решением, принимаемым сразу всеми агентами системы. Между собой они отличаются способом задания переходов. На данном этапе это различие несущественно.

В том случае, если моделируемая система имеет вероятностный характер, вместо структур Крипке используют марковские модели (марковские цепи или марковские процессы принятия решений). На основе таких моделей строятся различные вероятностные темпоральные логики.

Вероятностная темпоральная логика с альтернирующим временем и явными временными ограничениями PTATL (Probabilistic Timed Alternating-Time Temporal Logic), которая предлагается в данной работе, объединяет подход к описанию свойств мультиагентных систем с помощью логики с альтернирующим временем (см. напр. [RHK02]) и вероятностный подход. По мнению, представленному в работе [B05], где описываются открытые задачи логики и теории игр, и по нашему мнению, проблема углубления интеграции логики в теории игр с теорией вероятности является актуальной.

Логика PTATL позволяет описывать поведение систем, в которых агенты действуют в вероятностном окружении. При этом действовать агенты могут как согласованно, так и друг против друга.

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


  • представление времени в логиках,

  • темпоральные логики,

  • вероятностные темпоральные логики.
      1. Представление времени в логиках


Темпоральные логики предназначены для описания свойств вычислений, которые могут осуществляться в рамках моделируемой системы, причем таких, для описания которых существенна возможность представления времени. В большинстве темпоральных логик для этого используются темпоральные операторы. Однако, это – не единственный способ представления времени в логиках. Приведем описания трех основных способов [W92].

Логика первого порядка

Утверждения, в которых задействовано время, могут быть сформулированы с использованием средств логики первого порядка, позволяющей строить функциональные выражения, зависящие от времени. Например, каждый n-местный предикат может быть превращен в n+1-местный добавлением временного аргумента. Такой временной аргумент позволяет задать время выполнения предиката на данном наборе значений. При таком представлении времени предложение “A никогда не болеет” записывается следующим образом:



.

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



Метаязык первого порядка

Вторым подходом к работе со временем является использование метаязыка первого порядка, состоящего из набора предикатов наподобие Holds или True, принимающих атом основного языка и временной параметр и возвращающих соответствующее значение истинности. В рамках этого подхода предложение "A никогда не болеет" может записываться так



Такой подход называется материализованным (reified). Его недостатком считается недостаточная наглядность и относительная сложность логического аппарата.



Темпоральные операторы

Третий подход формулировки временных фактов основан на применении темпоральных операторов. Набор стандартных операторов темпоральной логики включает операторы ("на следующем ходу"), ("всегда") , ("когда-нибудь"), U ("до тех пор, как").

Выражение "A никогда не болеет" с помощью темпорального оператора может быть записано так

.

В ряде случаев, стандартного набора темпоральных операторов недостаточно. Это связано с тем, что в базовом варианте они не приспособлены для описания ограничений на длительность сроков (например, утверждение вида “условие должно выполняться в течение десяти дней” не может быть выражено с их помощью).

Существуют два основных подхода для определения временных ограничений в темпоральных логиках [LST00]. Первый подход использует явно определяемые в формулах точки отсчета времени и связанные с ними переменные (обычно такие переменные называют часами), на основе которых могут определяться временные ограничения. Примерами логик, которая базируется на таком подходе, является TATL [HP06] и [LST00].

Утверждение "A не болеет в течение десяти шагов" записывается с использованием часов следующим образом



.

Альтернативным подходом является использование операторов с ограничениями ([LST00], PCTL [HJ94], PBTL [CK98]).

В случае операторов с ограничениями с каждым оператором связывается новая система отсчета времени, однако она может использоваться только в ограничениях этого оператора, что существенно упрощает процедуру проверки моделей по сравнению со случаем часов. Для подхода, базирующегося на часах, вычислительная сложность алгоритма проверки моделей является экспоненциальной, а при использовании операторов с ограничениями – полиномиальной [LST00]. В рамках данного подхода утверждение "A не болеет в течение десяти шагов" записывается так

.

В работе [LST00] показана связь между этими двумя типами ограничений и предложен алгоритм перехода (конвертации формул) между ними для временных расширений CTL. Хотя оба способа представления ограничений и эквивалентны с точки зрения выразительности, размер формулы (при переходе от представления временных ограничений на основе часов к операторам с ограничениями) может увеличиваться экспоненциально.

В данной работе разрабатываются две версии PTATL - (s - сокращение subscriptions), использующая операторы с ограничениями, и (с – сокращение от clocks), использующая часы. Заметим, что, в обоих случаях ограничения имеют не произвольный вид, а ограничиваются неравенствами между временными переменными и числовыми константами и конъюнкциями этих неравенств (в случае операторов с ограничениями неравенство всегда одно).

      1. Темпоральные логики


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

LTL

В 1977 для описания требований к реактивным системам была предложена логика с линейным временем (LTL) [Pnu77]. LTL может интерпретироваться относительно цепочки состояний структуры Крипке.



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

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

Синтаксически логика LTL расширяет пропозициональную логику темпоральными операторами. Синтаксис LTL определяется следующим образом

.

В приведенной выше формуле a – пропозициональная переменная, а темпоральные операторы имеют следующий смысл



  • выполнится на следующем ходу,

  • будет выполнено всегда, начиная с текущего состояния,

  • будет выполнено когда-нибудь в будущем или текущем состоянии,

  • будет выполняться до тех пор, пока не будет выполнено .

Пример

Формула LTL означает, что если некто болен, то он обязательно выздоровеет.



CTL

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

Для того чтобы обойти это ограничение, вводится логика с ветвящимся временем CTL (Computational Tree Logic) [CE81], в которой можно явно задать кванторы существования и универсальные кванторы на множестве возможных вычислений.

Логика CTL включает два типа формул: формулы состояний и формулы путей. Формулы состояний определяются как



,

где - это формула пути.

Определим теперь синтаксис формулы пути

,

где - формулы состояния.

Интерпретацией формулы состояния CTL является дерево вычислений (из каждого состояния ведет несколько переходов). Семантика формулы пути определяется аналогично семантике формул LTL.

Формула состояния означает, что в дереве есть бесконечный путь, начинающийся в корне (вычисление), который удовлетворяет формуле пути . А формула - что любое вычисление в дереве удовлетворяет .

Отношение выполнимости для формул состояния CTL, как и в случае LTL, определяется на паре из структуры Крипке и ее состояния. Деревом вычислений при этом является развертка графа (факторизованное множество всех возможных путей, начинающихся в данном состоянии) структуры Крипке из данного состояния.

Пример

Формула CTL означает, что если некто болен, то он всегда имеет шанс выздороветь.



ATL

LTL и CTL интерпретируются над структурами Крипке, которые представляют собой вычислительную модель закрытых систем, а именно систем, поведение которых полностью определяется состоянием. Моделирование реактивных систем как набора действующих компонентов предполагает рассмотрение каждого компонента как открытой подсистемы, которая взаимодействует с окружением и чье поведение зависит как от собственного состояния, так и от состояния окружения.

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

Такая квантификация формулы множеством компонентов называется альтернацией и является естественным расширением универсального и экзистенциального кванторов. Логики, в которых возможна такая квантификация, называются логиками с альтернирующим временем.

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

Пример

формула ATL означает, что пациент a может вести себя таким образом, чтобы любая болезнь могла бы быть вылечена при помощи врача b.

Семантика логики ATL [RHK02] определяется на основе структур параллельных игр (Concurrent Game Structure, CGS) и систем с альтернирующими переходами (Alternating Transitions System, ATS). Различия между этими моделями для нас сейчас не существенны. Параллельные структуры игр представляют собой структуры Крипке, ребра которых помечены не единичными действиями, а кортежами действий – по одному для каждого агента. Временное расширение ATL – TATL определяется на более сложной структуре – конечноавтоматных играх с явным представлением времени [HP06], в простейшем случае это означает, что каждому переходу сопоставлено целое число, являющееся его длительностью.

В работе [RHK02] представлены некоторые логики с альтернирующим временем: ATL, ATL*, GL. В статье [Pa00] представлена аналогичная логика CL и ее применение к ряду задач теории игр.

Существуют такие логики с альтернирующим временем [SGHW06], которые позволяют не только доказывать утверждения о достижимости состояний, но и непосредственно выводить необходимые для этого действия. Это позволяет связать логики c альтернирующим временем и формальные методы разработки программ (напр. [Utt92]).

      1. Вероятностные темпоральные логики


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

Альтернативным способом представления недетерминизма являются вероятностные модели. В качестве вероятностной интерпретации темпоральных логик, как правило, выступает марковская цепь. Существует несколько темпоральных вероятностных логик. Например, логики PTL (расширение LTL) [CT00], PCTL [HJ94] и PBTL [СK98] (расширения CTL).



PCTL

PCTL является наиболее распространенной вероятностной логикой. В ней универсальный квантор и квантор существования CTL заменены оценкой вероятности. Синтаксис PCTL [HJ94] заимствован из CTL и, кроме вероятностных конструкций, расширен временными ограничениями, которые реализуются с помощью операторов с ограничениями.



Выражения PCTL порождаются следующей грамматикой.

.

Пример

Формула CTL из предыдущего раздела может быть переписана как , где накладывает ограничение c на вероятность выполнения формулы. Формула означает, что, в случае возникновения, болезнь будет вылечена с вероятностью 0.8.



Вероятностные структуры для темпоральных логик

В качестве структуры, на основе которой определяется семантика PCTL, может быть выбрана либо марковская цепь c дискретным временем [HJ94] [P02], либо марковский процесс принятия решений [P02].



Марковская цепь c дискретным временем (Discrete Time Markov Chain) – это структура состояний и переходов, в которой каждый переход имеет определенную вероятность, причем сумма вероятностей для исходящих переходов в каждом состоянии должна быть равна 1. Как и в случае структуры Крипке, данная модель включает конечное множество пропозициональных переменных, и каждому состоянию сопоставляется множество тех пропозициональных переменных, которые истинны в этом состоянии.

Формально марковская цепь (как модель для PCTL) определяется как набор , состоящий из



  • конечного множества состояний Q,

  • начального состояния ,

  • функции оценки вероятности переходов между состояниями p,

  • конечного множества наблюдаемых величин Г,

  • функции означивания наблюдаемых величин .

Марковская цепь хорошо подходит для моделирования полностью вероятностных систем. Однако, для моделирования систем, в рамках которых могут приниматься сознательные решения, требуется расширение этой модели. Таким расширением является марковский процесс принятия решений (Markov Decision Process). Эта модель включает состояния, действия и переходы. Для каждого состояния определено множество допустимых действий. Каждому состоянию и допустимому в нем действию сопоставляется множество переходов с вероятностями, в сумме дающими единицу.

Приведем формальное определение марковского процесса принятия решений. Марковский процесс принятия решений – это кортеж .



  • Q – это конечное множество состояний,

  • A – конечное множество действий,

  • - начальное состояние,

  • - конечное множество наблюдаемых величин,

  • d – функция, сопоставляющая каждому состоянию множество доступных в нем действий,

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

  • - функция, сопоставляющая значение каждой наблюдаемой величине и состоянию.

На основе марковского процесса принятий решений также может быть определена семантика PCTL [P02]. Для этого типа структур оператор имеет следующий смысл: независимо от выбора действий вероятность формулы удовлетворяет ограничению с. Аналогичные утверждения о существовании действий (а не о любом действии) могут быть представлены в двойственной форме. Например, для утверждения о том, что формула должна выполняться c вероятностью не меньшей p хотя бы для одного действия (а не для любых как в случае ), записывается как .

Другими логиками, семантика которых определяется на основе марковских процессов принятия решений, являются логики PBTL [LST00] и GPL [NCI99]. Логика PBTL не отличается от PCTL по своей выразительности и очень незначительно отличается по синтаксису. Логика GPL отличается тем, что позволяет включать в формулы условия на выполнение действий и классов действий.

Естественным расширением существующих вероятностных логик является их адаптация для описания свойств вероятностных параллельных систем. Для мультиагентого случая такие логики могли бы быть расширены альтернирующей квантификацией и, таким образом, предоставить средства для представления недетерминизма двух типов: вероятностного и свойственного мультиагентным системам с частичным контролем. На данный момент предлагаемая в данной работе логика PTATL является единственной из известных автору вероятностных логик с альтернирующим временем.


    1. страница 1 страница 2 ... страница 8 страница 9


      Смотрите также:





            следующая страница >>

      скачать файл




 



 

 
 

 

 
   E-mail:
   © zaeto.ru, 2020