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

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

Синтаксис

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

конечное множество пропозициональных переменных AP ,
логические операторы ¬ и ∨, и
временной U оператор модальный ,
сравнение часов $x\sim c$ , с $x\in X$ , $c$ число и $\sim$ оператор сравнения, например <, ≤, =, ≥ или >.
оператор количественного определения замораживания $x.\phi$ , для $\phi$ формула TPTL с набором часов $X\cup \{x\}$ .

Кроме того, для $I=(a,b)$ интервал, $x\in I$ рассматривается как сокращение от $x>a\land x<b$ ; и аналогично для всех остальных интервалов.

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

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

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

— Закрытая формула это формула для пустого набора часов. ^[2]

Модели

Позволять $T\subseteq \mathbb {R} _{+}$ , который интуитивно представляет собой набор времен. Позволять $\gamma :T\to {\mathcal {P}}(AP)$ функция, которая связывается с каждым моментом $t\in T$ набор предложений от AP . Моделью формулы TPTL является такая функция $\gamma$ . Обычно, $\gamma$ это либо синхронизированное слово , либо сигнал . В таких случаях $T$ является либо дискретным подмножеством, либо интервалом, содержащим 0.

Семантика

Позволять $T$ и $\gamma$ быть как указано выше. Позволять $X$ быть набором часов . Позволять $\nu :X\to \mathbb {R} _{\geq 0}$ ( часовая оценка более $X$ ).

Теперь мы объясним, что это означает для формулы TPTL. $\phi$ держать во время $t$ для оценки $\nu$ . Это обозначается $\gamma ,t,\nu \models \phi$ .Позволять $\phi$ и $\psi$ две формулы для набора часов $X$ , $\xi$ формула для набора часов $X\cup \{y\}$ , $x\in X$ , $l\in {\mathtt {AP}}$ , $c$ число и $\sim$ являющийся оператором сравнения, например <, ≤, =, ≥ или >:Сначала рассмотрим формулы, главный оператор которых также принадлежит LTL:

$\gamma ,t,\nu \models l$ имеет место, если $l\in \gamma (t)$ ,
$\gamma ,t,\nu \models \neg \phi$ имеет место, если $\gamma ,t,\nu \not \models \phi$
$\gamma ,t,\nu \models \phi \lor \psi$ имеет место, если либо $\gamma ,t,\nu \models \phi$ или $\gamma ,t,\nu \models \psi$
$\gamma ,t,\nu \models \phi \mathbin {\mathcal {U}} \psi$ имеет место, если существует $t<t''$ такой, что $\gamma ,t'',\nu \models \psi$ и такой, что для каждого $t<t'<t''$ , $\gamma ,t',\nu \models \phi$ ,
$\gamma ,t,\nu \models \phi \mathbin {\mathcal {S}} \psi$ имеет место, если существует $t''<t$ такой, что $\gamma ,t'',\nu \models \psi$ и такой, что для каждого $t''<t'<t$ , $\gamma ,t',\nu \models \phi$ ,
$\gamma ,t,\nu \models x\sim c$ имеет место, если $t-\nu (y)\sim c$ ,
$\gamma ,t,\nu \models y.\xi$ имеет место, если $\gamma ,t,\nu [y\to t]\models \phi$ держит.

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

Метрическая темпоральная логика — это еще одно расширение LTL, позволяющее измерять время. Вместо добавления переменных он добавляет бесконечное количество операторов. ${\mathcal {U}}_{I}$ и ${\mathcal {S}}_{I}$ для $I$ интервал неотрицательного числа. Семантика формулы $\phi \mathbin {\mathcal {U_{I}}} \psi$ в какое-то время $t$ по существу совпадает с семантикой формулы $\phi \mathbin {\mathcal {U}} \psi$ , с ограничениями, заключающимися в том, что время $t''$ на котором $\psi$ должно удерживаться происходит в интервале $t+I$ .

TPTL столь же выразителен, как и MTL. Действительно, формула MTL $\phi \mathbin {\mathcal {U_{I}}} \psi$ эквивалентно формуле TPTL $x.\phi {\mathcal {(}}x\in I\land \psi )$ где $x$ это новая переменная. ^[2]

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

TPTL строго более выразителен, чем MTL. ^[1]^: 2 как по синхронизированным словам, так и по сигналам. Для слов с синхронизацией ни одна формула MTL не эквивалентна $\Box (a\implies x.\Diamond (b\land \Diamond (c\land x\leq 5)))$ . По сигналу не существует формулы MTL, эквивалентной $x.\Diamond (a\land x\leq 1\land \Box (x\leq 1\implies \neg b))$ , в котором говорится, что последнее атомарное предложение перед моментом времени 1 является $a$ .

Сравнение с ЛТЛ

Стандартное (неограниченное по времени) бесконечное слово $w=a_{0},a_{1},\dots ,$ это функция от $\mathbb {N}$ к $A$ . Мы можем рассмотреть такое слово, используя набор времени $T=\mathbb {N}$ , и функция $\gamma (i)=a_{i}$ . В этом случае для $\phi$ произвольная формула LTL, $w,i\models \phi$ тогда и только тогда, когда $\gamma ,i,\nu \models \phi$ , где $\phi$ рассматривается как формула TPTL с нестрогим оператором, а $\nu$ — единственная функция, определенная в пустом множестве.