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

 

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

 

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

 

 

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

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

программы обучения магистра 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 означает, что если некто болен, то он обязательно выздоровеет.

 

 

 

 

 

 

 

 

 

 

 

 

 

2. ЛОГИКА С  ВЕТВЯЩИМСЯ ВРЕМЕНЕМ (С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´L_P ®{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 означает, что если некто болен, то он всегда имеет шанс выздороветь.

 

 

 

 

 

 

 

 

 

 

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

 

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