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

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

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

Мотивация

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

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

История

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

На протяжении тысячелетий развития не было, как отмечал в 19 веке Чарльз Сандерс Пирс : ^[2]

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

К удивлению Пирса , первая система темпоральной логики была построена, насколько нам известно, в первой половине 20 века. Хотя Артур Прайор широко известен как основатель темпоральной логики, первая формализация такой логики была предоставлена ​​в 1947 году польским логиком Ежи Лось . ^[3] В своей работе « Основы методологического анализа методов Милля » он представил формализацию канонов Милля . В подходе Лось акцент был сделан на факторе времени. Таким образом, чтобы достичь своей цели, ему пришлось создать логику, которая могла бы предоставить средства формализации временных функций. Логику можно рассматривать как побочный продукт главной цели Лося , ^[4] хотя это была первая позиционная логика, которая в качестве основы позже использовалась для изобретений Лося в эпистемической логике . Сама логика имеет синтаксис, сильно отличающийся от временной логики Прайора, в которой используются модальные операторы. Язык логики Лось скорее использует оператор реализации, специфичный для позиционной логики, который связывает выражение с конкретным контекстом, в котором рассматривается его истинностное значение. В творчестве Лося этот рассматриваемый контекст был лишь временным, поэтому выражения были связаны с конкретными моментами или интервалами времени.

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

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

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

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

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

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

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

Синтаксис

Язык логики, впервые опубликованный в 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 означает «будущее»).
• Г : «Так будет всегда…»
• Х : «Так всегда было…»

Их можно объединить, если мы позволим π быть бесконечным путем: ^[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 ⊨ φ [ ты ]

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

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

Бёрджесс обрисовывает логику, которая не делает никаких предположений относительно отношения <, но допускает значимые выводы, основанную на следующей схеме аксиом: ^[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}}}$

где — предложение , в котором все индексы переменных увеличены на 1, и является одноместным предикатом, определяемым . ${\displaystyle A^{+}}$ ${\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]}

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

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

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

Примечания

1. Варди 2008, с. 153
2. Варди 2008, с. 154
3. Лось, Ежи (1920-1998); Лось, Ежи (1920–1998) (1947). «Подставный анализ методологических канонов Миллы». Zasoby Biblioteki Głównej Umcs . накл. Университет Марии Кюри-Склодовской.{{cite journal}}: CS1 maint: numeric names: authors list (link)
4. Орстрем, Питер (2019). «Значение вклада А. Н. Приора и Ежи Лося в раннюю историю современной темпоральной логики». Логика и философия времени: дальнейшие темы из предыдущего, том 2 . Логика и философия времени. ISBN 9788772102658.
5. Питер Орстрем; Согласно Ф.В. Хасле (1995). Временная логика: от древних идей к искусственному интеллекту . Спрингер. ISBN 978-0-7923-3586-3.стр. 176–178, 210.
6. Решер, Николас; Гарсон, Джеймс (январь 1969 г.). «Топологическая логика». Журнал символической логики . 33 (4): 537–548. дои : 10.2307/2271360. ISSN  0022-4812. JSTOR  2271360. S2CID  2110963.
7. "Временная логика (Стэнфордская энциклопедия философии)" . Plato.stanford.edu . Проверено 30 июля 2014 г.
8. Уолтер Карниелли; Клаудио Пицци (2008). Модальности и мультимодальности. Спрингер. п. 181. ИСБН 978-1-4020-8589-5.
9. Серджио Тессарис; Энрико Франкони; Томас Эйтер (2009). Сеть рассуждений. Семантические технологии для информационных систем: 5-я Международная летняя школа 2009 г., Бриксен-Брессанон, Италия, 30 августа – 4 сентября 2009 г., учебные лекции. Спрингер. п. 112. ИСБН 978-3-642-03753-5.
10. Ткачик, Марцин; Ярмужек, Томаш (2019). «Позиционное исчисление Ежи Лося и происхождение темпоральной логики». Логика и логическая философия . 28 (2): 259–276. дои : 10.12775/LLP.2018.013 . ISSN  2300-9802.
11. Прайор, Артур Норман (2003). Время и модальность: лекции Джона Локка за 1955–1956 годы, прочитанные в Оксфордском университете . Оксфорд: Кларендон Пресс. ISBN 9780198241584. ОСЛК  905630146.
12. Лоуфорд, М. (2004). «Введение в темпоральную логику» (PDF) . Кафедра компьютерных наук Университета Макмастера .
13. Горанко, Валентин; Гальтон, Энтони (2015). Залта, Эдвард Н. (ред.). Стэнфордская энциклопедия философии (изд. Зима 2015 г.). Лаборатория метафизических исследований Стэнфордского университета.
14. Мюллер, Томас (2011). «Временная или временная логика» (PDF) . В Хорстене, Леон (ред.). Континуум-компаньон философской логики . А&С Черный. п. 329.
15. Берджесс, Джон П. (2009). Философская логика . Принстон, Нью-Джерси: Издательство Принстонского университета. п. 21. ISBN 9781400830497. OCLC  777375659.
16. Берджесс, Джон П. (2009). Философская логика . Принстон, Нью-Джерси: Издательство Принстонского университета. п. 17. ISBN 9781400830497. OCLC  777375659.
17. «Временная логика». Стэнфордская энциклопедия философии . 7 февраля 2020 г. . Проверено 19 апреля 2022 г.
18. Малер, О.; Никович, Д. (2004). «Мониторинг временных свойств непрерывных сигналов». дои : 10.1007/978-3-540-30206-3_12.
19. Мехрабиан, Мохаммадреза; Хаятян, Мохаммед; Шривастава, Авирал; Эйдсон, Джон К.; Дерлер, Патрисия; Андраде, Хьюго А.; Ли-Бабуд, Я-Шиан; Гриффор, Эдвард; Вайс, Марк; Стэнтон, Кевин (2017). «Темпоральная логика временных меток (TTL) для проверки синхронизации киберфизических систем». Транзакции ACM во встроенных вычислительных системах . 16 (5с): 1–20. дои : 10.1145/3126510 . S2CID  3570088.
20. Койманс, Р. (1990). «Определение свойств реального времени с помощью метрической темпоральной логики», Real-Time Systems 2 (4): 255–299. дои : 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. дои : 10.1007/978-94-017-3546-9_13. ISBN 978-90-481-8331-9.
24. фон Райт, Георг Хенрик (1979). «Модальная логика места». Философия Николаса Решера . стр. 65–73. дои : 10.1007/978-94-009-9407-2_9. ISBN 978-94-009-9409-6.

Рекомендации

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

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

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

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

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