WikiDer > Временная пропозициональная темпоральная логика

Timed propositional temporal logic

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

Синтаксис

В будущий фрагмент TPTL определяется аналогично линейная темпоральная логика, в котором, кроме того, Часы переменные можно вводить и сравнивать с константами. Формально с учетом набора часов MTL состоит из:

Кроме того, для интервал, считается аббревиатурой для ; и то же самое для всех других видов интервалов.

Логика TPTL + Прошлое[1] построен как будущий фрагмент TLS а также содержит

  • темпоральный модальный оператор S.

Обратите внимание, что следующий оператор N не считается частью синтаксиса MTL. Вместо этого он будет определяться другими операторами.

А закрытая формула - формула над пустым набором часов.[2]

Модель

Позволять он интуитивно представляет собой набор времени. Позволять функция, которая ассоциируется с каждым моментом набор предложений от AP. Модель формулы TPTL - это такая функция . Обычно, является либо синхронизированное слово или сигнал. В таких случаях либо дискретное подмножество, либо интервал, содержащий 0.

Семантический

Позволять и как указано выше. Позволять набор часы. Позволять оценка часов закончилась .

Теперь мы собираемся объяснить, что означает, что формула TPTL держится на время для оценки . Это обозначается .Позволять и две формулы над набором часов , формула по набору часов , , , число и оператор сравнения, такой как <, ≤, =, ≥ или>: сначала рассмотрим формулы, главный оператор которых также принадлежит LTL:

  • имеет место, если ,
  • имеет место, если либо или же
  • имеет место, если либо или же
  • выполняется, если существует такой, что и такой, что для каждого , ,
  • выполняется, если существует такой, что и такой, что для каждого , ,
  • имеет место, если держит,
  • имеет место, если .

Метрическая темпоральная логика

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

TPTL не менее выразителен, чем MTL. Действительно, формула MTL эквивалентно формуле TPTL куда это новая переменная.[2]

Отсюда следует, что любой другой оператор, представленный на странице MTL, Такие как и также могут быть определены как формулы TPTL.

TPTL строго более выразителен, чем MTL[1]:2 как синхронизированные слова, так и сигналы. Для слов, рассчитанных по времени, никакая формула MTL не эквивалентна . По сигналу нет формулы MTL, эквивалентной , в котором говорится, что последнее атомарное предложение перед моментом времени 1 является .

Сравнение с LTL

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

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

  1. ^ а б Буйе, Патрисия; Шевалье, Фабрис; Марки, Николас (2005). «О выразительности TPTL и MTL». материалы 25-й конференции по основам программных технологий и теоретической информатики: 436. Дои:10.1007/11590156_3.
  2. ^ а б Алур, Раджив; Хенцингер, Томас А. (январь 1994 г.). «Действительно временная логика». Журнал ACM. 41 (1): 181–203. Дои:10.1145/174644.174651.