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

 

МИНИСТЕРСТВО ОБРАЗОВАНИЯ И  НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ

 

ГОУ САРАТОВСКИЙ  ГОСУДАРСТВЕННЫЙ  ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ

 

 

КУРСОВАЯ РАБОТА

по дисциплине:  Современные проблемы информатики и вычислительной техники

программы обучения магистра 230100 по направлению 230100 «Информатика и вычислительная техника»

Аннотированная магистерская программа  «Сети ЭВМ и телекомууникации»

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

Руководитель  курсовой работы _________________   д. с. н., профессор  Н.И. Мельникова 

Члены комиссии:

_____________________________________

_____________________________________

_____________________________________

Выполнил: __________________________ магистрант группы мИВЧТ-11 Е.С. Исекетов

 

Саратов 2010

СОДЕРЖАНИЕ

 

ВВЕДЕНИЕ 3

1. ЛОГИКА С ЛИНЕЙНЫМ ВРЕМЕНЕМ (LTL) 5

2. ЛОГИКА С ВЕТВЯЩИМСЯ ВРЕМЕНЕМ (СTL) 6

3. ЛОГИКА С АЛЬТЕРНИРУЮЩИМ ВРЕМЕНЕМ (АTL) 9

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

ЗАКЛЮЧЕНИЕ 13

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

 

ВВЕДЕНИЕ

 

Термин «логика» происходит от древнегреческого слова «логос» (logos), основные значения которого связаны с понятиями «мышление» («мысль», «мысль») и «язык», «речь» («слово»). Тогда мышление еще не осознавалось как относительно самостоятельный феномен.  
«Логос» в понимании древнегреческого мыслителя Гераклита (VI-V вв до н.э.), который первым прибег к этому термину, - это то, что упорядочивает мир, вечная объективная всеобщая прочная закономерность. Определенной степени такое значение термин «логика» сохраняет и в наше время. Бытие, по современным представлениям, являются противоречивым единством упорядоченности и хаоса. Исходя из определяющей роли первого момента, говорят о объективную логику возникновения, становления и развития тех или иных объектов, в частности о логике событий и т.д.

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

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

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

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

Темпоральная логика (англ. temporal logic) в логике — это логика, учитывающая причинно-следственные связи в условиях времени. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале. Она была разработана в 1960-х Артуром Приором на основе модальной логики и получила дальнейшее развитие в информатике благодаря трудам лауреата Тьюринговской премии Амира Пнуэли.

Темпоральные логики являются удобным формализмом для спецификации и верификации свойств параллельных и распределенных систем. В данной проблематике сформировалось два подхода: аксиоматический и алгоритмический. При первом подходе разрабатывается система аксиом, с помощью которой может быть описана как сама система, так и ее свойства. Для верификационных целей используется механический доказыватель теорем. Основу второго подхода составляют алгоритмы проверки на моделях (model checking), объединяющие в себе традиционные и логические методы анализа свойств параллельных и распределенных систем.

Автоматные  программы, в отличие от программ традиционного типа, могут быть эффективно верифицированы с помощью метода Model Checking, так как в таких программах первичными являются модели, а в традиционных – код. Однако в настоящее время не разработаны методы, позволяющие интегрировать технологии реализации автоматных программ и их верификации в современные процессы разработки объектно-ориентированного ПО. В частности, недостаточно проработаны следующие вопросы:

- механизм эффективной формализации требований к автоматным программам;

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

- синхронизация требований и реализации автоматных программ (односторонняя).

Исходя из этого, можно  утверждать, что исследования, направленные на разработку методов реализации качественных автоматных объектно-ориентированных  программ, весьма актуальны.

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

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

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

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

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

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

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

  1. ЛОГИКА С  ЛИНЕЙНЫМ ВРЕМЕНЕМ (LTL)

 

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

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

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

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

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

  • – выполнится на следующем ходу,
  • – будет выполнено всегда, начиная с текущего состояния,
  • – будет выполнено когда-нибудь в будущем или текущем состоянии,
  • – будет выполняться до тех пор, пока не будет выполнено .

Пример

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

 

 

 

 

 

 

 

 

 

 

 

 

 

  1. ЛОГИКА С  ВЕТВЯЩИМСЯ ВРЕМЕНЕМ (СTL)

 

