6.5. Темпоральная логика

Для темпоральной логики вместо символа используются символы [F] – «будет» и [P] – «было». Аналогично символу  определяются символы <F> = [F] и <Р> = [Р]. Модель Крипке M = (W, R, h) была определена как граф вместе с оценкой h : P  P(W). Напомним, что истинность формул [F]A и [P]A устанавливается с помощью выражений:

M, t |= [F]A, если и только если M, u |= A для всех u  W, таких, что R(t, u);