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

Модальная темпоральная логика с модальностями, относящимися ко времени

В логике линейная темпоральная логика или темпоральная логика линейного времени ^{[1] [2]} ( LTL ) представляет собой модальную темпоральную логику с модальностями, относящимися ко времени. В LTL можно кодировать формулы о будущем путей , например, условие в конечном итоге будет истинным, условие будет истинным до тех пор, пока другой факт не станет истинным и т. д. Это фрагмент более сложного CTL* , который дополнительно допускает ветвление время и квантификаторы . LTL иногда называют пропозициональной темпоральной логикой , сокращенно PTL . ^[3] С точки зрения выразительной силы , линейная темпоральная логика (ЛТЛ) представляет собой фрагмент логики первого порядка . ^{[4] [5]}

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

Синтаксис

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

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

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

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

Семантика

Формула LTL может удовлетворяться бесконечной последовательностью истинностных оценок переменных в AP . Эти последовательности можно рассматривать как слово на пути структуры Крипке ( ω-слово в алфавите 2 ^AP ). Пусть 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 ¹ ⊨ ψ (на следующем временном шаге x t ψ должно быть истинным)
• w ⊨ φ U ψ , если существует i ≥ 0 такое, что w ⁱ ⊨ ψ и для всех 0 ⩽ k < i, wk ^⊨ φ ( φ должно оставаться истинным до тех пор , пока ψ не станет истинным)

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

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

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

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

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

Слабое до и сильное освобождение

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

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

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

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

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

Эквиваленты

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

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

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

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

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

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

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

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

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

Вычислительные проблемы

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

Приложения

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

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

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

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

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

Одним из применений линейной темпоральной логики является спецификация предпочтений на языке определения области планирования с целью планирования на основе предпочтений . ^{[ нужна цитата ]}

Расширения

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

Смотрите также

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

Рекомендации

1. Логика в информатике: моделирование и рассуждения о системах: стр. 175.
2. «Темпоральная логика линейного времени». Архивировано из оригинала 30 апреля 2017 г. Проверено 19 марта 2012 г.
3. Дов М. Габбай ; А. Куруц; Ф. Уолтер; М. Захарьящев (2003). Многомерные модальные логики: теория и приложения. Эльзевир. п. 46. ​​ИСБН 978-0-444-50826-3.
4. Дикерт, Волкер. «Определяемые языки первого порядка» (PDF) . Университет Штутгарта.
5. Камп, Ганс (1968). Напряженная логика и теория линейного порядка (доктор философии). Калифорнийский университет Лос-Анджелеса.
6. Амир Пнуэли , Временная логика программ. Труды 18-го ежегодного симпозиума по основам информатики (FOCS) , 1977, 46–57. дои : 10.1109/SFCS.1977.32
7. Раздел. 5.1 Кристель Байер и Йост-Питер Катоен , Принципы проверки моделей , MIT Press «Принципы проверки моделей - MIT Press». Архивировано из оригинала 4 декабря 2010 г. Проверено 17 мая 2011 г.
8. Раздел. 5.1.5 «Слабые условия до», «Выпуск» и «Положительная нормальная форма» принципов проверки моделей.
9. Абрамский, Самсон ; Гавуа, Сирил; Киршнер, Клод; Спиракис, Пол (30 июня 2010 г.). Автоматы, языки и программирование: 37-й международный коллоквиум, ICALP… — Google Книги. ISBN 9783642141614. Проверено 30 июля 2014 г.
10. Моше Ю. Варди (2008). «От церкви и до PSL ». В Орне Грумберг ; Хельмут Вейт (ред.). 25 лет проверки моделей: история, достижения, перспективы . Спрингер. ISBN 978-3-540-69849-4.препринт
11. А. Пнуэли и Р. Рознер. «О синтезе реактивного модуля» В материалах 16-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования (POPL '89). Ассоциация вычислительной техники, Нью-Йорк, штат Нью-Йорк, США, 179–190. https://doi.org/10.1145/75277.75293
12. Моше Ю. Варди. Автоматно-теоретико-подход к линейной временной логике. Материалы 8-го семинара высшего порядка в Банфе (Banff'94). Конспекты лекций по информатике , вып. 1043, стр. 238–266, Springer-Verlag, 1996. ISBN 3-540-60915-6 . 
13. Боуэн Альперн, Фред Б. Шнайдер , Определение живости , Письма об обработке информации , Том 21, Выпуск 4, 1985, страницы 181–185, ISSN 0020–0190, https://doi.org/10.1016/0020-0190 (85) 90056-0
14. Чакраборти, Суймодип; Катоен, Йост-Питер (2014). Диас, Хосеп; Ланезе, Иван; Санджорджи, Давиде (ред.). «Параметрическая LTL на цепях Маркова». Теоретическая информатика . Конспекты лекций по информатике. Шпрингер Берлин Гейдельберг. 7908 : 207–221. arXiv : 1406.6683 . Бибкод : 2014arXiv1406.6683C. дои : 10.1007/978-3-662-44602-7_17. ISBN 978-3-662-44602-7. S2CID  12538495.

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

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