Стандартный перевод

С целью обобщения теоремы Салквиста на темпоральную логику применяются преобразования:

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)).

Рассмотрим темпоральные операции, применяемые при описании программ и в параллельном программировании.