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

Система представления и рассуждения о времени

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

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

Мотивация

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

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

История

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

В XIX веке Чарльз Сандерс Пирс отмечал , что на протяжении тысячелетий не наблюдалось существенного развития : ^[2]

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

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

В последующие годы начались исследования временной логики Артуром Прайором . ^[4] Он был обеспокоен философскими последствиями свободной воли и предопределения . По словам его жены, он впервые задумался о формализации временной логики в 1953 году. Результаты его исследований были впервые представлены на конференции в Веллингтоне в 1954 году. ^[4] Система, представленная Прайором, была синтаксически похожа на логику Лося , хотя только в 1955 году он явно сослался на работу Лося в последнем разделе Приложения 1 к «Формальной логике» Прайора . ^[4]

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

Наряду с временной логикой Прайор построил несколько систем позиционной логики, которые унаследовали свои основные идеи от Лося . ^[6] Работу в области позиционной темпоральной логики продолжил Николас Решер в 60-х и 70-х годах. В таких работах, как Note on Chronological Logic (1966), On the Logic of Chronological Propositions (1968) , Topological Logic (1968) и Temporal Logic (1971) он исследовал связи между системами Лося и Прайора . Более того, он доказал, что временные операторы Прайора могут быть определены с помощью оператора реализации в конкретных позиционных логиках. ^[6] Решер в своей работе также создал более общие системы позиционной логики. Хотя первые из них были созданы для чисто временного использования, он предложил термин «топологическая логика» для логик, которые должны были содержать оператор реализации, но не имели конкретных временных аксиом, таких как аксиома часов.

Бинарные темпоральные операторы Since и Until были введены Гансом Кампом в его докторской диссертации 1968 года ^[7] , которая также содержит важный результат, связывающий темпоральную логику с логикой первого порядка — результат, теперь известный как теорема Кампа. ^{[8] [2] [9]}

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

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

Логика Лоса была опубликована в качестве его магистерской диссертации 1947 года Podstawy Analizy Metodologicznej Kanonów Milla ( Основы методологического анализа методов Милля ). ^[10] Его философские и формальные концепции можно рассматривать как продолжение концепций Львовско -Варшавской школы логики , поскольку его руководителем был Ежи Слупецкий , ученик Яна Лукасевича . Статья не была переведена на английский язык до 1977 года, хотя Генрик Хиж представил в 1951 году краткий, но содержательный обзор в Journal of Symbolic Logic . Этот обзор содержал основные концепции работы Лоса и был достаточен для популяризации его результатов среди логического сообщества. Главной целью этой работы было представить каноны Милля в рамках формальной логики. Для достижения этой цели автор исследовал важность временных функций в структуре концепции Милля. Имея это в виду, он предложил свою аксиоматическую систему логики, которая могла бы послужить основой для канонов Милля вместе с их временными аспектами.

Синтаксис

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

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

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

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

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

• все формулы логики первого порядка действительны
• если и является пропозициональной переменной, то ${\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 \{\wedge ,\vee ,\rightarrow ,\equiv \}}$ ${\displaystyle \phi \circ \psi \in For}$
• если и и υ — пропозициональная, моментная или интервальная переменная, то ${\displaystyle \phi \in For}$ ${\displaystyle Q\in \{\forall ,\exists \}}$ ${\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)

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

• П : «Было дело, что...» (П означает «прошлое»)
• F : «Будет так, что...» (F означает «будущее»)
• Г : «Всегда будет так, что...»
• Х : «Всегда было так, что...»

Их можно объединить, если мы допустим, что π будет бесконечным путем: ^[12]

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

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

${\displaystyle {\begin{aligned}F&\equiv \lnot G\lnot \\P&\equiv \lnot H\lnot \end{aligned}}}$

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

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

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

где a — некоторая атомарная формула . ^[13]

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

Учитывая класс F кадров, предложение ϕ языка TL является

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

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

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

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

1. A , где A — тавтология логики первого порядка
2. Г( А → Б )→( ГА → ГБ )
3. Н( А → В )→(Н А →Н В )
4. А → ГП А
5. А →HF А

со следующими правилами вычета:

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 определяется рекурсивно следующим образом: ^[16]

${\displaystyle {\begin{aligned}&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}\rightarrow M(A^{+}))\\&M({\mathsf {H}}\phi )&&=\forall x_{1}(x_{1}<x_{0}\rightarrow M(A^{+}))\end{aligned}}}$

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

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

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

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

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

Унарные операторы являются правильно сформированными формулами , когда B( φ ) является правильно сформированным. Бинарные операторы являются правильно сформированными формулами, когда B( φ ) и C( φ ) являются правильно сформированными.

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

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

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

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

Разновидностью, тесно связанной с временной, хронологической или временной логикой, являются модальные логики, основанные на «топологии», «месте» или «пространственном положении». ^{[23] [24]}

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

• Философский портал

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

Примечания

