5.4. Активность и достижимость

Достижимость — важная задача сетей Петри. Другой задачей, получившей много внимания в публикациях по сетям Петри, является активность. Как отмечено в разд. 4.1.4, активность связана с тупиками. Мы коснемся здесь двух задач, связанных с активностью сети Петри с начальной маркировкой Сеть Петри активна, если активен всякий ее переход. Переход активен в маркировке если для всякой маркировки существует последовательность такая, что разрешен в Переход пассивен в маркировке если не существует достижимой маркировки, в которой бы он мог быть запущен.

Определение 5.7. Задача активности. Активны ли все переходы

Определение 5.8. Задача активности одного перехода. Активен ли данный переход

Очевидно, что задача активности сводится к задаче активности одного перехода. Для нахождения решения задачи активности мы просто решим задачу активности одного перехода для каждого если то мы должны решить задач активности одного перехода.

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

Сеть Петри строится из введением двух позиций и трех переходов Сначала модифицируем все переходы включая в качестве входа и выхода. Начальная маркировка будет включать фишку в Позиция это позиция «действия», пока фишка остается в переходы могут запускаться. Следовательно, любая маркировка, достижимая в достижима также и в позициях Определим переход так, что его входом будет а выход пуст. Это позволяет удалить фишку из запрещая запуск всех переходов в и «замораживая» маркировку (Заметим, что все переходы находятся в конфликте и не только по определению, но и по построению могут запускаться каждый раз не более чем по одному.)

Позиция и переход позволяют сети достичь любой достижимой маркировки, затем запуском заморозить сеть в этой маркировке. Далее необходимо проверить, является ли позиция нулевой. Введем новые позицию и переход имеющий в качестве входа а в качестве выхода Если может когда-либо стать нулевой, то этот переход не является активным. В действительности вся сеть будет пассивной, если в этой маркировке сработает переход Следовательно, если может быть пустой, сеть неявляется активной. Если не может быть пустой, тогда всегда может быть запущен, помещая фишку в В этом случае мы должны будем вернуть фишку в и гарантировать, что все переходы в активны. Необходима уверенность в том, что активна, даже если не является активной. Это обеспечивается переходом который «наполняет» сеть фишками, гарантируя тем самым, что, если фишка помещена в каждый переход активен. Переход в качестве входа имеет а в качестве выхода все позиции Эта конструкция иллюстрируется рис. 5.6.

Далее, если маркировка достижима в тогда также может достичь этой маркировки в позициях путем выполнения той же самой последовательности запусков переходов. Затем можно запустить замораживая подмножество Поскольку запустить нельзя и пассивна. Таким образом, если может стать нулевой — неактивна.

Справедливо обратное, если неактивна, тогда должна быть

Рис. 5.6. (см. скан) Конструкция, переводящая задачу достижимости нуля в одной позиции (достижима ли маркировка с в задачу активности (является ли сеть активной?).

достижима маркировка из которой недостижимо состояние с фишкой в (Если в есть фишка, то разрешен, а повторно запуская достаточное число раз, можно разрешить любой (или все) переход, т. е. сеть активна.) Если не имеет фишек и не может их получить, тогда маркировка также должна быть нулевой. Таким образом, если неактивна, тогда достижима маркировка, в которой маркировка нулевая.

На основе этой конструкции мы доказали следующую теорему.

Теорема 5.5. Задача достижимости сводится к задаче активности.

Для доказательства основного утверждения раздела покажем следующее.

Теорема 5.6. Задача активности одного перехода сводится к задаче достижимости.

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

Рис. 5.7. Сеть Петри, иллюстрирующая пассивные маркировки для

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

В общем случае, однако, может существовать бесконечное число пассивных для маркировок и бесконечное множество маркировок, в котором находятся пассивные для маркировки. Заметив два свойства, сведем множество маркировок, которые необходимо проверить для достижимости, к конечному числу. Во-первых, если маркировка пассивна для то и любая маркировка пассивна для (Любая последовательность запусков, возможная из возможна также из поэтому если может привести к запуску то это может и Во-вторых, маркировки некоторых позиций не будут влиять на пассивность для данной маркировки, поэтому маркировки этих позиций являются «несущественными», они могут быть произвольными. Заимствуя прием из построения дерева достижимости, заменим «несущественные» компоненты на показывая, что в этих позициях может быть произвольно большое число фишек, не влияющих на пассивность маркировки для Теперь, поскольку любая пассивна для если пассивна для нам не нужно рассматривать позиции Это означает, что мы применяем задачу достижимости подмаркировки с

Рассмотрим в качестве примера сеть Петри на рис. 5.7. Маркировки являются пассивными для но их можно представить конечным образом множеством .

Хэк [113, 116] показал, что для сети Петри С существует такое конечное множество маркировок (расширенных, т. е.

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

Более того, можно эффективно вычислять. Поскольку конечно, -компоненты имеют верхнюю границу Граница определяется как такое наименьшее число, что если пассивна для любая маркировка такая, что для всех то является пассивной для и подмаркировка такая, что если если При такохм определении можно построить следующим образом.

1. Вычислить Начать с увеличивать до тех пор, пока не окажется, что удовлетворяет описанному определению границы. Проверка каждого требует проверки всех маркировок с компонентами, меньшими или равными

2. Вычислить проверкой всех маркировок и подмаркировок с компонентами, не превышающими или равными это множество пассивных для маркировок из множества маркировок.

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

Теорема 5.7. Следующие задачи эквивалентны:

1. Задача достижимости.

2. Задача активности.

3. Задача активности одного перехода.

Более формальные доказательства сводимости активности к достижимости можно найти в [113, 116].