Интернет магазин китайских планшетных компьютеров

Компьютеры - Темпоральная логика - Приложения

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

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

Известны следующие темпоральные логики:

• Интервальная темпоральная логика
• μ-исчисление
  • CTL*
    • Логика линейного времени LTL
    • Логика деревьев вычислений CTL