Разработка алгоритмов планирования

. а) для любого действия 𝜇"≠b"Îres верно, что (𝜇")=𝜇Îseq,

б) для любого действия 𝜇Îseq верно, что ħ(𝜇)=𝜇'Îрlan,

в) из а) и б) следует что, 𝜇"~𝜇'.

. Количество альтернативных расположений b'Îplan среди действий plan'a, подобных действиям из res (имеется в виду подобие, выведенное в 3 пункте: 𝜇"~𝜇') и между действиями ħ(a)=a' и ħ(𝜒)=𝜒' конечно.

. из 2, 3, 4 и по определению гомоморфизма последовательностей следует, что существует такая последовательность действий resÎRESseq, что ħ(res)=plan Единственность существования res, такого, что ħ(res)=plan, следует из того факта, что не существует альтернативного порядка следования действий в res, для которого сохранилось бы утверждение ħ(res)=plan. Следовательно, последовательность res единственна Докажем возможность res=plan.

В любой последовательности resÎRESseq количество действий больше чем в seq.

Количество действий в плане конечно.

. Тогда из А.5, C.l, С.2 следует, что в одном из вариантов пошагового разрешения действительно имеет место res≅plan.

Теорема доказана.

Обратим внимание, на интересное свойство последовательности init

.

Начальная последовательность init такова, что ħ (I,it) = plan, где plan - это любой существующий план для задачи Т.

Очевидно.

Теперь мы можем модифицировать алгоритм ITPA. Назовём его CRPA (conflict resolution planning algorith).

Рис. 11 - Алгоритм CRPA

Основной идеей алгоритма CRPA является полное разрешение конфликтов некоторой исходной последовательности действий seq, дли которой справедливо ħ(seq)=plan. Полное разрешение конфликтов приводит к множеству последовательностей, которые в свою очередь могут также содержать конфликты. Разрешение конфликтов продолжается для очередных последовательностей, до тех пор, пока не будут получены бесконфликтные последовательности действий.

Алгоритм CRPA начинает свою работу с разрешения конфликтов в последовательности init=(start, finish). Более того, задача планирования Т может оказаться тривиально разрешимой, то есть GÌ, и как следствие eff(start)=pre(flnish) без каких-либо конфликтов. Множество взаимовлияний, порождаемое последовательностью init, будем называть первичными взаимовлияниями.

Приведём теорему 2 описанную в [59].

Теорема 2.

Если для задачи планирования Т существует решение, то алгоритм CRPA найдёт план.

Доказательство:

l.Ha вход CRPA подаётся последовательность seq=init, обладающая свойством ħ (seq) = plan, где plan - это некоторый конкретный план.

. Алгоритм CRPA есть не что иное, как процедурная реализация пошагового полного разрешения конфликтов входной последовательности seq.

. Из 1 и 2, и в соответствии с теоремой 1. следует, что существует одна из рекурсивных ветвей алгоритма, которая возвращает конкретный план plan. Теорема доказана.

Опишем

утверждение 3 приведённое в [59].

Утверждение 3.

Если для задачи планирования Т существует решение, то алгоритм CRPA найдёт все планы.

Доказательство:Это так поскольку, относительно любого плана plan, решающего задачу планирования Т, справедливо утверждение ħ(init)=plan.