Темпоральная логика

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

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

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

Пример

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

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

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

4. ВЕРОЯТНОСТНЫЕ ТЕМПОРАЛЬНЫЕ ЛОГИКИ (PСTL)

 

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

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

PCTL (Branching Computational Tree Logic) является наиболее распространенной вероятностной логикой. В ней универсальный квантор и квантор существования CTL заменены оценкой вероятности. Синтаксис PCTL заимствован из CTL и, кроме вероятностных конструкций, расширен временными ограничениями, которые реализуются с помощью операторов с ограничениями.

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

.

Пример

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

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

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

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

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

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

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

• Q – это конечное множество состояний,
• A – конечное множество действий,
• - начальное состояние,
• - конечное множество наблюдаемых величин,
• d – функция, сопоставляющая каждому состоянию множество доступных в нем действий,
• - функция перехода, определяющая для каждой пары из состояния и допустимого в нем действия распределение вероятностей на множестве состояний,
• - функция, сопоставляющая значение каждой наблюдаемой величине и состоянию.

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

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

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

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

ЗАКЛЮЧЕНИЕ

 

На сегодня известно более  сотни различных темпоральных логик, назначение которых, как принято считать, состоит в формализации рассуждений о времени. Но сам процесс рассуждения при этом происходит как бы вне времени: мир как бы останавливается, пока система «думает». В реальной жизни такая идеализация не всегда приемлема, особенно в системах «жесткого» реального времени. Для систем этого типа при решении задач важно уметь оценивать количество времени, имеющегося в их распоряжении «на размышления» до того момента, когда думать уже будет поздно. Для этого необходимо уметь соотносить по времени шаги и результаты проводимых рассуждений с событиями, происходящими во внешней среде. Рассуждения такого типа получили название рассуждений во времени (reasoning situated in time ).

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

- логика с линейным временем (LTL);

- логика с ветвящимся  временем (СTL);

- логика с альтернирующим  временем (АTL);

- вероятностные  темпоральные логики (PСTL).

Построены примеры  и определены разницы между вышеперечисленных темпоралных логик.

 

 

 

 

 

 

 

 

 

 

 

СПИСОК  ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ

 

1.  Поспелов Д.А. Логико-лингвистические модели в системах управления. - М.: Энегоиздат, 1981.
2. Кандрашина Е.Ю., Литвинцева Л.В., Поспелов Д.А. Представление знаний о времени и пространстве в интеллектуальных системах. / Под ред. Д.А. Поспелова. М.: Наука. Гл. ред. физ.-мат. лит., 1989.
3. Поспелов Д.А., Осипов Г.С. Введение в прикладную семиотику // Новости искусственного интеллекта. 2002, № 6.
4. Вагин В.Н., Еремеев А.П. Некоторые базовые принципы построения интеллектуальных систем поддержки принятия решений реального времени // Изв. РАН. Теория и системы управления. 2001, № 6.
5. Еремеев А.П., Троицкий В.В. Модели представления временных зависимостей в интеллектуальных системах поддержки принятия решений // Изв. РАН. Теория и системы управления, 2003, № 5.
6. Еремеев А.П., Куриленко И.Е. Реализация временных рассуждений для интеллектуальных систем поддержки принятия решений реального времени // Программные продукты и системы, 2005, № 2.
7. Смирнов В.А. Логические системы с модальными временными операторами // Материалы II Советско-финского коллоквиума по логике «Модальные и временные логики». – М.: Институт философии АН СССР, 1979.