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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

Темпоральная логика (англ. temporal logic) в логике — это логика, учитывающая причинно-следственные связи в условиях времени. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале. Она была разработана в 1960-х Артуром Приором на основе модальной логики и получила дальнейшее развитие в информатике благодаря трудам лауреата Тьюринговской премии Амира Пнуэли.

Есть два подхода темпоральной логики, основанные на принципах здравого смысла и диалектики: «после этого» означает «по причине этого», либо «после этого» означает «позже» в хронологическом смысле.

Пример[править | править вики-текст]

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

Темпоральные операторы[править | править вики-текст]

В темпоральных логиках бывает два вида операторов: логические и модальные. В качестве логических операторов обычно используются (\neg,\or,\and,\rightarrow). Модальные операторы, используемые в логике линейного времени и логике деревьев вычислений, определяются следующим образом.

Текстовое обозначение Символьное обозначение Определение Описание Диаграмма
Бинарные операторы
\phi U \psi \phi ~\mathcal{U}~ \psi \begin{matrix}(B\,\mathcal{U}\,C)(\phi)= \\ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)))\end{matrix} Until (strong): \psi должно выполниться в некотором состоянии в будущем (возможно, в текущем), свойство \phi обязано выполняться во всех состояниях до обозначенного (не включительно).
\phi R \psi

\phi V \psi

\phi ~\mathcal{R}~ \psi

\phi ~\mathcal{V}~ \psi

\begin{matrix}(B\,\mathcal{R}\,C)(\phi)= \\ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)))\end{matrix} Release: \phi освобождает \psi, если \psi истинно, пока не наступит момент, когда \phi первый раз станет истинно (или всегда, если такого момента не наступит). Иначе, \phi должно хотя бы раз стать истинным, пока \psi не стало истинным первый раз.
Унарные операторы
N \phi

X \phi

\circ \phi \mathcal{N}B(\phi_i)=B(\phi_{i+1}) NeXt: \phi должно быть истинным в состоянии, непосредственно следующим за данным.
F \phi \Diamond \phi \mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi) Future: \phi должно стать истинным хотя бы в одном состоянии в будущем.
G \phi \Box \phi \mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi) Globally: \phi должно быть истинно во всех будущих состояниях.
A \phi  \mathcal{A} \phi \begin{matrix}(\mathcal{A}B)(\psi)= \\ (\forall \phi:\phi_0=\psi\to B(\phi))\end{matrix} All: \phi должно выполняться на всех ветвях, начинающихся с данной.
E \phi  \mathcal{E} \phi \begin{matrix}(\mathcal{E}B)(\psi)= \\ (\exists \phi:\phi_0=\psi\land B(\phi))\end{matrix} Exists: существует хотя бы одна ветвь, на которой \phi выполняется.

Другие модальные операторы[править | править вики-текст]

  • Оператор W, означающий Weak until: f W g эквивалентно f U g \or G f

Тождества двойственности[править | править вики-текст]

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

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

Приложения[править | править вики-текст]

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

Темпоральные логики[править | править вики-текст]

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

Литература[править | править вики-текст]

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