Семантика пропозициональной динамической логики

Пусть ₀ – множество базисных программ,  – множество всех программ, Р – атомные формулы, F(P) – все формулы, W – множество состояний машины, в которой могут работать программы . Для каждого    определена модальность []. Стало быть, мы должны каждому  поставить в соответствие некоторое отношение доступности R_  W  W.

Шкала Крипке (или система переходов) будет состоять из пары: (W, (R_)_), где W – множество состояний, а R_{ –} отношения R_  W  W.

Программу можно интерпретировать как множество пар (x, y)  R_ таких, что после выполнения программы  машина из состояния х перейдёт в состояние y. Каждому атому p  P ставится в соответствие подмножество h(p)  W состояний, при которых высказывание р верно.

Интерпретацией называется тройка M = (W, (R_)_, h), состоящая из шкалы Крипке и оценки h : P  P(W), удовлетворяющих соотношениям:

1. R_  _ = R_  R_;

2. R_ ; _ = R_  R_;

3. ;

4. R_A? = {(x, x) : x  W и M, x |= A}.

Здесь R_* – наименьшее рефлексивное транзитивное отношение, содержащее R_. Расширим h на множество формул F(P), полагая t  h(A), если и только если M, t |= A. Получим соотношения:

5. h(A  B) = h(A)  h(B);

6. h(A) = W \ h(A);

7. h(<>A) = {t  W : (t, u)  R_ для некоторого u  h(A)}.

В некоторых случаях под семантикой логики PDL понимают шкалу с расширенной на F(P) оценкой, удовлетворяющие соотношениям 1 – 7.