WikiSort.ru - Не сортированное

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

В древности теории темпоральных логик изучали философы мегарской школы, в частности Диодор Крон, и стоики. Современная темпоральная логика была разработана в 1950-х Артуром Приором^[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}}}$	Until (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}}}$	Release: ${\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})}$	NeXt: ${\displaystyle \phi }$ должно быть истинным в состоянии, непосредственно следующим за данным.
F ${\displaystyle \phi }$	${\displaystyle \Diamond \phi }$	${\displaystyle {\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )}$	Future: ${\displaystyle \phi }$ должно стать истинным хотя бы в одном состоянии в будущем.
G ${\displaystyle \phi }$	${\displaystyle \Box \phi }$	${\displaystyle {\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )}$	Globally: ${\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}}}$	All: ${\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}}}$	Exists: существует хотя бы одна ветвь, на которой ${\displaystyle \phi }$ выполняется.

Приложения

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

Темпоральные логики

Известны следующие темпоральные логики:

• Интервальная темпоральная логика
• μ-исчисление
  • CTL*
    • Логика линейного времени LTL
    • Логика деревьев вычислений CTL

См. также

• TLA⁺

Примечания

Литература

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

Это заготовка статьи по математике. Вы можете помочь проекту, дополнив её.

Это заготовка статьи по информатике. Вы можете помочь проекту, дополнив её.