logo search
МЛиТА 6 - 7

Пропозициональная динамическая логика

Пусть 0 – произвольное множество. Его элементы называются базисными программами. Предположим, что   0 – такое множество слов, что вместе с любыми 1, 2   оно содержит:

  1. 1  2 (неопределённый выбор одной из программ 1 или 2);

  2. 1 ; 2 (выполнение 1 ,затем 2);

  3. 1* (выполнение 1 конечное, возможно нулевое, количество раз);

  4. 1  2 (одновременное выполнение программ 1 или 2).

Элементы из  будем называть программами. Рассмотрим атомы из Р как простые высказывания о состояниях машины, в которую загружаются программы. Для каждой программы    обозначим через [] соответствующую ей модальность. Определим формулы пропозициональной динамической логики PDL по индукции:

  1. атомы р  Р – формулы;

  2. А & В, А, []А – формулы для любых формул А и В, и элемента   ;

  3. все формулы PDL составляются с помощью правил 1 – 2.

Введём обозначение: <>А как сокращение для []А.

Для каждой формулы А определим программу: А?  , тестирующую, верна ли формула А. Эта программа заканчивает работу, если формула А верна, и зависает (аварийно завершает работу), если нет. Эта программа вводится с целью интерпретации оператора

if (A) then 1 else 2

как программы

(А?; 1)  ((А)? ; 2)  .