Аксиомы pdl

Можно ожидать, что для любых формулы А и программы    формула <*>А, (означающая возможность того, что после кратного применения  машина перейдёт в состояние, удовлетворяющее формуле А), будет равносильна формуле А  <; *>А, (означающей, что верно А, или А будет, возможно, верно после применения  не менее, чем 1 раз). Получим аксиому:

<*>А  А  <; *> А.

Аналогично, исходя из других соображений, получаем аксиомы PDL и формальную теорию:

1. все тавтологии исчисления высказываний;

2. <>A & <>B  <>(A & B);

3. <>(A  B)  <>A  <>B);

4. <  >A  <>A  <>A;

5. < ; >A  <><>A;

6. <A?>B  A&B;

7. A  <><*>A  <*>A;

8. <*>A  A  <*> (A & <>A).

Аксиомы 1 – 3 стандартны для модальных логик. Аксиома 8 равносильна аксиоме Сегерберга:

[*](A  []A)  (A  [*]A)

и называется аксиомой PDL – индукции.