Алгоритм построения дерева достижимости

Рассмотрим алгоритм построения усеченного ДД. Пусть х – граничная вершина. Сначала это х₀, соответствующая µ₀. Строить дерево будем в ширину, вершины одного уровня будем обрабатывать слева направо. Алгоритм работает до тех пор, пока имеются граничные вершины.

1. Если для маркировки µ[x] ни один из переходов не разрешен (т. е. δ(µ[x], t_j) не определена для всех t_j ∈ Т), то х – терминальная вершина.

2. Если в построенной части дерева имеется вершина у≠x, для которой µ[x]= µ[y], то вершина х – дублирующая.

3. Если х – нетерминальная и недублирующая, то для х существуют переходы t_j ∈Т:

δ(µ[x], t_j) определена. Поэтому существует дуга из вершины х, помеченная t_j и ведущая в вершину z.

Маркировка µ[z], связанная с этой вершиной, определяется для каждой позиции р_i следующим образом:

а) если µ[х]_i= ω, то µ[z]_i=ω.

б) если на пути от корневой вершины к х существует вершина y:

µ[y]< δ([x], t _j) и µ[y] _i < δ(µ[x], t _j) _i, то µ[z] _i = ω.

Отметим, что в данном случае используется принцип монотонности, с помощью символа мы говорим, что все переходы, разрешенные в вершине y, разрешены и в вершине z. Это позволяет усечь (ограничить) ДД, правда, часть информации теряется – мы можем сказать, что количество фишек в позиции может быть потенциально сколь угодно большим, но не можем сказать, какие точные значения

оно может принимать.

в) Во всех остальных случаях µ[z] _i = δ(µ[x],t _j) _i.

После обработки вершина х становится внутренней, а z – граничной. Когда все вершины становятся дублирующими либо терминальными либо внутренними, работа алгоритма завершается.

Замечание 1. Алгоритма построения усеченного дерева достижимости позволяет установить в сети наличие пассивных переходов и позиций. Если ни одна из дуг дерева достижимости не помечена названием данного перехода, то он пассивный. Если некоторая позиция во всех вершинах дерева достижимости имеет ноль фишек, то позиция – пассивная.

Замечание 2. В процессе построения усеченного ДД использование символа ω приводит к потере информации о том, какие именно значения может принимать количество фишек в позиции, известно лишь, что это число потенциально сколь угодно большое. Следствием этого является невозможность применения усеченного ДД для решения задач достижимости и покрываемости,если маркировки его вершин содержат символ ω.

Замечание 3. Еще одним важным свойством алгоритма построения усеченного ДД является то, что он заканчивает работу за конечное число шагов. Доказательство этого свойства алгоритма основано на трех леммах.

Поиск по сайту: