Линейная темпоральная логика

В логике — линейная временная логика или временная логика линейного времени. ( LTL ) — это модальная темпоральная логика , модальности которой относятся ко времени. В LTL можно кодировать формулы о будущем путей , например, условие в конечном итоге будет истинным, условие будет истинным до тех пор, пока другой факт не станет истинным и т. д. Это фрагмент более сложного CTL* , который дополнительно допускает ветвление время и квантификаторы . LTL иногда называют пропозициональной темпоральной логикой , сокращенно PTL . С точки зрения выразительной силы линейная темпоральная логика (ЛТЛ) представляет собой фрагмент логики первого порядка .

LTL был впервые предложен для формальной проверки компьютерных программ Амиром Пнуэли в 1977 году.

Синтаксис

LTL состоит из конечного набора пропозициональных переменных AP , логических операторов ​​∨, а также временных модальных операторов X (в некоторой литературе используются O или N ) и U. ¬ и Формально множество формул LTL над AP определяется индуктивно следующим образом:

• если p ∈ AP , то p — формула LTL;
• если ψ и φ — формулы LTL, то ¬ψ, φ ∨ ψ, X ψ и φ U ψ — формулы LTL.

X читается как next x t, а U читается как until .Помимо этих фундаментальных операторов, существуют дополнительные логические и временные операторы, определенные в терминах фундаментальных операторов, чтобы лаконично записывать формулы LTL.Дополнительные логические операторы: ∧, →, ↔, true и false .Ниже приведены дополнительные временные операторы.

• G значит всегда ( g глобально)
• F значит наконец ​
• R за выпуск ​
• W для слабых, пока
• М — могучий выпуск

Семантика

Формула LTL может удовлетворяться бесконечной последовательностью истинностных оценок переменных в AP .Эти последовательности можно рассматривать как слово на пути структуры Крипке ( ω-слово в алфавите 2 ^АП ).Пусть w = a ₀ ,a ₁ ,a ₂ ,... — такое ω-слово. Пусть ш ( я ) знак равно а _я . Пусть w ^я = a _i , a _{i +1} ,..., который является суффиксом w . Формально отношение удовлетворения ⊨ между словом и формулой LTL определяется следующим образом:

• w ⊨ p, если p ∈ w (0)
• w ⊨ ¬ ψ, если w ⊭ ψ
• w ⊨ φ ∨ ψ , если w ⊨ φ или w ⊨ ψ
• w ⊨ X ψ, если w ¹ ⊨ ψ (на следующем временном шаге ψ должно быть истинным)
• w ⊨ φ U ψ, если существует i ≥ 0 такое, что w ^я ⊨ ψ и для всех 0 ⩽ k < i, w ^к ⊨ φ ( φ должно оставаться истинным до тех пор, пока ψ не станет истинным)

Мы говорим, что ω-слово w удовлетворяет формуле LTL ψ, когда w ⊨ ψ . L ω-язык ( ψ ) , определенный ψ, равен { w | w ⊨ ψ }, который представляет собой набор ω-слов, удовлетворяющих ψ .Формула ψ выполнима , если существует ω-слово w такое, что w ⊨ ψ . Формула ψ справедлива , если для каждого ω-слова w в алфавите 2 ^АП , мы имеем w ⊨ ψ .

Дополнительные логические операторы определяются следующим образом:

• φ ∧ ψ ≡ ¬(¬ φ ∨ ¬ ψ )
• φ → ψ ≡ ¬ φ ∨ ψ
• φ ↔ ψ ≡ ( φ → ψ ) ∧ ( ψ → φ )
• true ≡ p ∨ ¬ p , где p ∈ AP
• ложь ≡ ¬ правда

Дополнительные временные операторы R , F и G определяются следующим образом:

• ψ R φ ≡ ¬(¬ ψ U ¬ φ ) ( φ остается истинным до тех пор, пока ψ не станет истинным включительно. Если ψ никогда не станет истинным, φ должно оставаться истинным навсегда. ψ r освобождает φ .)
• F ψ ≡ true U ψ (в конечном итоге ψ становится истиной)
• G ψ ≡ false R ψ ≡ ¬ F ¬ ψ ( ψ всегда остается истинным)

