double arrow

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

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

Если утверждения естественного языка явно или неявно включают зависимость выска­зываний от времени или от порядка событий во времени, то формализация их в класси­ческой логике высказываний обычно неадекватна. Например, коммутативность операции конъюнкции (перестановочность ее аргументов А /\ В º В /\ А) не выполняется для следую­щих предложений:

"Джон умер, и его похоронили"

не эквивалентно предложению

"Джона похоронили, и он умер";

"Джейн вышла замуж и родила ребенка"

не эквивалентно предложению

"Джейн родила ребенка и вышла замуж";

"Сообщение послано в канал, и на него пришло подтверждение"

не эквивалентно предложению

"На сообщение пришло подтверждение, и оно послано в канал".

Анализ этих утверждений в рамках обычной логики высказываний невозможен. Для адекватного формального выражения подобных утверждений нужна логика, позволяющая отразить соотношения моментов времени наступления событий, в естественном языке определяемые такими словами, как "случилось после", "случается иногда", "случается всегда". Это требует формализации высказываний, истинность которых меняется во вре­мени.

Необходимость оперировать высказываниями, истинность которых меняется со време­нем, возникает часто. Например, высказывание: "Путин - президент России" истинно только в определенный период времени. Высказывание "Светит солнце", ложное сегод­ня, может стать истинным завтра. Утверждение "Я голоден" станет ложным после того, как я поем. Многие утверждения, в которых вводятся причинно-следственные отноше­ния, также связаны со временем:

"Если я видел ее раньше, то я узнаю ее при встрече ";

"Раз Персил - всегда Персил";

"Мы не друзья, пока ты не извинишься".

Утверждение естественного языка:

"Вчера он сказал, что придет завтра, значит, он сказал, что придет сегодня", несомненно, истинно. Но в обычной логике высказываний формальное доказательство истинности этого утверждения невозможно[1].

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

С1: Посланный запрос когда-нибудь в будущем будет обработан;

С2: Лифт никогда не пройдет мимо этажа, вызов от которого поступил, но еще не обслужен.

Элементарные (атомарные) утверждения в этих высказываниях могут быть истинны в один момент времени и ложны в другой. Мы не можем адекватно представить утвержде­ние С1 с помощью такой формулы логики высказываний:

Послан(R)” Обработан(R) (то есть если запрос R послан, то он обработан).

Действительно, в классической логике утверждения обычно понимаются как истинные либо ложные независимо от времени, а утверждение C1 явно различает разные моменты времени. Оно утверждает, что если в некоторый момент времени t запрос R послан, то в какой-то будущий момент времени t ' > t он будет обработан.

Попытаемся выразить эти свойства с помощью логики предикатов первого порядка, вводя в употребление такие выражения, как "событие р наступило в момент t". Утверж­дение С1 при этом будет выглядеть так:

Утверждение С2 в логике предикатов выглядит так (здесь ЛифтN(t)) - утверждение: Лифт в момент t находится на этаже n):

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

Попытка построения формальной модели, неявно учитывающей время в высказывани­ях, была предпринята философом и логиком Гансом Райхенбахом ([1]) для изучения глагольных времен английского языка. В теории Райхенбаха время глагола в предложении характеризуется соотношением моментов наступления событий, о которых говорится и которые подразумеваются в предложении. Используя соотношения во времени двух мо­ментов: момента S, в который сделано высказывание (Speech time), и момента Е наступле­ния события, о котором говорится в высказывании (Event time), можно образовать только три простых времени глагола - настоящее, прошедшее и будущее с соотношениями соот­ветственно E=S, E<S и S<E. Для того чтобы покрыть большое число различных глаголь­ных времен, Рейхенбах ввел третий момент - момент R точки референции (Reference time), то есть момента, на который ссылается высказывание. В Past Perfect, когда мы говорим, например, "I shall have seen John" (буквально "Я буду иметь Джона увиденным"), это высказывание отсылает нас не к тому моменту, когда я увидел Джона, но к моменту, по отношению к которому (with reference to) мое видение Джона уже произошло, то есть соотношение между этими моментами времени есть S<E<R.

