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

Задача достижимости — одна из самых важных задач анализа сетей Петри. Она до сих пор еще не решена для различных вариаций ее определения. Были поставлены следующие четыре задачи достижимости для сети Петри с начальной маркировкой

Определение 5.3. Задача достижимости. Выполняется ли для данной

Определение 5.4. Задача достижимости подмаркировки. Для подмножества и маркировки существует ли такая, что Для всех

Определение 5.5. Задача достижимости нуля. Выполняется ли где для всех

Определение 5.6. Задача достижимости нуля в одной позиции. Для данной позиции существует ли

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

Хотя эти четыре задачи различны, все они эквивалентны. Определенные взаимосвязи очевидны сразу. Задача достижимости нуля сводится к задаче достижимости; просто в задаче достижимости устанавливается Аналогично задача достижимости сводится к задаче достижимости подмаркировки путем установки Задача достижимости нуля в одной позиции сводится к задаче достижимости подмаркировки установкой Сложнее показать, что задача достижимости подмаркировки сводится к задаче достижимости нуля и что задача достижимости нуля

сводится к задаче достижимости нуля в одной позиции. Все множество взаимосвязей представлено на рис. 5.1.

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

Рис. 5.1. Сводимость задач достижимости. Дуга от одной задачи к другой означает, что первая сводится ко второй.

Наш подход заключается в построении новой сети Петри с начальной маркировкой такой, что маркировка для всех существует тогда и только тогда, когда

Построение из осуществляется исключительно просто. Начнем с 62, совпадающей с Для того чтобы позволить всякой позиции вне стать пустой, введем переход с входом и пустым выходом. Этот переход можно запускать всякий раз, когда в имеются фишки, чтобы изъять их, что позволяет достичь нулевой маркировки и тем самым игнорировать такие позиции.

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

Рис. 5.2. Сеть Петри, служащая для доказательства сводимости задачи достижимости подмаркировки к задаче достижимости нуля. Подмножество позиций будет иметь маркировку в первоначальной сети тогда и только тогда, когда в модифицированной показанным здесь способом сети будет достижима нулевая маркировка.

Два типа вводимых переходов иллюстрируются на рис. 5.2. Формально определим следующим образом:

с начальной маркировкой:

Теорема 5.1. Задача достижимости подмаркировки сводится к задаче достижимости нуля.

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

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

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

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

Построение определяет так, что всякий раз число фишек в равно сумме числа фишек в позициях Следовательно, если то в позициях нет фишек, и наоборот. Определим начальную маркировку следующим образом:

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

Тогда это разность числа фишек после запуска перехода и числа фишек до запуска Теперь, если то фишек должно быть добавлено в позицию поэтому введем дуг из если то удалим фишек из введением дуг из

Если то

Если , то

Если , то

При таком построении любая последовательность запусков переходов, приводящая к маркировке 0, приведет к маркировке (а также и наоборот.

Теорема 5.2. Задача достижимости нуля сводится к задаче достижимости нуля в одной позиции.

Доказательство. Формальное доказательство, основанное на описанной конструкции, оставляем читателю.

На основе этих двух теорем и очевидных выводов можно заключить следующее:

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

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

2. Задача достижимости нуля.

3. Задача достижимости подмаркировки.

4. Задача достижимости нуля в одной позиции.

Эти теоремы и их доказательства принадлежат главным образом Хэку [116].