Warning: session_start(): open(C:\Windows\temp\sess_0s72ui1ftue55n0oekdieitmj6, O_RDWR) failed: No space left on device (28) in C:\www\lemma4.1php\login.php on line 15 Warning: session_commit(): open(C:\Windows\temp\sess_0s72ui1ftue55n0oekdieitmj6, O_RDWR) failed: No space left on device (28) in C:\www\lemma4.1php\login.php on line 36 Warning: session_commit(): Failed to write session data (files). Please verify that the current setting of session.save_path is correct (C:\Windows\temp) in C:\www\lemma4.1php\login.php on line 36 Сети Петри: модификации и расширения

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

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

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

Сначала определим понятие ординарной сети Петри.

Определение 28   Сеть Петри  N=(S,T,F,W,M0)  называется ординарной, если  W(f)=1  для каждой дуги  fF.  Поэтому ординарная сеть Петри, как правило, задается четверткой  N=(S,T,F,M0).

Рассмотрим ряд вспомогательных результатов, связанных с поведенческими свойствами ОСП. Начнем со свойства ограниченности.

Утверждение 3  Каждая k-ограниченная (ограниченная) ОСП имеет конечное множество достижимых маркировок.

Доказательство. Если ОСП k-ограничена, то она имеет не больше, чем (K+1)|S| достижимых маркировок, где S — множество мест сети. □

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

Лемма 8  Пусть  (N,M0)  ограниченная ОСП и  M1  ее достижимая маркировка. Тогда  M1M0M1=M0.

Доказательство. Пусть M0[σ>M1. Предположим, что M1M0. По лемме 4, имеем, что M0[σ>M1[σ>M2[σ>..., где Mi=M0+i.(M1-M0) для каждого iN. Из ограниченности ОСП следует, что M1-M0=0. □

Приведенные ниже утверждения показывают, что свойство живости сильнее свойств S -живости и M -живости.

Утверждение 4   Живая ОСП является S-живой.

Доказательство. Пусть (N,M0) — живая ОСП, M — ее достижимая маркировка и s — место в N. По определению N, существует по крайней мере один переход t из ss. В силу свойства живости, t может сработать при некоторой маркировке L[M>. Пусть L[t>L'. Если ts, то верно, что L'(s)1. Если ts, то имеем, что L(s)1. □

Утверждение 5   Живая ОСП является M-живой.

Доказательство. Предположим обратное, т.е. в ОСП достижима маркировка M, при которой ни один переход сети не может сработать. Тогда множество достижимых из  M  маркировок равно {M}. По определению базовой сети, ОСП содержит по крайней мере один переход t, который не может сработать при любой достижимой из M маркировке. Следовательно, ОСП не является живой. □

Покажем, что живые и ограниченные ОСП имеют ряд интересных свойств. Только сначала напомним, что A(σ)={tT|t=σ(i) для некоторого i} для любой последовательности срабатываний σ.

Лемма 9   Живая и ограниченная ОСП  (N,M0)  имеет достижимую маркировку M и последовательность срабатываний  σ  такие, что  M[σ>M  и все переходы сети N включены в  σ.

Доказательство. Пусть T — множество переходов в N и k — число достижимых маркировок в (N,M0). Согласно утверждению 3, число достижимых маркировок в (N,M0) конечно.

Так как (N,M0) — живая ОСП, то существует последовательность срабатываний σ1 такая, что M0[σ1>M1 и A(σ1)=T. Поскольку (N,M) — также живая ОСП, то существует последовательность срабатываний σ2 такая, что M1[σ2>M2 и A(σ2)=T. Таким образом мы можем построить последоватеоьность срабатываний σ1σ2σ3...σk такую, что

M0[σ1>M1[σ2>M2[σ3>...[σk>Mk

В силу выбора k, маркировки M0, M1, ..., Mk не могут быть попарно различны, так как их количество равно k+1. Предположим, что Mi=Mj для 0ijk. Определим M=Mi=Mj и σ=σi+1 ... σj. Тогда верно, что M[σ>M. Так как A(σi+1)=T и σi+1 — префикс σ, то имеем, что A(σ)=T. □

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

Теорема 13   Пусть  (N,M0)живая и ограниченная ОСП. Если N — связная сеть, то N сильно связная сеть.

Доказательство. В силу леммы 1, достаточно показать, что для каждой дуги (x,y) существует путь, ведущий из y в x. Согласно лемме 9, существует достижимая маркировка M и последовательность срабатываний σ такие, что M[σ>M и все переходы в N включены в σ по крайней мере один раз. Тогда верно, что бесконечная последовательность σσσ... разрешена при M.

Рассмотрим два случая.

Случай 1. (x,y)=(s,t) для некоторого места s и некоторого перехода t. Построим путь из t в s. Определим множества V={vT| существует путь из t в v} и U=T\V.

Покажем, что σ|V — последовательность срабатываний такая, что M[σ|V>M. Корректность этого утверждения очевидна в случае, когда σ не содержит переходы из U. Рассмотрим случай, когда σ|U — непустая последовательность.

По определению множества V, имеем, что (V)V. Следовательно, U и V — различные множества, удовлетворяющие условию UV=. Применяя лемму 5 к M[σσσ...>, получаем, что (σσσ...)|U=σ|Uσ|Uσ|U... разрешена при M.

Пусть M[σ|U>M'. Так как σ|U разрешена бесконечно часто при M, то число фишек в каждом месте не может уменьшаться при этом. Поэтому верно, что M'M. В силу леммы 8, имеем, что M'=M. Применяя лемму 5 к M[σ>M, получаем, что M[σ|Uσ|V>M. Следовательно, верно, что M[σ|U>M[σ|V>M.

По определению множества V, имеем, что tV. Значит, t содержится в σ|V. Так как ts и σ|V повторно приводит к M, существует переход vs, который также содержится в σ|V. Переход v принадлежит V, и, следовательно, существует путь π, который ведет из t в v. Поскольку vs, то путь πs ведет из t в s.

Случай 2. (x,y)=(t,s) для некоторого места s и некоторого перехода t. Построим путь из s в t. Определим множества U={uT| существует путь из u в t} и V=T\U.

Рассуждая, как в случае 1, получаем, что M[σ|U>M. Так как t содержится в σ|U и ts, то существует переход us, который также содержится в σ|U. Следовательно, существует путь π, который ведет из u в t. Поскольку us, то путь sπ ведет из s в t.    □

Пример 2-ограниченной и живой ОСП показан на рис. 2.20. Однако, если добавить еще одну фишку в место s2, то переход t1 может сработать дважды и тогда уже никакой другой переход сети не сможет сработать, т.е. ОСП больше не является ни S-живой, ни M-живой и ни живой. Пример безопасной и живой ОСП показан на рис. 2.21. Вместе с тем, после добавления фишки в место s данная ОСП будет небезопасной. Отметим, что базовые сети обеих ОСП являются сильно связными.