Формальная модель Райхенбаха позволяет прояснить различия многих времен глаго­лов английского языка. Например, в предложении "I saw John" соотношение между этими

моментами R=E<S; а в предложении "I have seen John" это соотношение E<R=S (рис. 1).

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

В приведенных выше примерах высказываний время не присутствует явно. И нам действительно часто неважно, при каких конкретных значениях времени наступали те или иные события, важно только выразить порядок событий, отношения между момента­ми времени, в которых эти события наступали (вспомним знаменитый тезис Л. Лэмпорта: Время есть способ упорядочения событий). Характеристики временных свойств систем используют категории вида "никогда не будет верно, что...", или "в будущем обязатель­но случится, что..." и тому подобные, характеризующие истинность суждения с учетом отношений между моментами наступления различных событий во времени. Можно рас­ширить классическую логику, разрешив использовать такие категории перед утверждени­ями логики, например, выражение ¥Получено(т) можно понимать так: Когда-нибудь в будущем сообщение m обязательно будет получено. Такие категории называются модаль­ностями, их можно поместить перед высказываниями, чтобы они как-то характеризова­ли содержание этих высказываний.

Модальность в логике (от латинского modus - способ, наклонение) вводится дополни­тельным оператором, предваряющим высказывание. Модальный оператор характеризует высказывание, являющееся его операндом. В общем случае модальный оператор не обяза­тельно связан со временем. Например, пусть q - некоторое высказывание. Можно выра­зить неполную уверенность в истинности утверждения q, сказав: "Возможно, что q насту­пит". Для формализации этого введем модальный оператор М. Тогда Мq имеет смысл "возможно, что q наступит", или "может быть, наступит q".

Формальные теории устанавливают соотношения между формулами. Например, вве­дем модальный оператор L, имеющий смысл "необходимо, что...". Тогда можно следую­щим образом определить отношение между модальностями М и L: Lq ºØ MØq, что согла­суется с интуитивно истинным утверждением:

"q обязательно наступит, это то же самое, что неверно, что q, возможно, не насту­пит вовсе".

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

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

Определение 1 (темпоральные логики). Темпоральные логики - это логики, в кото­рых истинностное значение логических формул зависит от момента времени, в котором вычисляются значения этих формул.

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

В одной из предшественниц современных темпоральных логик - Tense Logic, разрабо­танной английским логиком Артуром Прайором в середине прошлого века [2], были впер­вые введены две модальности: F (от Future): "когда-нибудь в будущем будет истинно..." и P (от Past): "когда-то в прошлом было истинно...".

На рис. 2 показано, при каких значениях времени истинны утверждения Fq и Pq, если заданы отрезки времени, в которых истинно утверждение q. Обозначим t|=Ф утверждение:

"В момент времени t истинно утверждение Ф". Тогда (см. рис. 2):

- утверждение q истинно в момент времени t (t|=q), если утверждение q истинно в момент t (что является тождественной истиной, тавтологией);

- утверждение Fq истинно в момент времени t (t|=Fq), если для какого-то момента времени t' в будущем (при некотором t'>t) q станет истинным (заметьте, что будущее здесь включает настоящее);

- утверждение Рq истинно в момент времени t (t|=Pq), если для какого-то момента времени t' в прошлом (при некотором t'> t < t) утверждение q было истинным.

В Tense Logic введены и два дуальных темпоральных оператора: G (от слова Globally) и H (от слова History) с очевидными соотношениями: Gq ºØ F Ø q, Hq ºØ P Ø q. Справедли­вость этих соотношений очевидна. Например, первого: "Утверждать, что в будущем утверждение q будет всегда истинно, это то же самое, что утверждать, что неверно, что когда-нибудь в будущем утверждение q станет ложным". Эти операторы можно определить и независимо от F и P (см. рис. 2):

Рис. 2. Темпоральные операторы Tense Logic

- утверждение Gq истинно в момент времени t (t|=Gq), если для любого момента времени t' в будущем (при всех t'>t) утверждение q истинно (заметьте, что будущее здесь также включает настоящее);

