Завтра и вчера

Добавляются одноместные операции T(завтра) и Y(вчера), и новое правило для построения формул:

Если А – формула, то TA и YA – формулы. Семантика в модели M = (Z, <, h):

M, t |= TA, если и только если M, t+1 |= A;

M, t |= YA, если и только если M, t-1 |= A.

Вместо TA применяются также записи Next A, 0A, XA.

Since, Until

Для любых формул А и В добавляются формулы ASB и AUB. Семантика в модели M = (W, <, h):

M, t |= AUB, если и только если для некоторого u > t верно M, u |= B и при всех v, удовлетворяющих соотношениям t < v < u, верно M, v |= A (иными словами, А верно до тех пор, пока не В);

M, t |= ASB, если и только если для некоторого u > t верно M, u |= B, а для всех v, удовлетворяющих соотношениям u < v < t, верно M, v |= A (с тех пор, как случилось В, верно А).