Темпоральная логика линейного времени (LTL)

Современная темпоральная логика линейного времени (LTL, Linear Time Logic) явля­ется наследницей временной логики Tense Logic Артура Прайора. LTL разработана изра­ильским ученым Амиром Пнуэли для спецификации свойств параллельных техничес­ких систем. За разработку этой логики и выделение специального класса программ, реа­гирующих на внешние события (reactive systems) в 1966 г. Амир Пнуэли был награжден премией Тьюринга.

В LTL максимально упрощены все включенные в нее концепции.

Во-первых, в LTL темпоральными операторами расширена простейшая логика выска­зываний, формулы которой строятся из конечного числа атомарных предикатов (утверж­дений) и булевых операций над ними.

Определение 2 (атомарный предикат). Атомарный предикат (атомарное утверж­дение) — это утверждение, которое может принимать истинное или ложное значение, от структуры1 которого мы абстрагируемся.

Во-вторых, в новую логику включено минимальное число темпоральных операторов, которые определяют характеристики истинности высказываний, упорядоченных во вре­мени. Таких операторов только два, U и X. Логика LTL не включает темпоральных операторов прошлого. Основания для этого очевидны: прошлое для технических систем менее важно, чем их будущее поведение, начинающееся с момента их включения, запуска.

В качестве интерпретации формул темпоральной логики рассматривается дискретная во времени бесконечная линейная направленная в будущее последовательность "миров", в каждом из которых существует своя интерпретация атомарных утверждений. Иными сло­вами, формулы LTL принимают истинное или ложное значение на последовательности миров, и в каждом из миров для всех введенных атомарных утверждений определены свои конкретные истинностные значения. Такой взгляд на изменчивость во времени значения истинности атомарных утверждений (атомарных предикатов) имел еще Аристотель, кото­рый говорил, что "утверждения и мнения" могут иметь разные значения истинности в зависимости от моментов, в которые они делаются, отражая изменения в объектах, свой­ства которых они представляют.

Направленность последовательности миров от прошлого к будущему позволяет прово­дить рассуждения об относительном времени, в терминах "до" и "после".