Система Гильберта для темпоральной логики

Формальная теория K_t состоит из следующих аксиом и правил вывода.

Аксиомы

1) Формулы D(B₁, … B_n), где D(p₁, …, p_n) – пропозициональные тавтологии.

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 (отражение).

Правила вывода

; .

Здесь А, В, В₁, …, В_n – темпоральные формулы, возможно, содержащие [F] и [P].

Исходя из того, что для любой интерпретации с помощью шкалы Крипке формулы A ® [F]<P>A и A ® [P]<F>A будут тавтологиями, легко доказать следующую теорему корректности и полноты:

Теорема 1. Для любой темпоральной формулы А утверждение K_t A верно, если и только если А – тавтология относительно каждой шкалы Крипке (W, R), имеющей транзитивное отношение R. Здесь K_t ,означает, что А – теорема в формальной теории K_t.

Потоки времени

В темпоральной логике используются нерефлексивные транзитивные шкалы Крипке.

Шкала Крипке (W, <) называется потоком времени, если

1) "x Î W (Ø(x < x)),

2) "x, y, z Î W (x < y & y < z ® x < z).

Если t < v, то v называется будущим для t, а t – прошлым для v.

Теорема 2. Для любой темпоральной формулы А утверждение K_t 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(х, Р₁, …, Р_n) существует формула А(Р₁, …, Р_n) темпоральной логики, для которой А*(х, Р₁*, …, Р_n*) эквивалентна q(х, Р₁*, …, Р_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 – наименьшего элементов.