Линейные потоки времени

Чтобы ограничить виды потоков времени, к системе 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 – наименьшего элементов.








Дата добавления: 2016-09-20; просмотров: 603;


Поиск по сайту:

При помощи поиска вы сможете найти нужную вам информацию.

Поделитесь с друзьями:

Если вам перенёс пользу информационный материал, или помог в учебе – поделитесь этим сайтом с друзьями и знакомыми.
helpiks.org - Хелпикс.Орг - 2014-2024 год. Материал сайта представляется для ознакомительного и учебного использования. | Поддержка
Генерация страницы за: 0.006 сек.