Система Гильберта для темпоральной логики
Формальная теория Kt состоит из следующих аксиом и правил вывода.
Аксиомы
1) Формулы D(B1, … Bn), где D(p1, …, pn) – пропозициональные тавтологии.
2) [F](A ® B) ® ([F]A ® [F]B); [P](A ® B) ® ([P]A ® [P]B) (нормальность).
3) [F]A ® [F][F]A (транзитивность).
4) A ® [F]<P>A; A ® [P]<F>A (отражение).
Правила вывода
; 
.
Здесь А, В, В1, …, Вn – темпоральные формулы, возможно, содержащие [F] и [P].
Исходя из того, что для любой интерпретации с помощью шкалы Крипке формулы A ® [F]<P>A и A ® [P]<F>A будут тавтологиями, легко доказать следующую теорему корректности и полноты:
Теорема 1. Для любой темпоральной формулы А утверждение Kt 
A верно, если и только если А – тавтология относительно каждой шкалы Крипке (W, R), имеющей транзитивное отношение R. Здесь Kt ,означает, что А – теорема в формальной теории Kt.
Потоки времени
В темпоральной логике используются нерефлексивные транзитивные шкалы Крипке.
Шкала Крипке (W, <) называется потоком времени, если
1) "x Î W (Ø(x < x)),
2) "x, y, z Î W (x < y & y < z ® x < z).
Если t < v, то v называется будущим для t, а t – прошлым для v.
Теорема 2. Для любой темпоральной формулы А утверждение Kt A верно, если и только если А – тавтология относительно всех потоков времени.
Линейные потоки времени
Чтобы ограничить виды потоков времени, к системе Kt добавляются аксиомы. Аксиомы <F>1 и <P>1 означают отсутствие наименьшего и наибольшего t Î W.
Истинность аксиомы [F][F]A ® [F]A равносильна свойству плотности отношения доступности:
"t"u (t < u ® $v(t < v <u)).
Например, Q и R – плотные линейно упорядоченные множества, а Z – нет.
Для того чтобы потоки времени были линейно упорядочены, т.е. удовлетворяли условию:
"t"u (t < u Ú t = u Ú u < t),
добавляется аксиома
<F>A&<F>B ® <F>(A&B)Ú<F>(A&<F>B)Ú(B&<F>A)
(или её зеркальное отображение).
В случае шкалы (Z, <) добавляются аксиомы:
[F]([F]A ® A) ® (<F>[F]A ® [F]A),
[P]([P]A ® A) ® (<P>[P]A ® [P]A).
Для шкалы (N, <) добавляются аксиомы:
[F]([F]A ® A) ® (<F>[F]A ® [F]A),
[P]([P]A ® A) ® [P]A.
Для (R, <) добавляются аксиомы, обеспечивающие плотность отношения порядка и отсутствие максимального и минимального элементов. Добавляется аксиома Прайера:
<F>[F] ® <F>ØA ® <F>)[F]A& Ø<P>[F]A).
Стандартный перевод
С целью обобщения теоремы Салквиста на темпоральную логику применяются преобразования:
1) атомы р переводятся в унарные предикаты р*(х);
2) 1* = 1, 0* = 0;
3) (ØА)* = Ø(А*);
4) (А & В)* = А* & В*, (А Ú В)* = А* Ú В*;
5) ([F]A)* = "y(x < y ® A*(y)), где y – новая переменная;
6) ([P]A)* = "y(x < y ® A*(y)), где y – новая переменная;
7) (<F>A)* = $y(x < y & A*(y));
8) (<P>A)* = $y(y < x & A*(y)).
Рассмотрим темпоральные операции, применяемые при описании программ и в параллельном программировании.
Завтра и вчера
Добавляются одноместные операции 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 (с тех пор, как случилось В, верно А).
Выбор операторов
Можно сформулировать темпоральную логику для применений одного типа, выбирая отдельные логические связки и темпоральные операторы. Булевы связки &, Ø и символ 1 включаются всегда.
Примеры
Темпоральная логика FT состоит из формул, построенных из символа 1 и атомов с помощью &, Ø, <F> и Т. Она включает оператор [F], ибо [F] = Ø<F>Ø.
Логика FPTY состоит из формул, построенных из символа 1 и атомов &, Ø, <F>, <P>, T и Y.
Логика US состоит из формул, построенных из символа 1 и атомов с помощью &, Ø, U, S.
В общем случае <F> и <P> невозможно выразить операторы T и Y. Тем не менее, операторы T и Y бывают нужны. Логика US включает формулы из FPTY:
<F>A = 1UA, <P>A = 1SA, TA = 0UA, YA = 0SA.
Стандартный перевод формул логики US основывается на определении:
(B U A)*(x) = $y(y > x & A*(y)) & "z(x < z < y ® B*(x)).
Перевод S определяется симметрично.
Пусть С – класс потоков времени. Темпоральная логика (такая, как FP или US) называется экспрессивно полной относительно С, если для любой формулы первого порядка q(х, Р1, …, Рn) существует формула А(Р1, …, Рn) темпоральной логики, для которой А*(х, Р1*, …, Рn*) эквивалентна q(х, Р1*, …, Рn*) над С. То есть, для любой модели М с потоком времени из С верно:
M |= "x (A*(x) « q(x)).
Теорема 3 (Кемп). Темпоральная логика US экспрессивно полна над любым классом полных по Дедекинду линейных потоков времени.
Под полным по Дедекинду линейным потоком времени (T, <) понимается линейно упорядоченное множество, в котором нет таких непустых подмножеств X,YÍT, таких, что
1) X È Y = T;
2) x < y для всех x Î X и y Î Y;
3) X не имеет наибольшего, а Y – наименьшего элементов.