Методы анализа на основе дерева достижимости

Дерево достижимости. Дерево достижимости представляется множеством состояний сети.

 

P1 t2 P3

 

 

В начальной маркировке (1, 0, 0) разрешены два перехода t₁ и t₂. Первый шаг построения дерева достижимости показан на рис (б). Из маркировки (1, 1, 0) можно снова запустить t₁ (получая (1, 2, 0)) и t₂ (получая (0, 2, 1)); из (0, 1, 1) можно запустить t₃ (получая (0, 0, 1)). Второй шаг построения дерева достижимости показан на рис (в).

 

 

 

 

Продолжая три маркировки (рис (в)) на третьем шаге маркировки (рис (г)). Маркировка (0, 0, 1) пассивная: никакой переход в ней не разрешен. Маркировка (0, 1, 1), порождаемая запуском t₃ в (0, 2, 1) была уже порождена непосредственно из начальной маркировки запуском t₂.

 

 

Если эту процедуру повторять снова и снова, каждая достижимая маркировка окажется порожденной, а полученное дерево может оказаться бесконечным.

Всякий путь в дереве, начинающийся в корне соответствует допустимой последовательности переходов.

Для превращения дерева в полезный инструмент анализа необходимо найти средства ограничения его до конечного размера. Приведение к конечному представлению осуществляется двумя операциями.

Первая из них – это использование пассивных маркировок, именуемых терминальными вершинами, и маркировок, ранее встречавшихся в дереве, именуемых дублирующими вершинами. В нашем примере маркировка (0, 0, 1) – терминальная, а (0, 1, 1) – дублирующая.

Вторая операция. Рассмотрим последовательность запусков переходов s, начинающуюся в начальной маркировке М₀ и концом M’, M’>M₀. Маркировка M’ совпадает с маркировкой М₀, за исключением того, что имеет некоторые «дополнительные» метки в некоторых позициях, то есть M’=M₀+(M’-M₀) и (M’-M₀)>0. Поскольку на запуски переходов дополнительные метки не влияют, последовательность s можно запустить снова, начиная в M’, приходя к маркировке M”. Так как действие последовательности переходов s добавило M’-M₀ меток к маркировке M₀, она добавит также M’-M₀ меток к маркировке M’, поэтому M”=M’+(M’-M₀) или M”=M₀+2(M’-M₀). В общем случае последовательность s можно запустить n раз, получив в результате маркировку M₀+n(M’-M₀).

В нашем примере можно запустить переход t₁ столько раз сколько необходимо для того, чтобы получить произвольное число меток в P₂. Это бесконечное число маркировок обозначим символом w. Для любого a определим

w+а=w, w-а=w, а<w, w£w

Эти операции с символом w достаточны для построения дерева.

 

Алгоритм построения дерева. Каждая вершина i дерева связывается с расширенной маркировкой M(i). В этой маркировке число меток в позиции может быть либо неотрицательным целым, либо w. Каждая вершина классифицируется как граничная или терминальная или дублирующая или внутренняя.

Граничными являются вершины, которые не обработаны алгоритмом. Алгоритм превратит их в терминальные, дублирующие, внутренние.

Алгоритм начинает с начальной маркировки М₀, принимая ее в качестве граничной вершины.

Пусть х – граничная вершина.

1. Если в дереве имеется другая вершина у, не являющаяся граничной, и с ней связана также маркировка М(х)=М(у), то вершина х – дублирующая.

2. Если для маркировки М(х) ни один из переходов не разрешен для всех t_jÎT, то х – терминальная вершина.

3. Для всякого перехода t_jÎT, разрешенного в М(х), создать новую вершину z дерева. Маркировка М(z) определяется для каждой позиции P_i следующим образом:

а) если М(х)i=w, то М(z)_i=w.

б) если на пути от корневой вершины к х существует вершина у с М(у)<d(M(x), t_j) и М(у)_i<d(M(x), t_j)_i, то М(z)_i=w, d - функция следующего состояния.

в) в противном случае М(z)_i=d(M(x), t_j)_i,

Функция d(M(x), t_j) не определена, если t_j не разрешен в маркировке М(х). Если t_j разрешен, то d(M(x), t_j)=M’(x), где M’(x) – маркировка, полученная после срабатывания t_j. Дуга, помеченная t_j, направлена от вершины х к вершине z. Вершина х переопределяется как внутренняя, вершина z становится граничной.

Когда все вершины дерева – терминальные, дублирующие или внутренние, алгоритм останавливается.

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

 

 

Имеется доказательство того, что алгоритм конечный и не может создавать новые граничные вершины бесконечно.

Ниже на рис. 5.15 приведем еще один пример сети Петри и дерево достижимости для него.

 

Рис 5.15. Пример дерева достижимости

 

Анализ сетей Петри на основе дерева достижимости. Сеть Петри ограничена тогда и только тогда, когда символ w отсутствует в ее дереве достижимости. Если сеть ограничена и символ w отсутствует в дереве достижимости, то сеть представляет систему конечных состояний. Это позволяет решить вопросы анализа простым перебором и проверкой конечного множества всех достижимых маркировок.

Сеть Петри является сохраняющей, если она не теряет и не порождает метки, а просто передвигает их. Свойство сохранения проверяется по дереву достижимости вычислением для каждой маркировки суммы меток. Если метки взвешены, то вычисляется взвешенная сумма. Если сумма одинакова для каждой достижимой маркировки, сеть - сохраняющая.

Задача покрываемости маркировки М маркировкой М’ сводится к поиску на дереве такой вершины х, состояние которой покрывает состояние М. Если такой вершины М(х) не существует, маркировка М не покрывается никакой достижимой маркировкой.

Таким образом, дерево достижимости можно использовать для решения задач безопасности, ограниченности, сохранения и покрываемости. К сожалению, в общем случае его нельзя использовать для решения задач достижимости и активности, а также для определения возможной последовательности запусков. Решение этих задач ограничено существованием символа w. Символ w означает потерю информации, конкретные количества меток отбрасываются, учитывается только существование их большого числа. Вместе с тем, в отдельных конкретных случаях дерево достижимости позволяет судить о свойствах достижимости и активности. Например, сеть, дерево достижимости которой содержит терминальную вершину, не активна. Аналогично искомая маркировка M’ в задаче достижимости может встретиться в дереве достижимости, что означает ее достижимость. Кроме того, если маркировка не покрывается некоторой вершиной дерева достижимости, то она недостижима.