- утверждение Hq истинно в момент времени t (t|=Hq), если для любого момента времени t' в прошлом утверждение q истинно.

Уже с помощью двух темпоральных операторов F и G можно выразить сложные свойства, зависящие от времени. Например:

Утверждение q будет истинным:

всегда в будущем: Gq

хотя бы раз в будущем: Fq

никогда в будущем: Ø Fq

бесконечно много раз в будущем: GFq

с какого-то момента постоянно: FGq.

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

События е1 и е2 никогда не произойдут одновременно (взаимное исключение): G[Ø(е1 /\ e2) ]

Посланное сообщение m когда-нибудь в будущем будет получено:

G[ Посланоm ” F Полученот ]

Джейн вышла замуж и родила ребенка:

Р(Джейн_выходит_замуж /\ FДжейн_рожаеm_ребенка)

Джейн родила ребенка и вышла замуж:

Р(Джейн_рожает_ребенка /\ FДжейн_выходum_замуж)

Пока ключ зажигания не вставлен, машина не поедет:

G(ØP Зажигание ” Старт).

В темпоральную логику можно ввести еще два оператора: NextTime (X) и Until (U). Оператор Next time: утверждение Xq истинно в момент времени t, если q истинно в следующий момент t + 1:

Джон убил, и ему стало страшно:

Р(Джон_убивает /\ XG Джону_страшно)

Если я видел ее раньше, я ее узнаю при встрече:

РУвидел ” G(Всmреmuл ^ ХУзнал)

Джон умер и его похоронили:

Р(Джон_умирает /\ XGДжона_хоронят)

Оператор Until (до тех пор, пока не наступит нечто) требует двух аргументов - утверждений. Формально он записывается довольно сложно:

Утверждение pUq истинно в момент времени t, если q истинно в некоторый будущий момент времени t'> t, а во всем промежутке [t, t') от момента t до t' истинно p. Пример развертки во времени, показывающей, когда будет истинно утверждение pUq при различ­ных истинностных значениях p и q, показан на рис. 3.

С оператором Until многие сложные утверждения легко представимы в формальной записи, например:

Мы не друзья, пока ты не извинишься:

(ØМы_друзья) U Ты_извиняешься

Лифт никогда не пройдет мимо этажа, вызов от которого поступил, но еще не обслужен:

G [ Вызов(n) ” (ØЛифт(n))U Обслуживается(n) ].

Через оператор U легко выражается оператор F:

Fq = true U q,

а следовательно, и оператор G:

G = ØFØq = Ø (true U Ø q).

В этой логике для операторов X и U существуют их аналоги в прошлом: X^(-1) (в предыдущий момент времени, 'вчера') и S (since, 'с тех пор, как').

Tense Logic позволяет формализовать философские мысли о времени. Например, обо­значим атомарное утверждение "нечто есть" символом q. Тогда следующее глубокомыс­ленное абсолютно истинное заключение (тавтологию):

"Будет, что нечто было, если и только если оно или есть сейчас, или будет, или уже было"

можно формализовать так:

FPq º q \/ Fq \/ Pq.

Философскую мысль о времени:

"Любое 'вчера' было когда-то 'завтра', любое 'завтра' когда-нибудь станет 'вчера'" формально можно записать так:

(PX^(-1)q ” PXq) /\ (FXq ” FX^(-1)q).

Временная логика помогает точно и однозначно выразить временные соотношения между событиями, о которых повествуют (часто неоднозначные) фразы естественного языка. Обозначим:

Д(х): х - мой друг, П(х): х - президент.

Используя эти обозначения, можно формально записать несколько совершенно раз­личных интерпретаций предложения "Мой друг NN будет президентом":

1 Д(NN) & FXП(NN):

сейчас NN — мой друг, а в будущем он станет президентом;

2 FX(Д(NN) & П(NN)):

в будущем NN станет моим другом, и в это время он уже будет президентом;

3 F(Д(NN) & FXП(NN))

в будущем NN станет моим другом, а затем он станет президентом.


Понравилась статья? Добавь ее в закладку (CTRL+D) и не забудь поделиться с друзьями:  



Сейчас читают про: