Warning: session_start(): open(C:\Windows\temp\sess_mtb2mj5r82nnq46jagkhae2fu5, 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_mtb2mj5r82nnq46jagkhae2fu5, 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 Сети Петри: модификации и расширения

2.2.7 FC-СП и их свойства

В данном параграфе рассматриваются свойства сетей Петри со свободным выбором (free-choice Petri nets) — FC-СП. Достоинство этого класса сетей состоит в том, что с одной стороны FC-СП — это элегантный математический аппарат, для которого многие проблемы анализа являются разрешимыми, а с другой — FC-СП позволяют моделировать достаточно широкий спектр параллельных систем.

Сначала рассмотрим альтернативные характеризации самого FC-свойства.

Утверждение 18

а)  Сеть  (S,T.F)  является FC-сетью, если и только если для каждых двух мест s и  s'  и каждых двух переходов t и  t'  верно

(s,t),(s,t')(s',t)F(s',t')F.

б)  Сеть  (S,T.F)  является FC-сетью, если и только если для каждых двух мест s и  s'  верно

ss'=s=s'.

в)  Сеть  (S,T.F)  является FC-сетью, если и только если для каждых двух переходов t и  t'  верно

tt'=t=t'.

Доказательство.

а)  Следует из определения FC-сети.

б)  (): Пусть N=(S,T.F)FC-сеть, и пусть s и s' — два места в N такие, что ss'. Тогда существует переход tss' и, следовательно, существуют дуги (s,t) и (s',t). Пусть t' — выходной переход места s. Тогда (s,t'). Согласно пункту а), имеем, что (s',t'). Тогда t' — выходной переход места s'. Следовательно, имеем ss'. Аналогично доказывается факт, что s's.

(): Пусть N=(S,T.F) не является FC-сетью, Тогда существуют дуга (s,t), место s't и переход t's такие, что (s',t')F. Значит, верно, что ss', поскольку ts и ts'. Так как t's и t's', то ss'.

в)  Аналогично доказательству пункта б).                   □

Рассмотрим фундаментальное свойство FC-сети.

Утверждение 19  Пусть s — место в FC-сети N и M — маркировка N. Если некоторый переход из  s  может сработать при M, то любой переход из  s  может сработать при M.

Доказательсво. Непосредственно следует из утверждения 18 (пункт в).                             □

Теперь рассмотрим свойства кластеров FC-сети. Кластеры FC-сети имеют простую структуру: каждое место s кластера c связано с каждым переходом t данного кластера дугой (s,t). Это означает, что все переходы кластера имеют одно и то же множество входных мест, и все места кластера имеют одно и то же множество выходных переходов. Тогда фундаментальное свойство FC-сети может быть переформулировано следующим образом.

Утверждение 20  Если в FC-сети переход t может сработать при некоторой маркировке, то любой другой переход кластера  [t]  может сработать при этой маркировке.

Доказательство. Непосредственно следует из того факта, что в FC-сети все переходы кластера имеют одно и то же множество входных мест.                            □

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

Следующая лемма устанавливает взаимосвязи между мертвыми местами и мертвыми переходами в FC-сети.

Лемма 10   Если переход t в FC-сети мертв при маркировке M, то некоторое его входное место мертво при некоторой мркировке, достижимой из M.

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

Пусть t={s1, ..., sn}. В силу утверждения 18 (пункт б), все входные места перехода t имеют одно и то же множество выходных переходов. Так как все входные места перехода t не мертвы при любой маркировке, достижимой из M, то существуствуют последовательности срабатываний σ1, ..., σn такие, что верно

