Темпоральная логика ( временна́я логика ; англ. temporal logic ) — логика , в высказываниях которой учитывается временной аспект. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале.

В древности применение логики во временно́м аспекте изучали философы мегарской школы , в частности Диодор Крон , и стоики . Современная символическая темпоральная логика, впервые концептуализированная и сформулированная в 1950-е годы на основе модальной логики , наибольшее распространение и развитие получила в информатике благодаря трудам лауреата Тьюринговской премии Амира Пнуэли .

Пример

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

Темпоральные операторы

В темпоральных логиках бывает два вида операторов : логические и модальные. В качестве логических операторов обычно используются ( ${\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 (strong): ${\displaystyle \psi }$ должно выполниться в некотором состоянии в будущем (возможно, в текущем), свойство ${\displaystyle \phi }$ обязано выполняться во всех состояниях до обозначенного (не включительно).
${\displaystyle \phi }$ R ${\displaystyle \psi }$ ${\displaystyle \phi }$ V ${\displaystyle \psi }$	${\displaystyle \phi ~{\mathcal {R}}~\psi }$ ${\displaystyle \phi ~{\mathcal {V}}~\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 }$ первый раз станет истинно (или всегда, если такого момента не наступит). Иначе, ${\displaystyle \phi }$ должно хотя бы раз стать истинным, пока ${\displaystyle \psi }$ не стало истинным первый раз.
Унарные операторы
N ${\displaystyle \phi }$ X ${\displaystyle \phi }$	${\displaystyle \circ \phi }$	${\displaystyle {\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})}$	N e X t: ${\displaystyle \phi }$ должно быть истинным в состоянии, непосредственно следующим за данным.
F ${\displaystyle \phi }$	${\displaystyle \Diamond \phi }$	${\displaystyle {\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )}$	F uture: ${\displaystyle \phi }$ должно стать истинным хотя бы в одном состоянии в будущем.
G ${\displaystyle \phi }$	${\displaystyle \Box \phi }$	${\displaystyle {\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )}$	G lobally: ${\displaystyle \phi }$ должно быть истинно во всех будущих состояниях.
A ${\displaystyle \phi }$	${\displaystyle {\mathcal {A}}\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 {\mathcal {E}}\phi }$	${\displaystyle {\begin{matrix}({\mathcal {E}}B)(\psi )=\\(\exists \phi :\phi _{0}=\psi \land B(\phi ))\end{matrix}}}$	E xists: существует хотя бы одна ветвь, на которой ${\displaystyle \phi }$ выполняется.

Другие модальные операторы

• Оператор W , означающий W eak until : ${\displaystyle fWg}$ эквивалентно ${\displaystyle fUg\lor Gf}$

Тождества двойственности

Подобно правилам де Моргана существуют свойства двойственности для темпоральных операторов:

• ${\displaystyle \phi ~{\mathcal {U}}~\psi =\neg (\neg \phi ~{\mathcal {V}}~\neg \psi )}$
• ${\displaystyle \neg \Diamond \phi =\Box \neg \phi }$
• ${\displaystyle \neg {\mathcal {A}}\phi ={\mathcal {E}}\neg \phi }$

Приложения

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

Варианты

Основной универсальный вариант темпоральной логики — ( Скотт — , 1969); оно в качестве подмножества включает и , а основные используемые в информатике варианты — ( англ. ) и ( англ. ) — являются фрагментами CTL*.

Кроме того, существуют и другие варианты темпоральной логики, не сводимые к модальному μ-исчислению, например, и

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

Примечания

Литература

• Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: МЦНМО. 2002. ISBN 5-94057-054-2