Слабый до и сильный выпуск

Некоторые авторы также определяют слабый бинарный оператор «до тех пор», обозначаемый W , с семантикой, аналогичной семантике оператора «до тех пор», но условие остановки не требуется (аналогично освобождению). Иногда это полезно, поскольку и U , и R можно определить в терминах слабых до тех пор, пока:

• ψ W φ ≡ ( ψ U φ ) ∨ г ψ ≡ ψ U ( φ ∨ г ψ ) ≡ φ R ( φ ∨ ψ )
• ψ U φ ≡ F φ ∧ ( ψ W φ )
• ψ р φ ≡ φ W ( φ ∧ ψ )

Бинарный оператор сильного освобождения , обозначаемый M , является двойственным оператору слабого до тех пор, пока. Он определяется аналогично оператору до тех пор, пока условие освобождения не должно выполняться в какой-то момент. Следовательно, он сильнее, чем оператор Release.

• ψ M φ ≡ ¬(¬ ψ W ¬ φ ) ≡ ( ψ р φ ) ∧ F ψ ≡ ψ R ( φ ∧ F ψ ) ≡ φ U ( ψ ∧ φ )

Семантика темпоральных операторов графически представлена ​​следующим образом.

Текстовый	Символический	Объяснение	Диаграмма
Унарные операторы :
Х ж	$\bigcirc \varphi$	ne X t: φ должна выполняться в следующем состоянии.
F φ	$\Diamond \varphi$	Наконец : φ в конечном итоге должна выполняться (где-то на следующем пути).
г ж	$\Box \varphi$	G глобально: φ должна соблюдаться на всем последующем пути.
Бинарные операторы :
ψ U f	$\psi \;{\mathcal {U}}\,\varphi$	До тех пор, пока: ψ должно выполняться по крайней мере до тех пор, пока φ не станет истинным, что должно выполняться в текущей или будущей позиции.
ψ р ж	$\psi \;{\mathcal {R}}\,\varphi$	Освобождение : φ должно быть истинным до тех пор, пока ψ впервые не станет истинным; если ψ никогда не станет истинным, φ должно оставаться истинным навсегда.
ψ Вт f	$\psi \;{\mathcal {W}}\,\varphi$	Слабость до: ψ должна выполняться по крайней мере до φ ; если φ никогда не станет истинным, ψ должно оставаться истинным навсегда.
ψ М ж	$\psi \;{\mathcal {M}}\,\varphi$	Сильное освобождение: φ впервые не станет истинным, включая точку, должно быть истинным до тех пор, пока ψ которая должна сохраняться в текущей или будущей позиции.

Эквиваленты

Пусть φ, ψ и ρ — формулы LTL. В следующих таблицах перечислены некоторые полезные эквиваленты, расширяющие стандартные эквивалентности обычных логических операторов.

Дистрибутивность
Икс (φ ∨ ψ) ≡ ( X φ) ∨ ( X ψ)	Икс (φ ∧ ψ) ≡ ( X φ) ∧ ( X ψ)	Икс (φ U ψ)≡ ( X φ) U ( X ψ)
F (φ ∨ ψ) ≡ ( F φ) ∨ ( F ψ)	G (φ ∧ ψ) ≡ ( G φ) ∧ ( G ψ)
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ)	(φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ)

Распространение отрицания
X самодвойственный	F и G двойственны	U и R двойственны	W и M двойственны
¬ X φ ≡ X ¬φ	¬ F φ ≡ G ¬φ	¬ (φ U ψ) ≡ (¬φ R ¬ψ)	¬ (φ W ψ) ≡ (¬φ M ¬ψ)
	¬ G φ ≡ F ¬φ	¬ (φ R ψ) ≡ (¬φ U ¬ψ)	¬ (φ M ψ) ≡ (¬φ W ¬ψ)

