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

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

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

Мотивация [ править ]

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

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

История [ править ]

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

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

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

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

Бинарные временные операторы Since и Again были введены Хансом Кампом в его докторскую диссертацию 1968 года. тезис, ^[4], который также содержит важный результат, связывающий темпоральную логику с логикой первого порядка - результат, теперь известный как теорема Кампа . ^{[5] [2] [6]}

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

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

Сентенциальная напряжены логика введены в время и модальности имеет четыре (не- правды-функциональных ) модальные оператор (в дополнении ко всем обычным истинность-функциональные операторам в пропозициональной логике первого порядка . ^[7]

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

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

• ${\ 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 {align}}}$

Синтаксис и семантика [ править ]

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

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

где а - некоторая атомарная формула . ^[9]

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

Для класса фреймов 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 ]

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

Минимальная аксиоматическая логика [ править ]

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

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

${\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)}$

Временные операторы [ править ]

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

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

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

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

Унарные операторы - это правильно сформированные формулы, если B ( ) правильно сформирован. Бинарные операторы - это правильно сформированные формулы, если B ( ) и C ( ) правильно сформированы.${\displaystyle \phi }$${\displaystyle \phi }$${\displaystyle \phi }$

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

Темпоральная логика [ править ]

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

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

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

См. Также [ править ]

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

Примечания [ править ]

Ссылки [ править ]

• Мордехай Бен-Ари, Зохар Манна, Амир Пнуели: временная логика разветвления времени . 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.

Внешние ссылки [ править ]

Викискладе есть медиафайлы по теме временной логики .

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