Временная логика - Temporal logic

В логике , временная логика является любая система правил и символика для представления и рассуждения о, предложения квалифицируются по времени (например, «Я всегда голоден», «Я в конце концов , быть голодным», или «Я буду голодным пока я что-нибудь не съем "). Иногда он также используется для обозначения временной логики , основанной на модальной логике системы темпоральной логики, введенной Артуром Прайором в конце 1950-х годов с важным вкладом Ханса Кампа . Его дальнейшее развитие получили компьютерные ученые , в частности Амир Пнуэли , и логики .

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

Мотивация

Рассмотрим высказывание «Я голоден». Хотя его значение постоянно во времени, истинность утверждения может меняться во времени. Иногда это правда, а иногда ложь, но никогда одновременно истина и ложь. Во временной логике утверждение может иметь значение истинности, которое изменяется во времени - в отличие от вневременной логики, которая применяется только к утверждениям, значения истинности которых постоянны во времени. Такой подход к значению истинности с течением времени отличает темпоральную логику от вычислительной глагольной логики .

Временная логика всегда имеет возможность рассуждать о временной шкале. Так называемая линейная «логика времени» ограничивается этим типом рассуждений. Однако логика ветвления может приводить к нескольким временным рамкам. Это предполагает среду, которая может действовать непредсказуемо. Чтобы продолжить пример, в логике ветвления мы можем заявить, что «есть вероятность, что я останусь голодным вечно», и что «есть вероятность, что со временем я перестану голодать». Если мы не знаем, накормят ли меня когда-нибудь, оба эти утверждения могут быть правдой.

История

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

Чарльз Сандерс Пирс отмечал в XIX веке, что тысячелетия мало развивались :

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

Как ни удивительно для Пирса , первая система темпоральной логики была построена, насколько нам известно, в первой половине 20 века. Хотя Артур Прайор широко известен как основатель темпоральной логики, первая формализация такой логики была предоставлена ​​в 1947 году польским логиком Ежи Лосем . В своей работе Podstawy Analizy Metodologicznej Kanonów Milla ( Основы методологического анализа методов Милля ) он представил формализацию канонов Милля . В Łoś . В подходе упор был сделан на фактор времени. Таким образом, для достижения своей цели он должен был создать логику, которая могла бы предоставить средства для формализации временных функций. Логику можно было рассматривать как побочный продукт главной цели Лоса , хотя это была первая позиционная логика, которая в качестве основы была использована позже для изобретений Лоса в эпистемической логике. Сама логика имеет синтаксис, сильно отличающийся от временной логики Prior, в которой используются модальные операторы. Язык логики oś скорее использует специфический для позиционной логики оператор реализации, который связывает выражение с конкретным контекстом, в котором рассматривается его истинностное значение. В работе Тоси этот рассматриваемый контекст был только временным, поэтому выражения были связаны с конкретными моментами или интервалами времени.

В последующие годы Артур Прайор начал исследования темпоральной логики . Его интересовали философские последствия свободы воли и предопределения . По словам его жены, он впервые рассмотрел вопрос о формализации темпоральной логики в 1953 году. Результаты его исследований были впервые представлены на конференции в Веллингтоне в 1954 году. Система, которую представил Прайор, синтаксически была похожа на логику Тося , хотя только в 1955 году он явно ссылался на нее. Oś ', в последнем разделе приложения 1 в Формальной логике Прайора.

Прайор читал лекции по этой теме в Оксфордском университете в 1955–1956 гг., А в 1957 г. опубликовал книгу « Время и модальность» , в которой представил пропозициональную модальную логику с двумя временными связками ( модальными операторами ), F и P, соответствующими «когда-нибудь в будущем» и «когда-нибудь в прошлом». В этой ранней работе Приор считал время линейным. Однако в 1958 году он получил письмо от Сола Крипке , в котором указывалось, что это предположение, возможно, необоснованно. В развитии, которое предвосхитило подобное в компьютерных науках, Приор принял это во внимание и разработал две теории ветвления времени, которые он назвал «Оккамистом» и «Пирсаном». Между 1958 и 1965 годами Прайор также переписывался с Чарльзом Леонардом Хамблином , и в этой переписке можно проследить ряд ранних достижений в этой области, например, последствия Гамблина . В 1967 году Прайор опубликовал свою наиболее зрелую работу по этой теме - книгу « Прошлое, настоящее и будущее» . Два года спустя он умер.

Наряду с временной логикой Прайор построил несколько систем позиционной логики , которые унаследовали основные идеи от Лось . Работу по позиционной темпоральной логике продолжил Николас Решер в 60-70-х годах. В таких работах, как « Заметка о хронологической логике» (1966 г.), « О логике хронологических суждений» (1968 г.) , «Топологическая логика» (1968 г.), « Временная логика» (1971 г.) он исследовал связи между системами Лосья и Прайора . Более того, он доказал, что временные операторы Приора могут быть определены с помощью оператора реализации в конкретной позиционной логике . Решер в своей работе также создал более общие системы позиционной логики . Хотя первые были созданы для чисто временного использования, он предложил термин топологической логики, который должен был содержать оператор реализации, но не имел конкретных временных аксиом, таких как аксиома часов.

Бинарные временные операторы Since и Again были введены Хансом Кампом в его докторскую диссертацию 1968 года. тезис, который также содержит важный результат, связывающий темпоральную логику с логикой первого порядка - результат, теперь известный как теорема Кампа .

Двумя первыми претендентами на формальные проверки были линейная временная логика , линейная временная логика Амира Пнуели и логика дерева вычислений, логика ветвящегося времени Мордехая Бен-Ари , Зохара Манна и Амира Пнуели. Практически эквивалентный CTL формализм был предложен примерно в то же время Э. М. Кларком и Э. А. Эмерсоном . Тот факт, что вторая логика может быть решена более эффективно, чем первая, не влияет на ветвление и линейную логику в целом, как это иногда утверждается. Напротив, Эмерсон и Лей показывают, что любую линейную логику можно расширить до логики ветвления, решение которой может быть решено с такой же сложностью.

Позиционная логика Лось

Логика Лоша была опубликована на польском языке в 1947 году, когда была озаглавлена ​​его магистерская диссертация. Его философские и формальные концепции можно рассматривать как продолжение Львовско-Варшавской школы логики, поскольку его руководителем был Ежи Слупецкий, ученик Яна Лукасевича. Документ не переводился на английский до 1977 года, хотя в 1951 году Хенрик Хио представил краткий, но информативный обзор в Journal of Symbolic Logic . Его обзор содержал основные концепции его работы и был достаточным для популяризации результатов Лоса среди логического сообщества. Основная цель этой работы - представить каноны Милля в рамках формальной логики. Для достижения этой цели автор исследовал важность временных функций в структуре концепции Миила. Получив это, он представил свою аксиоматическую систему логики, которая могла бы служить основой канонов Милля вместе с их временными аспектами.

Синтаксис

Язык логики, впервые опубликованный в Podstawy Analizy Metodologicznej Kanonów Milla ( Основы методологического анализа методов Милля ), состоял из:

• логические операторы первого порядка '¬', '∧', '∨', '→', '≡', '∀' и '∃'
• оператор реализации U
• функциональный символ δ
• пропозициональные переменные p ₁ , p ₂ , p ₃ , ...
• переменные, обозначающие моменты времени t ₁ , t ₂ , t ₃ , ...
• переменные, обозначающие временные интервалы n ₁ , n ₂ , n ₃ , ...

Набор терминов (обозначается S) строится следующим образом:

• переменные, обозначающие моменты времени или интервалы, являются терминами
• если и - переменная временного интервала, то${\ displaystyle \ tau \ in S}$${\ displaystyle \ epsilon}$${\ Displaystyle \ дельта (\ тау, \ эпсилон) \ в S}$

Набор формул (обозначается For) строится следующим образом:

• все формулы логики первого порядка действительны
• если и - пропозициональная переменная, то${\ displaystyle \ tau \ in S}$${\ displaystyle \ phi}$${\ Displaystyle U _ {\ tau} (\ phi) \ in For}$
• если , то${\ displaystyle \ phi \ in For}$${\ displaystyle \ neg \ phi \ in For}$
• если и , то${\ displaystyle \ phi, \ psi \ in For}$${\ Displaystyle \ circ \ in \ {\ клин, \ vee, \ rightarrow, \ эквив \}}$${\ displaystyle \ phi \ circ \ psi \ in For}$
• если и и υ - пропозициональная, моментная или интервальная переменная, то${\ displaystyle \ phi \ in For}$${\ Displaystyle Q \ в \ {\ forall, \ существует \}}$${\ displaystyle Q _ {\ upsilon} \ phi \ in For}$

Оригинальная аксиоматическая система

1. ${\ Displaystyle U_ {t_ {1}} \ neg p_ {1} \ Equiv \ neg U_ {t_ {1}} p_ {1}}$
2. ${\ displaystyle U_ {t_ {1}} (p_ {1} \ rightarrow p_ {2}) \ rightarrow (U_ {t_ {1}} p_ {1} \ rightarrow U_ {t_ {1}} p_ {2}) }$
3. ${\ displaystyle U_ {t_ {1}} ((p_ {1} \ rightarrow p_ {2}) \ rightarrow ((p_ {2} \ rightarrow p_ {3}) \ rightarrow (p_ {1} \ rightarrow p_ {3 })))}$
4. ${\ displaystyle U_ {t_ {1}} (p_ {1} \ rightarrow (\ neg p_ {1} \ rightarrow p_ {2}))}$
5. ${\ displaystyle U_ {t_ {1}} ((\ neg p_ {1} \ rightarrow p_ {1}) \ rightarrow p_ {1})}$
6. ${\ displaystyle \ forall _ {t_ {1}} U_ {t_ {1}} p_ {1} \ rightarrow p_ {1}}$
7. ${\ displaystyle \ forall _ {t_ {1}} \ forall _ {n_ {1}} \ exists _ {t_ {2}} \ forall _ {p_ {1}} (U _ {\ delta (t_ {1}, n_ {1})} p_ {1} \ Equiv U_ {t_ {2}} p_ {1})}$
8. ${\ displaystyle \ forall _ {t_ {1}} \ forall _ {n_ {1}} \ exists _ {t_ {2}} \ forall _ {p_ {1}} (U _ {\ delta (t_ {2}, n_ {1})} p_ {1} \ Equiv U_ {t_ {1}} p_ {1})}$
9. ${\ displaystyle \ forall _ {t_ {1}} \ exists _ {p_ {1}} \ forall _ {t_ {2}} (U_ {t_ {2}} p_ {1} \ Equiv \ forall _ {p_ { 2}} (U_ {t_ {1}} p_ {2} \ Equiv U_ {t_ {2}} p_ {2}))}$

Логика предшествующего времени (TL)

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

• П : «Дело было в том, что ...» (П означает «прошлое»)
• F : «Будет так, что ...» (F означает «будущее»)
• G : "Всегда будет так, что ..."
• H : "Всегда было так, что ..."

Их можно объединить, если мы позволим π быть бесконечным путем:

• ${\ displaystyle \ pi \ vDash FG \ phi}$: "В определенный момент верно на всех будущих состояниях пути"${\ displaystyle \ phi}$
• ${\ displaystyle \ pi \ vDash GF \ phi}$: " верно в бесконечно многих состояниях на пути"${\ displaystyle \ phi}$

Из P и F можно определить G и H , и наоборот:

${\ Displaystyle {\ begin {выровнено} F & \ Equiv \ lnot G \ lnot \\ P & \ Equiv \ lnot H \ lnot \ end {выровнено}}}$

Синтаксис и семантика

Минимальный синтаксис для TL определяется следующей грамматикой BNF :

${\ displaystyle \ phi, \ psi :: = a \; | \; \ bot \; | \; \ lnot \ phi \; | \; \ phi \ lor \ psi \; | \; G \ phi \; | \; H \ phi}$

где a - некоторая атомарная формула .

Модели Крипке используются для оценки истинности предложений в TL. Пара ( T , <) множества T и бинарного отношения <на T (называемая «приоритетом») называется фреймом . Модель задается тройка ( Т , <, V ) из рамы и функции V называется оценка , которая сопоставляет каждой паре ( , у ) атомарной формулы и значение времени некоторое значение истина. Понятие « ϕ истинно в модели U = ( T , <, V ) в момент u » обозначается сокращенно U ⊨ ϕ [ u ]. В этих обозначениях

Заявление	... верно только тогда, когда
U ⊨ a [ u ]	V ( a , u ) = верно
U ⊨¬ ϕ [ u ]	не U ⊨ ϕ [ u ]
U ⊨ ( ϕ ∧ ψ ) [ u ]	U ⊨ ϕ [ u ] и U ⊨ ψ [ u ]
U ⊨ ( ϕ ∨ ψ ) [ u ]	U ⊨ ϕ [ u ] или U ⊨ ψ [ u ]
U ⊨ ( ϕ → ψ ) [ u ]	U ⊨ ψ [ u ], если U ⊨ ϕ [ u ]
U ⊨G ϕ [ u ]	U ⊨ ϕ [ v ] для всех v с u < v
U ⊨H ϕ [ u ]	U ⊨ ϕ [ v ] для всех v с v < u

Для класса F фреймов предложение ϕ языка TL является

• справедливо по отношению к F, если для каждой модели U = ( T , <, V ) с ( T , <) в F и для каждого u в T , U ⊨ ϕ [ u ]
• выполнима по отношению к F , если существует модель U = ( Т , <, V ) с ( Т , <) в F таким образом, что для некоторых U в T , U ⊨ ф [ у ]
• является следствием предложения ψ относительно F, если для любой модели U = ( T , <, V ) с ( T , <) в F и для любого u в T , если U ⊨ ψ [ u ], то U ⊨ ϕ [ u ]

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

Минимальная аксиоматическая логика

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

1. , Где является тавтологией из логики первого порядка
2. G ( A → B ) → (G A → G B )
3. H ( A → B ) → (H A → H B )
4. А → ГП А
5. А → ВЧ А

со следующими правилами удержания:

1. учитывая A → B и A , выведите B ( modus ponens )
2. учитывая тавтологию A , вывести G A
3. учитывая тавтологию A , вывести H A

Можно вывести следующие правила:

1. Правило Беккера : для данного A → B выведите T A → T B, где T - время , любую последовательность, состоящую из G, H, F и P.
2. Зеркальное отображение : по теореме A выведите ее зеркальное утверждение A ^§ , которое получается заменой G на H (и, следовательно, F на P), и наоборот.
3. Двойственность : по теореме A выведите двойственное утверждение A *, которое получается заменой на, G на F и H на P.

Перевод в логику предикатов

Берджесс дает перевод Мередита из утверждений в TL в утверждения в логике первого порядка с одной свободной переменной x ₀ (представляющей настоящий момент). Этот перевод M рекурсивно определяется следующим образом:

${\ Displaystyle {\ begin {align} & M (a) && = a ^ {*} x_ {0} \\ & M (\ lnot \ phi) && = \ lnot M (\ phi) \\ & M (\ phi \ land \ psi) && = M (\ phi) \ land M (\ psi) \\ & M ({\ mathsf {G}} \ phi) && = \ forall x_ {1} (x_ {0} <x_ {1} \ стрелка вправо M (A ^ {+})) \\ & M ({\ mathsf {H}} \ phi) && = \ forall x_ {1} (x_ {1} <x_ {0} \ rightarrow M (A ^ {+ })) \ end {выровнены}}}$

где - предложение со всеми индексами переменных, увеличенными на 1, и является одноместным предикатом, определяемым с помощью . ${\ displaystyle A ^ {+}}$${\ displaystyle A}$${\ displaystyle a ^ {*}}$${\ Displaystyle х \ mapsto V (а, х)}$

Временные операторы

Временная логика имеет два типа операторов: логические операторы и модальные операторы [1] . Логические операторы - это обычные функциональные операторы истинности ( ). Модальные операторы, используемые в линейной временной логике и логике дерева вычислений, определены следующим образом. ${\ displaystyle \ neg, \ lor, \ land, \ rightarrow}$

Текстовый	Символический	Определение	Объяснение	Диаграмма
Бинарные операторы
φ U ψ	${\ Displaystyle \ phi ~ {\ mathcal {U}} ~ \ psi}$	${\ Displaystyle (B \, {\ mathcal {U}} \, C) (\ phi) = \ (\ существует я: C (\ phi _ {i}) \ land (\ forall j <i: B (\ фи _ {j})))}$	U ntil: ф имеет при токе или позиции в будущем, и φ имеет держать до этой позиции. В этой позиции φ больше не должно удерживаться.
φ R ψ	${\ Displaystyle \ phi ~ {\ mathcal {R}} ~ \ psi}$	${\ Displaystyle (В \, {\ mathcal {R}} \, C) (\ phi) = \ (\ forall i: C (\ phi _ {i}) \ lor (\ существует j <i: B (\ фи _ {j})))}$	R elease: ф - релизы ф если ψ верно вплоть до и включая первое положение , в котором φ истинно (или навсегда , если такая позиция не существует).
Унарные операторы
N φ	${\ displaystyle \ bigcirc \ phi}$	${\ Displaystyle {\ mathcal {N}} В (\ фи _ {я}) = В (\ фи _ {я + 1})}$	N ext: φ должен удерживаться в следующем состоянии. ( X используется как синоним.)
F φ	${\ displaystyle \ Diamond \ phi}$	${\ Displaystyle {\ mathcal {F}} В (\ phi) = (истина \, {\ mathcal {U}} \, B) (\ phi)}$	F uture: φ в конечном счете должен провести (где - то на последующем пути).
G φ	${\ Displaystyle \ Box \ phi}$	${\ Displaystyle {\ mathcal {G}} В (\ phi) = \ neg {\ mathcal {F}} \ neg B (\ phi)}$	G lobally: φ должен держать на весь последующий путь.
А φ	${\ displaystyle \ forall \ phi}$	${\ displaystyle ({\ mathcal {A}} B) (\ psi) = \ (\ forall \ phi: \ phi _ {0} = \ psi \ to B (\ phi))}$	A ll: φ должен удерживать все пути, начиная с текущего состояния.
E φ	${\ Displaystyle \ существует \ phi}$	${\ Displaystyle ({\ mathcal {E}} B) (\ psi) = \ (\ exists \ phi: \ phi _ {0} = \ psi \ land B (\ phi))}$	E xists: существует по крайней мере один путь , начиная с текущего состояния , где φ имеет место.

Альтернативные символы:

• оператор R иногда обозначают через V
• Оператор W является слабым до оператора: эквивалентен${\ displaystyle f \ mathbf {W} g}$${\ displaystyle f \ mathbf {U} g \ lor \ mathbf {G} f}$

Унарные операторы - это правильно сформированные формулы, если B ( φ ) правильно сформирован. Бинарные операторы - это правильно сформированные формулы, если B ( φ ) и C ( φ ) правильно сформированы.

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

Временная логика

Временная логика включает:

• Некоторые системы позиционной логики
• Интервальная временная логика (ITL)
• Линейная временная логика (LTL)
• Логика дерева вычислений (CTL)
• Временная логика сигнала (STL)
• Временная логика отметки времени (TTL)
• Язык спецификации свойств (PSL)
• CTL *, который обобщает LTL и CTL
• Логика Хеннесси-Милнера (HML)
• Модальное μ-исчисление, включающее в качестве подмножества HML и CTL *
• Метрическая временная логика (MTL)
• Временная логика метрических интервалов (MITL)
• Временная пропозициональная темпоральная логика (TPTL)
• Усеченная линейная временная логика (TLTL)
• Гипервременная логика (HyperLTL)

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

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

• Формализм HPO
• Структура Крипке
• Теория автоматов
• Грамматика Хомского
• Система перехода состояний
• Расчет продолжительности (DC)
• Гибридная логика
• Временная логика в проверке с конечным числом состояний
• Временная логика действий (ВЛА)
• Важные публикации в формальной верификации (включая использование темпоральной логики в формальной верификации )
• Рео Координационный Язык
• Модальная логика
• Материалы исследования: Архив Общества Макса Планка

Примечания

использованная литература

• Мордехай Бен-Ари, Зохар Манна, Амир Пнуели: временная логика разветвления времени . POPL 1981: 164–176
• Амир Пнуэли: временная логика программ FOCS 1977: 46–57
• Venema, Yde, 2001, «Temporal Logic», в Goble, Lou, ed., The Blackwell Guide to Philosophical Logic . Блэквелл.
• Э.А. Эмерсон и К. Лей, « Модальности для проверки модели: логика времени ветвления наносит ответный удар », в Science of Computer Programming 8, pp. 275–306, 1987.
• Э.А. Эмерсон, " Временная и модальная логика ", Справочник по теоретической информатике , глава 16, MIT Press, 1990
• Практическое введение в PSL , Синди Эйснер, Дана Фисман
• Варди, Моше Ю. (2008). «От церкви и до PSL ». В Орне Грумберг; Гельмут Вейт (ред.). 25 лет проверки моделей: история, достижения, перспективы . Springer. ISBN 978-3-540-69849-4. препринт . Исторический взгляд на то, как, казалось бы, разрозненные идеи соединились в информатике и инженерии. (Упоминание Черча в названии этой статьи - это ссылка на малоизвестную статью 1957 года, в которой Черч предложил способ проверки оборудования.)

дальнейшее чтение

• Питер Эрстрём; Пер Ф.В. Хасле (1995). Временная логика: от древних идей до искусственного интеллекта . Springer. ISBN 978-0-7923-3586-3.

внешние ссылки

• Стэнфордская энциклопедия философии : « Временная логика » - Энтони Гальтон.
• Временная логика Yde Venema, формальное описание синтаксиса и семантики, вопросы аксиоматизации. Рассмотрение также диадических темпоральных операторов Кампа (с, до)
• Заметки Яна Ходкинсона об играх по темпоральной логике , включая формальное описание темпоральной логики первого порядка
• CADP - предоставляет общие средства проверки моделей для различной временной логики.
• PAT - это мощная бесплатная программа проверки моделей, проверка LTL, симулятор и проверка уточнения для CSP и его расширений (с общей переменной, массивами, широким диапазоном справедливости).