Особые временные свойства
F φ ≡ F F φ	г φ ≡ г г φ	φ U ψ ≡ φ U (φ U ψ)
φ U ψ ≡ ψ ∨ ( φ ∧ Икс (φ U ψ) )	φ W ψ ≡ ψ ∨ ( φ ∧ Икс (φ W ψ) )	φ р ψ ≡ ψ ∧ (φ ∨ X (φ R ψ))
г φ ≡ φ ∧ Икс ( г φ)	F φ ≡ φ ∨ X ( F φ)

Нормальная форма отрицания

Все формулы LTL можно преобразовать к нормальной форме отрицания , где

• все отрицания появляются только перед атомарными предложениями,
• могут появляться только другие логические операторы true , false , ∧ и ∨, и
• только временные операторы X , U и R. могут появиться

Используя приведенные выше эквивалентности для распространения отрицания, можно вывести нормальную форму. Эта нормальная форма позволяет R , true , false и ∧ появляться в формуле, которые не являются фундаментальными операторами LTL. Обратите внимание, что преобразование к нормальной форме отрицания не увеличивает длину формулы. Эта нормальная форма полезна при переводе формулы LTL в автомат Бюхи .

Отношения с другими логиками

Можно показать, что LTL эквивалентен монадической логике первого порядка порядка FO[<] — результат, известный как теорема Кампа — или, что эквивалентно, языкам без звезд .

Логика дерева вычислений (CTL) и линейная временная логика (LTL) являются подмножеством CTL* , но они несопоставимы. Например,

• Никакая формула в CTL не может определить язык, который определяется формулой LTL F ( G p).
• Никакая формула в LTL не может определять язык, который определяется формулами CTL AG ( p → ( EX q ∧ EX ¬q) ) или AG ( EF (p)).

Вычислительные задачи

Проверка модели и ее выполнимость по формуле LTL являются задачами , полными для PSPACE . Синтез LTL и проблема проверки игр на соответствие условиям выигрыша LTL завершаются за 2EXPTIME .

Приложения

Проверка теоретико-автоматной модели линейной темпоральной логики

Важный способ проверки модели — выразить желаемые свойства (например, описанные выше) с помощью операторов LTL и фактически проверить, удовлетворяет ли модель этому свойству. Один из методов состоит в том, чтобы получить автомат Бюхи , который эквивалентен модели (принимает ω-слово именно в том случае, если оно является моделью), и другой, который эквивалентен отрицанию свойства (принимает ω-слово в точности, если оно удовлетворяет отрицанию свойство) (ср. Линейная темпоральная логика автомата Бюхи ). Пересечение двух недетерминированных автоматов Бюхи пусто тогда и только тогда, когда модель удовлетворяет этому свойству.

Выражение важных свойств при формальной проверке

Существует два основных типа свойств, которые можно выразить с помощью линейной темпоральной логики: свойства безопасности обычно утверждают, что что-то плохое никогда не случается ( G ¬ φ ), тогда как свойства живучести утверждают, что что-то хорошее продолжает происходить ( GF ψ или G ( φ → F ψ )). В более общем смысле, свойства безопасности — это те, для которых каждый контрпример имеет конечный префикс, так что, хотя он и расширяется до бесконечного пути, он все равно остается контрпримером. С другой стороны, для свойств живучести каждый конечный путь может быть расширен до бесконечного пути, удовлетворяющего формуле.

Язык спецификации

Одним из применений линейной временной логики является спецификация предпочтений на языке определения области планирования с целью планирования на основе предпочтений .

Расширения

Параметрическая линейная темпоральная логика расширяет LTL переменными до модальности.

См. также

• Язык действий
• Метрическая темпоральная логика
• Свойства безопасности и живучести

Внешние ссылки

• Презентация LTL
• Временная логика линейного времени и автоматы Бюхи
• Слайды преподавания LTL профессора Алессандро Артале в Свободном университете Боцен-Больцано
• Алгоритмы перевода LTL в Buchi, генеалогия, с сайта Spot , библиотека для проверки моделей.