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

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

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

Пример

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

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

В темпоральных логиках бывает два вида операторов: логические и модальные. В качестве логических операторов обычно используются ( ¬ , ∨ , ∧ , → {displaystyle eg ,lor ,land , ightarrow } ). Модальные операторы, используемые в логике линейного времени и логике деревьев вычислений, определяются следующим образом.

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

• Оператор W, означающий Weak until: f W g {displaystyle fWg} эквивалентно f U g ∨ G f {displaystyle fUglor Gf}

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

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

• ϕ   U   ψ = ¬ ( ¬ ϕ   V   ¬ ψ ) {displaystyle phi ~{mathcal {U}}~psi = eg ( eg phi ~{mathcal {V}}~ eg psi )}
• ¬ ◊ ϕ = ◻ ¬ ϕ {displaystyle eg Diamond phi =Box eg phi }
• ¬ A ϕ = E ¬ ϕ {displaystyle eg {mathcal {A}}phi ={mathcal {E}} eg phi }

Приложения

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

Варианты

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

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

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