1. Варди 2008, стр. 153
2. Варди 2008, стр. 154
3. Лось, Ежи (1947). «Подставный анализ методологических канонов Миллы». Zasoby Biblioteki Głównej Umcs (на польском языке). накл. Университет Марии Кюри-Склодовской.
4. Øhrstrøm, Peter (2019). «Значение вклада ANPrior и Jerzy Łoś в раннюю историю современной темпоральной логики». Логика и философия времени: дополнительные темы из Prior, том 2. Логика и философия времени. ISBN 9788772102658.
5. Питер Эрстрём; Пер Ф. В. Хасле (1995). Временная логика: от древних идей до искусственного интеллекта . Springer. ISBN 978-0-7923-3586-3.стр. 176–178, 210
6. Решер, Николас; Гарсон, Джеймс (январь 1969). «Топологическая логика». Журнал символической логики . 33 (4): 537–548. doi :10.2307/2271360. ISSN  0022-4812. JSTOR  2271360. S2CID  2110963.
7. "Временная логика (Стэнфордская энциклопедия философии)". Plato.stanford.edu . Получено 2014-07-30 .
8. Вальтер Карниелли; Клаудио Пицци (2008). Модальности и мультимодальности. Springer. стр. 181. ISBN 978-1-4020-8589-5.
9. Серджио Тессарис; Энрико Франкони; Томас Эйтер (2009). Reasoning Web. Семантические технологии для информационных систем: 5-я международная летняя школа 2009, Бриксен-Брессаноне, Италия, 30 августа – 4 сентября 2009 г., Учебные лекции. Springer. стр. 112. ISBN 978-3-642-03753-5.
10. Ткачик, Марцин; Ярмужек, Томаш (2019). «Позиционное исчисление Ежи Лося и происхождение темпоральной логики». Логика и логическая философия . 28 (2): 259–276. дои : 10.12775/LLP.2018.013 . ISSN  2300-9802.
11. Прайор, Артур Норман (2003). Время и модальность: лекции Джона Локка за 1955–1956 годы, прочитанные в Оксфордском университете . Оксфорд: The Clarendon Press. ISBN 9780198241584. OCLC  905630146.
12. Лоуфорд, М. (2004). "Введение во временную логику" (PDF) . Факультет компьютерных наук Университета Макмастера .
13. Горанко, Валентин; Гальтон, Энтони (2015). Залта, Эдвард Н. (ред.). Стэнфордская энциклопедия философии (зима 2015 г.). Исследовательская лаборатория метафизики, Стэнфордский университет.
14. Мюллер, Томас (2011). «Временная или временная логика» (PDF) . В Хорстен, Леон (ред.). Континуум, сопутствующий философской логике . A&C Black. стр. 329.
15. Берджесс, Джон П. (2009). Философская логика . Принстон, Нью-Джерси: Princeton University Press. стр. 21. ISBN 9781400830497. OCLC  777375659.
16. Берджесс, Джон П. (2009). Философская логика . Принстон, Нью-Джерси: Princeton University Press. стр. 17. ISBN 9781400830497. OCLC  777375659.
17. "Temporal Logic". Стэнфордская энциклопедия философии . 7 февраля 2020 г. Получено 19 апреля 2022 г.
18. Малер, О.; Никович, Д. (2004). «Мониторинг временных свойств непрерывных сигналов». doi :10.1007/978-3-540-30206-3_12.
19. Мехрабиан, Мохаммадреза; Хаятиан, Мохаммад; Шривастава, Авирал; Эйдсон, Джон К.; Дерлер, Патрисия; Андраде, Хьюго А.; Ли-Бабуд, Я-Шиан; Гриффор, Эдвард; Вайс, Марк; Стэнтон, Кевин (2017). «Временная логика временных меток (TTL) для тестирования синхронизации киберфизических систем». Труды ACM по встроенным вычислительным системам . 16 (5s): 1–20. doi : 10.1145/3126510 . S2CID  3570088.
20. Койманс, Р. (1990). «Определение свойств реального времени с помощью метрической темпоральной логики», Real-Time Systems 2 (4): 255–299. doi :10.1007/BF01995674.
21. Ли, Сяо, Кристиан-Иоан Василе и Калин Белта. «Обучение с подкреплением с помощью временной логики». дои :10.1109/IROS.2017.8206234
22. Кларксон, Майкл Р.; Финкбайнер, Бернд; Колейни, Масуд; Мичински, Кристофер К.; Рабе, Маркус Н.; Санчес, Сезар (2014). «Временная логика гиперсвойств». Принципы безопасности и доверия . Конспекты лекций по информатике. Том. 8414. стр. 265–284. дои : 10.1007/978-3-642-54792-8_15. ISBN 978-3-642-54791-1. S2CID  8938993.
23. Решер, Николас (1968). «Топологическая логика». Темы философской логики . стр. 229–249. doi :10.1007/978-94-017-3546-9_13. ISBN 978-90-481-8331-9.
24. фон Райт, Георг Хенрик (1979). «Модальная логика места». Философия Николаса Решера . стр. 65–73. doi :10.1007/978-94-009-9407-2_9. ISBN 978-94-009-9409-6.

Ссылки

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

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

• Peter Øhrstrøm; Per FV Hasle (1995). Временная логика: от древних идей до искусственного интеллекта . Springer. ISBN 978-0-7923-3586-3.

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

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