Линейная временная логика

• Основы линейной темпоральной логики (LTL)

  • LTL — это модальная логика, которая описывает условия, связанные со временем. 
  • Она позволяет кодировать формулы о будущем и ветвлении времени. 
  • LTL является фрагментом логики первого порядка и была предложена для верификации программ в 1977 году. 

• Синтаксис и семантика

  • LTL состоит из пропозициональных переменных, логических операторов и временных модальных операторов. 
  • Существуют дополнительные логические и временные операторы для краткого описания формул. 
  • Отношение соответствия между словом и формулой определяется через последовательности истинностных оценок. 
  • Формула LTL выполнима, если существует слово, которое ее удовлетворяет. 

• Эквивалентности и нормальная форма

  • Существуют эквивалентности, которые расширяют стандартные логические операторы. 
  • Формулы LTL могут быть преобразованы в нормальную форму с отрицанием. 
  • Нормальная форма с отрицанием полезна для перевода формул в автоматы Бюхи. 

• Отношения с другими логиками и вычислительные задачи

  • LTL эквивалентна монадической логике первого порядка и языкам без звездочек. 
  • CTL и LTL являются подмножествами CTL*, но не сопоставимы. 
  • Задачи проверки модели и синтеза LTL требуют выполнения в PSPACE. 

• Приложения и рекомендации

  • Параметрическая LTL расширяет LTL переменными в модальность until. 
  • Существуют расширения и приложения LTL, включая метрическую временную логику и свойства безопасности. 
  • Ссылки на учебные материалы и презентации доступны для дальнейшего изучения.