Темпоральная логика ветвящегося времени (ветвящаяся темпоральная логика) может быть использована в интеллектуальных системах (ИС) типа интеллектуальных систем поддержки принятия решений реального времени (ИСППР РВ) [Вагин В.Н] для решения задач обучения, прогнозирования и моделирования, когда естественно рассматривать время ветвящимся в будущее. Известны различные модели ветвящегося времени, например, на основе модальной логики, где модальный оператор необходимости p может интерпретироваться как «необходимо, что всегда будет p», а оператор возможности àp – как «возможно, что будет p» [Смирнов В.А.]. Анализируются различные подходы к темпоральным высказываниям, являющимся утверждениями о будущем. При одном подходе утверждения о будущем рассматриваются аналогично утверждениям о прошлом и настоящем как констатация положения дел (ассерторические утверждения). Более соответствует реальности ситуация, когда допускается, что будущее не предопределено однозначно настоящим и возможны различные варианты развития событий, т.е. возможно ветвление в будущее. При втором (альтернативном) подходе утверждения о будущих событиях рассматриваются не как ассерторические, а как модальные утверждения. Тогда выражение «всегда будет p», «когда-нибудь будет p», «через n единиц времени будет p», корректные в случае первого подхода, не являются корректными в данном случае.

Более проста в плане сложности  реализации в ИСППР РВ пропозициональная  темпоральная логика ветвящегося времени (BPTL - Branching-Time Propositional Temporal Logic), являющейся расширением пропозициональной темпоральной логики (PTL). PTL является модальной темпоральной логикой, построенной на основе классической логики с добавленными модальными операторами для дискретного линейного времени. Используя PTL, определяется синтаксис и семантика BPTL в терминах модельной структуры M = (S,R,V), где V – функция означивания (valuation function), задающая отображение  
V: S´LP ®{T,F}, т.е. вычисляющая пропозициональное значение для каждого состояния sÎS, R – бинарное отношение, RÍS´S. Концепция ветвящегося времени требует введения условия линейности в прошлое и транзитивности R. Определена система аксиом для BPTL и доказано, что BPTL полна по отношению ко всем структурам ветвящегося времени.

В работе [Смирнов B.A] анализируются различные подходы к темпоральным высказываниям, являющимся утверждениями о будущем. При одном подходе утверждения о будущем рассматриваются аналогично утверждениям о прошлом и настоящем как констатация положения дел (ассерторические утверждения). В этом случае утверждение «когда-нибудь будет p» истинно в момент времени t, если и только если в некоторый момент t’, следующий за t, истинно p. Если будущее состояние однозначно детерминировано настоящим, то утверждения о будущем будут либо истинными, либо ложными. Однако более соответствует реальности ситуация, когда допускается, что будущее не предопределено однозначно настоящим и возможны различные варианты развития событий, т.е. возможно ветвление в будущее. При втором (альтернативном) подходе утверждения о будущих событиях рассматриваются не как ассерторические, а как модальные утверждения. В этом случае выражение типа «всегда будет p», «когда-нибудь будет p», «через n единиц времени будет p», корректные (правильно построенные) в случае первого подхода, не являются корректными.

Правильно построенными  выражения будут:

Gp - «необходимо (при любом развитии событий) всегда будет p»;

Gàp – «возможно (при некотором развитии событий) всегда будет p»;

Fp – «необходимо когда-нибудь будет p»;

Fàp – «возможно когда-нибудь будет p»;

Fnp – «через n единиц времени необходимо будет p»;

Fnàp – «через n единиц времени возможно будет p».

Для каждого приведенного оператора процесс развития событий  представляется в виде дерева, ветвящегося  в будущее (рис.1).

 

 

Рис. 1. Графическое представление  временных операторов

 

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

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

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

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

,

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

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

,

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

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

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

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

Пример

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

 

 

 

 

 

 

 

 

 

 

  1. ЛОГИКА С  АЛЬТЕРНИРУЮЩИМ ВРЕМЕНЕМ (АTL)

 

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

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

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

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

Пример

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

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

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

  1. ВЕРОЯТНОСТНЫЕ ТЕМПОРАЛЬНЫЕ ЛОГИКИ (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.