M[σ1>M1...Mn-1[σn>Mn,

где Mi(si)>0 для 1in.

Если в приведенной выше последовательности содержится переход u кластера [t], то u может сработать при некоторой промежуточной маркировке (1jn). Поскольку t и u принадлежат одному и тому же кластеру, то t может сработать при той же маркировке Mj, в силу утверждения 19. Тогда t не мертв при M.

Если в приведенной выше последовательности не содержится никакой переход кластера [t], то количество фишек в местах из множества t не уменьшается при любом функционировании сети. Поэтому верно, что Mn(si)>0 для 1in. Тогда t может сработать при Mn. Тогда t не мертв при M.            □

Из рассмотренной леммы легко следует, что в FC-СП свойства S-живости и живости совпадают.

Утверждение 21   FC-СП жива, если и только если она S-жива.

Доказательство. Факт, что живая FC-СП является S-живой, установлен в утверждении 4. Покажем, что S-живая FC-СП является живой. Отметим, что в неживой FC-СП существует достижимая маркировка M и переход t такие, что t мертв при M. По лемме 10, некоторое входное место перехода t мертво при некоторой маркировке, достижимой из M. Таким образом, FC-СП не S-жива.                  □

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

Теорема 24   Ограниченная и сильно связная FC-СП является живой, если и только если она M-жива.

Доказательство.

(): Выполняется для всего класса ОСП, согласно утверждению 5.

(): Пусть (N,M0) — ограниченная, сильно связная и M-живая FC-СП.

Пусть K — достижимая в FC-СП маркировка такая, что число переходов, мертвых при K, максимально, т.е. ни при каких достижимых маркировках нет больше мертвых переходов, чем при маркировке K. Покажем, что число переходов, мертвых при K, равно 0, т.е. никакой переход не становится мертвым ни при одной достижимой маркировке и, следовательно, FC-СП жива.

Так как (N,M0)  M-жива, то некоторый переход t не мертв при K. Поскольку N сильно связна, то в сети существует путь, начинающийся в t и содержащий все переходы данной сети. Покажем, что если u и v — следующие друг за другом переходы рассматриваемого пути и u не мертв при K, то v также не мертв при K. Это означает, что ни один переход не мерт при K.

Поскольку u не мерт при некоторой маркировке L, достижимой из K, то существует бесконечная последовательность срабатываний σ такая, что K[σ> и σ содержит u бесконечно часто. Так как мертвые переходы остаются мертвыми, то количество мертвых переходов при L больше, чем при K, что противоречит определению K. Исходя из того, что u и v — следующие друг за другом переходы рассматриваемого пути, то существует место s такое, что (u,s) и (s,v) — дуги в сети. Поскольку s ограничено, то некоторый переход v's содержится бесконечно часто в σ, т.е. v' не мертв при K. Согласно утверждению 19v и v' могут сработать при одних и тех маркировках. Таким образом, v не мертв при K.                             □

Теорема Коммонера

В этом пункте рассматривается теорема Коммонера, которая формулирует критерий живости FC-СП:

FC-СП жива  каждый тупик содержит изначально маркированную ловушку.

Лемма 11  Неживая FC-СП содержит тупик R и имеет достижимую маркировку M такие, что R не маркируется M.

Доказательство. В силу утверждения 21, свойства S-живости и живости совпадают, неживая FC-СП является не S-живой. Поэтому некоторое место s мертво при достижимой маркировке L. Пусть M[L> — маркировка такая, что каждое место, не мертвое при M, не мертво при любой маркировке из [M>. Такая маркировка существует, поскольку мертвое место остается мертвым (множество мертвых мест может только увеличиваться при срабативании переходов), и множество мертвых мест конечно. Тогда все маркировки из [M> имеют то же самое множество R мертвых мест. Покажем, что R — тупик, который не маркируется M. Сначала докажем корректность следующих трех утверждений.

  1. R. Место s мертво при L. Поскольку мертвое место остается мертвым, то s мертво при M. Тогда sR.
  2. Множество R содержит только переходы, мертвые при M. Пусть sR. Тогда s мертво при M. Тогда каждый переход из s мертв при M.
  3. Каждый переход t, мертвый при M, имеет входное место из R. В силу леммы 10, некоторое место st мертво при маркировке, достижимой из M. По определению маркировки M, это место уже мертво при M, и поэтому оно принадледит множеству R.

Согласно утверждениям 1 и 2, R — тупик. R не маркируется M, поскольку, по определнию мертвого места, каждое место, мертвое при M, не маркируется M. □

Рассмотрим первую часть теоремы Коммонера.

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

Доказательство. В силу леммы 11, неживая FC-СП содержит тупик R такой, что M(R)=0 для некоторой достижимой маркировки M. Тогда каждая ловушка, содержащаяся в R, не маркируется M. Так как маркированная ловушка остается маркированной, то каждая ловушка, содержащаяся в R, изначально не маркирована.                                     □

Доказательство теоремы Коммонера в обратную сторону значительно сложнеее. Нам понадобятся некоторые вспомогательные понятия и обозначения.

Определение 37  Пусть C — множество кластеров сети  (S,T,F)  такое, что каждый кластер из C содержит по крайней мере один переход. Назначением  называют функцию  α:CT,  удовлетворяющую условию: cC    α(c)c.

Переход t является  α-назначенным, если  t=α(c)  для некоторого кластера c. Множество  α-назначенных переходов обозначается как  α(C).

Назначение называется  тотальным,  если C — множество кластеров сети N, содержащих по крайней мере один переход.

Назначение определяет стратегию для разрешения конфликтов между переходами кластера.

Пусть c — кластер из области определения назначения α. Предположим, что переход кластера c может сработать при некоторой маркировке. FC-свойство означает, что все переходы кластера c могут сработать при этой маркировке. Поэтому они конфликтны друг с другом. Назначение α определяет стратегию, при которой только переходам из множества α(c) разрешено срабатывать.

Для FC-СП, показанной на рис. 2.30, назначение α:CT задается следующим образом:

C={{s1,t1,t2},{s2,s4,t3,t5}}

α({s1,t1,t2})=t2

α({s2,s4,t3,t5})=t5

Места, содержащиеся в кластерах из множества C, заштрихованы, так же как и переходы.

Назначение множества кластеров C определяет множество путей, формируемых местами кластеров из C и назначенными переходами. Для заданного назначения α эти пути имеют вид: s1t2s2t5 и s4t5. Последовательности срабатываний, которые разрешают конфликт между переходами согласно стратегии, определенной назначением α, обеспечивают прохождние фишек вдоль этих путей. В таком случае будем говорить, что последовательности срабатываний согласуются с α.

Определение 38   Последовательность  σ  переходов согласуется с назначением  α:CTесли она не содержит таких переходов t, что  [t]C  и  tα(c).

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

Лемма 12   Пусть  αназначение живой FC-СП, имеющее непустую область определения C. Тогда при начальной маркировке разрешена последовательность срабатываний  σ  такая, что:

а)  σ  согласуется с  α,

б)  σ|α(C)бесконечная последовательность.

Доказательство. Определим индуктивно последовательности σ0, σ1, σ2, … такие, что Mi[σi>Mi+1 (i0), где M0 — начальная маркировка FC-СП. Для заданной Mi пусть τi — минимальная последовательность такая, что Mi[τi>Li и некоторый α-назначенный переход ti может сработать при Li. Определим последовательность σi=τiti. Поскольку FC-СП жива и C, то существует по крайней мере один α-назначенный переход. Таким образом, σi существует для каждого i  N.

В силу FC-свойства, переход кластера cC может сработать при маркировке M, если и только если назначенный переход α(c) может сработать при M. Так как последовательность τi минимальна, она не содержит α-назначенные переходы. Переход ti назначается. Таким образом, σi согласуется с α.

Определим σ как бесконечную последовательность σ1, σ2, σ3, ... . Так как каждая подпоследовательность σi согласуется с α, то σ согласуется с α. Более того, σ|α(C) — бесконечная последовательность, поскольку каждая подпоследовательность σi содержит переход из α(C).            □

На рис. 2.31 показано назначение множества кластеров C. Места, содержащиеся в кластерах из C, изображены двойными окружностями, а назначенные переходы — двойными барьерами. Для данного назначения возьмем σ=(t2t3t6t4t1)ω (σ0=t2, σ1=t3, σ2=t6, σ3=t4t1t2, ...).

Определение 39   Пусть R — множество мест сети. Определим  C={[t]|tR}(C — множество всех кластеров, содержащих по крайней мере одно место из R и по крайней мере один переход.) Назначение с областью определения C называется свободным от циклов для R, если никакой цикл сети не содержит только места из R и назначенные переходы.

Назначение, показанное на рис. 2.31, свободно от циклов.

Следующая лемма устанавливает, что существует свободное от циклов назначение для множества D. Более того, никакой назначенный переход не принадлежит множеству Q.

Лемма 13   Пусть N — FC-СП, R — множество мест сети N и Q — максимальная ловушка, содержащаяся в R (которая может быть пустым множеством). Пусть D = R\Q и  C={[t]|tD}Тогда существует назначение  α  с областью определения C, которое свободно от циклов для D и для которого верно, что  α(C)Q=.

Доказательство. Будем доказывать индукцией по |R|.

|R|=0. В качестве можно взять уникальное назначение с пустой областью определения.

|R|>0. Предположим, что R не является ловушкой, поскольку в противном случае верно, что D=. В качестве α можем взять уникальное назначение с пустой областью определения.

Так как R не является ловушкой, то существует переход tR такой, что tR. Определим множество R'=R\t. Поскольку tR, то имеем, что R'R. Поэтому можем применить индукционное предположение к R'.

Пусть Q' — максимальная ловушка, содержащаяся в R'. Пусть D' = R'\ Q' и C'={[u]|uD}. По индукционному предположению, существует назначение α':C'T, которое свободно от циклов для D' и для которого верно, что α'(C')Q'= (где T — множество переходов сети N). Определим α:CT следующим образом:

α(c)=α'(c),c[t],tc=[t].

Сначала покажем, что α определено корректно. Для этого докажем в три этапа, что каждый кластер из C, за исключением [t], содержится в области определения назначения α', что эквивалентно, CC'{[t]}.

1. Q'=Q.

Покажем, что Q — максимальная ловушка, содержащаяся в R'. Так как Q — ловушка и QR, то верно, что QQR. Поскольку tR, имеем, что tQ, Другими словами, никакое место из t не принадлежит Q. Поэтому верно, что QR'. Так как Q — максимальная ловушка, содержащаяся в R, то Q — также максимальная ловушка, содержащаяся в R'.

2. DD't

            D = R\Q

                (R't)\Q          (по определению R'), 

                (R'\Q)t

                = (R'\Q')t       (по п. 1),

                = D't       (по определению D'),

3. CC'{[t]}

           C = {[u]|uD}       (по определению C),

               {[u]|uD'(t)}          (по п. 2),

               = {[u]|uD'}[t]       (поскольку (t){[t]}),

               = C'{[t]}       (по определению C'),

4. α(C)α'(C'){t}

           α(C)α(C'{[t]})             (по п. 3),

                    = α((C'\{[t]}){[t]}),

                    = α(C'\{[t]})α([t]),

                    = α(C'\{[t]}){t}         (по определению α),

                    = α'(C'\{[t]}){t}          (по определению α'),

                    α'(C'){t}

5. α свободно от циклов для D. Предположим, что существует цикл γ, содержащийся в Dα(C). Согласно пп. 2 и 4, имеем следующее:

Dα(C)D'α'(C'){t}t.

По предположению индукции, D'α'(C') не содержит циклов. Таким образом, γ содержит элемент из множества {t}t. Поскольку верно, что {t}t[t], то γ содержит переход из [t]. Так как γ содержит только назначенные переходы, то он содержит t.

Все места, содержащиеся в γ, содержатся в R, по определению γ, и поскольку верно, что DR. Так как tR, то γ не содержит места из t, что противоречит предположению, что γ — цикл.

6. α(C)Q=

      α(C)Q(α'(C'){t})Q (по п. 4)

                         = ('(C')Q)({t})Q)

                         = ({t}Q) (по предположению индукции и п. 1),

                         = (поскольку tR и QR)                  □

Рассмотрим вторую часть теоремы Коммонера.

Теорема 26  Каждый тупик в живой FC-СП содержит изначально маркированную ловушку.

Доказательство. Пусть (N,M0) — живая FC-СП, R — тупик сети N и Q — максимальная ловушка, содержащаяся в R. Покажем, что Q изначально маркирована, т.е. M0(Q)>0.

Поскольку (N,M0) живая FC-СП, то, согласно утверждению 9, верно, что M0(R)>0. Определим множество D=R\Q. Если верно, что D=, то D — ловушка, содержащаяся в R. Поскольку Q максимальна, то имеем, что DQ. По определению множества D, верно, что D=. Тогда Q=R и M0(Q)=M0(R)>0.

Теперь рассмотрим случай, когда D. Определим множество C={[t]|tD}. Согласно лемме 13, существует назначение α с областью определения C, свободное от циклов для D и удовлетворяющее условию:

a) α(C)Q=

Тогда лемма 12 может быть применена к α. Значит, существует бесконечная последовательность срабатываний σ(M0[σ>) такая, что

б) σ согласуется с α, что, согласно определению C, означает A(σ)Dα(C).

в) σ|α(C) — бесконечная последовательность.

Неформально говоря, последовательность σ удаляет фишки из множества D.

Покажем справедливость следующих фактов.

1. A(σ)QQ.

(Q не может стать маркированным при последовательности срабатывания σ.) Имеем следующее:

    A(σ)QA(σ)R (поскольку QR),

                       A(σ)R (пoскольку R — тупик),

                       = A(σ)(QD) (пoскольку R=QD),

                       (A(σ)Q)α(C)) (по п. б)),

Согласно пункту а), верно, что (A(σ)Q)α(C)=. Следовательно, (A(σ)Q)A(σ)QQ.

2. Переход из Q содержится в σ. (Q становится маркированным при последовательности срабатывания σ.)

Определим отношение Δα(C)×α(C) следующим образом:

tΔt', если существует путь t...t' содержащий только узлы из множества Dα(C).

Таким образом, имеем, что tΔt', если t предшествует t' в некотором пути, определенном назначением α. Свойство свободы от циклов назначения α означает, что Δ — частичный порядок.

Согласно пункту в), множество α-назначенных переходов, содержащихся бесконечно часто в σ, не пусто. Пусть u — минимальный переход этого множества относительно отношения Δ. Далее, пусть s — место из множества uD (такое место существует, по определению C). Поскольку u содержится бесконечно часто в σ, некоторый переход vs содержится бесконечно часто в σ. Тогда имеем следующее:

             vD (поскольку s и sD),

               R (поскольку DR),

               R (пoскольку R — тупик),

               = QD (поскольку R=QD),

В силу минимальности перехода u, верно, что vα(C). По п. б), имеем, что vD. Следовательно, vQ.

В силу фактов 1 и 2, σ может быть разбита на части следующим образом: σ=σ1tσ2ct и A(σ1)(Qe)=. Пусть M0[σ1>M. Тогда верно, что M0(Q)=M(Q). Поскольку tQ может сработать при M, то M(Q)>0. Значит, имеем, что M0(Q)>0, и поэтому Q — изначально маркированная ловушка.                 □