Pnets_print

ících mó dů: hraniční, duplikovaný, vnitřn í, koncový. Konstru kce končí, poku d
ve stromě nejsou již žádn é hrani ční uzly.
vytvoř hran iční uzel oho dnocený markingem M0.
while existuj e hraniční uzel x do
if existuj e nehr aničn í uzel y takový, že Mx = My then
x se stává duplikovaným
elsei f v Mx nejsou uschop něny žádné přec hody then
x se stává koncovým
else
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
forall přechod t uschopn ěný v Mx do
přidej nový hran iční uzel z jako následn íka uzlu x
uzlu z přiřaď marking Mz defin ovaný následo vně:
forall p ∈ P do
if Mx(p) = ω then
Mz(p) = ω
elsei f
na cestě z kořene do x existuj e uzel y tak, že
∀q ∈ P : My(q) ≤ Mx(q) − F(q,t) + F(t,q) a
My(p) < Mx(p) − F(p,t) + F(t,p)
then
Mz(p) = ω
else
Mz(p) = Mx(p) − F(p,t) + F(t,p)
fi
done
x se stává vnitřn ím
done
fi
done
Poznámk a (Rozho dnutelnost problému pokryt elnosti)
Strom pokryteln osti umož ňuje rozho dovat pokry telnost a ohran ičenost sítě. Neumožň uje
však rozho dovat dosažiteln ost.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Příkl ad (Strom pokrytelnosti Petrih o sítě)
t1 p2 t3
p1 t2 p3
(1,0,0)
(1,ω,0) (0,1,1)
(1,ω,0) (0,ω,1) (0,0,1)
(0,ω,1)
t1 t2
t1 t2 t3
t3
Lemma (Nek oneč ná nekles ající podposloup nost)
Z libovolné nekonečné posloupnosti s = s1,s2,... prvků z a780∪{ω} lze vybr at nekoneč nou
neklesa jící podposlou pnost.
Důkaz: Poku d poslou pnost obsah uje nekonečnou podposloup nost prvků ω, pak je to
podposloup nost hledaných vlastností. V opačném případě po vynec hání všech prvků ω
dostan eme nekoneč nou posloupn ost přiroze ných číse l s nulou. Je-li tato neohr aničená,
pak obsah uje nekonečnou ostře rostoucí podposloupnost, kterou lze vyb rat i z původní
posloupnosti. Je-li ohraniče ná, pak obsah uje nějak é přirozené číslo nekonečněkr át a ne-
konečná podposloup nost tvořená tímto čísle m je podposloupnost hledaných vlastn ostí.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Lemma (Dic ksono vo lemma, Dickson’s Lemm a)
Z libovolné nekonečné poslou pnosti prvků z (a780 ∪ {ω})k, k ∈ a78, lze vybr at nekonečnou
(po složk ách) nekles ající podposloup nost.
Důkaz: Ind ukcí vzhl edem ke k. Pro k = 1 dle předc hozího lemm atu. Nec hť tvrzení platí
pro k, uvažuj me případ pro k + 1. Podle předc hozího lemmatu lze vyb rat nekoneč nou
neklesa jící podposloupnost podle složky k + 1. Nek onečnou nekles ající podposloup nost
(k+1)-tic z ní může me vyb rat podle indukčníh o předp oklad u, uvažujem e-li pouze prvn ích
k slož ek.
Věta (Uk ončení konstrukce strom u pokryteln osti)
Algor itmus konstrukce strom u pokryteln osti vytvoří konečný strom.
Důkaz: Protože počet přechodů Petriho sítě je z defin ice koneč ný, obsahuje strom pokry-
telnosti vždy jen konečné větvení. Poku d by měl být nekonečný, musel by obsaho vat
nekonečnou větev. Podle důkazu Dicksono va lemmatu však tato větev musí obsaho vat
buď opaku jící se uzly neb o ostře rostoucí podposloup nost. V prvn ím případ ě bude opaku -
jící se uzel označe n jako duplicitní, v druhém případě vznikne ω. V obou případ ech dojde
k ukončení větve.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Funkce,kterØnejsouprimitivnj236rekurzj237vnj237
Obarví me-li v klice K každou hranu náho dně jednou ze dvou barev, vznikne monochro-
matic ká klika K.
Definice (Rams eova funkce)
Funkce R : a78 → a78, kde R(m) = k, se nazýv á Ram seova, jestliže při náh odném obarvení
hran dvěma barvami v Kk vzni kne mon ochromatic ká klika Km.
Věta (Rams eova věta)
Rams eova funkce je defin ována pro každé m ∈ a78. Exi stuje limita Rams eovy funkce pro
m → ∞.
Důkaz: Není snadn ý a patří do kombinatori ky.
Definice (Hil bert-Ac kermann ova funkce)
Pro každé i ∈ a780 defi nujme indukt ivně funkci Ai : a780 → a780
A0(x) = 2x + 1
Ai+1 (0) = 1
Ai+1 (x + 1) = Ai(Ai+1 (x)) = Ai ◦ ···◦Aibracehtipupleft bracehtipdownrightbracehtipdownleft bracehtipupright
x-krát
(1)
Funkce Ai je primitiv ně rekur zivní pro každé i ∈ a780, ale počet for-c yklů potřebných pro
její výpočet roste s i. Funkce
A(x) = Ax(2)
tedy není primitivně rekur zivní. Důkaz patří do vyčíslitelnosti.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Sloj190itostkonstrukcestromupokrytelnosti
Věta (Velikost strom u pokryteln osti)
Velikost stromu pokryt elnosti Petri ho sítě nelz e ohraničit žádn ou primitivn ě rekur zivní
funkcí.
Důkaz: Pro každé i ∈ a780 sestro jíme Petri ho síť a její označ kování velikosti O(n) tak, aby
síť počítala Hilb ert-Ac kermann ovu funkci Ai. Petrih o sítě defi nujeme induktivn ě tak, že
každá bude obsahovat místa in, out a run. Vlo žíme- li m tokenů do in a jeden token do run,
bude existovat takový běh sítě, který skončí s Ai(m) tokeny v out .
Síť pro A0
in out
run
me mory
multipl y cop y
init
finish
Na počátku lze odpálit pouze přechod init, čímž se řídící token dostane do místa multipl y,
a do paměti me mory se vloží jeden token, což odpovídá přičtení jedničky. Dokud zůstává
řídící token v multipl y, je možné násobením dvěma přesouv at tokeny z in do me mory. Jak-
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
mile se provede přechod finish , token se do multipl y už nem ůže nevrátit, protože mís to run
je již prázdn é. Řídící token zůstává v místě cop y a přesunuje (kopíruje) tokeny z me mory
do out .
Síť pro Ai+1
in out
run
i-in i-out
i-run
cop y-in cop y-out
init
finish
me mory
Petrih o síť pro funkci Ai
Vložíme -li m tokenů do in a jeden token do run, výp očet, jehož výsledkem bud e Ai+1 (m)
tokenů v out , bude probíhat násle dovně. Nejprve se odpálí přechod init, čímž se do i-out
vloží jeden token (argu ment m slož ených funkcí Ai). Říd ící token potom zůstan e v cop y-in,
dok ud se nepřem ístí všechny tokeny z in do me mory.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Nyn í se m-krát spu stí síť pro Ai. Dok ud je v me mory ales poň jeden token, mohou se
přemístit tokeny z i-out do i-in. Potom se vloží jeden token do i-run a nechá se počítat síť
pro Ai tak, aby po skončení jejího výpočtu v i-out bylo Ai(x) tokenů, kde x byl počáteč ní
počet tokenů v i-in. Doku d jsou v me mory tokeny, postup se opakuj e.
Nak onec se odpálí přechod finish , čímž se řídící token dostane do cop y-out. To umož ní
přemístit všechny tokeny z i-out do out .
Pro velikost sítí (velikost grafů a velikost mar kingů ) se vstupem m platí
|NA0| = c + O(m)
|NAi+1 | = k + |NAi|
|NAi| = O(i + m)
Protože je síť ohran ičená, při konstrukci strom u pokryt elnosti nevznikne ω a je tedy
totožn ý se stromem dosažitelnosti. Do out se navíc tokeny přem ísťu jí po jednom, takž e
pro síť NAi existuj e ales poň Ai(m) markin gů dosažiteln ých z počátečníh o markingu s m
tokeny v in. Velikost stromu pokryteln osti sítě NAi je tedy zdola ohrani čena funkcí A(i),
tedy je rovna Ω(A(i+m)). Prot ože A(x) není primitiv ně rekur zívní, nelze velikost strom u
pokry telnosti ohran ičit žádnou primiti vně rekur zívní funkcí.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Hierarc hie probl émů vzhledem k redukci
Věta (Polynomiál ní ekvivalence reachab ility problémů)
Reachab ility, zero-reac hab ility, single- place zero-reac habil ity a sub-markin g reachabi lity
problém y jsou polynomiáln ě ekviv alentní.
Důkaz: Ukážeme následu jící redu kce:
singl e-pla ce zero-re achab ility reduku jeme na sub-marki ng reac habili ty (1)
sub -marki ng reac habil ity reduk ujeme na zero-reachab ility (2)
zero-r eachability redu kujeme na reachab ility (3)
reac habil ity redu kujeme na sub -marking reachabi lity (4)
zero-r eachability redu kujeme na single- place zero-reac hability (5)
Vznik nou tedy následující cykly redukcí: (1) → (2) → (5) a (2) → (3) → (4).
Redukce single -place zero-re achab ility na sub -marking reac habi lity Problém singl e-place
zero-r eachability je speciáln ím případ em sub -marking-reachab ility, reduk ce je triviáln í.
Redukce sub-ma rking reac hab ility na zero-reac hability Mějme instanci problém u sub-
marki ng reac hab ility, tedy Petri ho síť N , její počáteč ní označkování M0 a částeč né oz-
načkování M. Označm e p1,...,pn mís ta, na nichž je M defi nováno, a q1,...,qm místa
ostatní . Dále označme t1,...,tk všechny přec hody N . Vyt voříme síť N ′ a její počáteč ní
označ kování M′0 (instanci prob lému zero-reachab ility) následovně:
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
M(p1) tokenů M(pn) tokenů
p1 pn q1 qm
t1
tk
r1 rn
run
halt em pty
trash
··
·
··· ···
··· ···
Petrih o síť N s označ kováním M0
Doku d je řídící token v run, provádí síť N ′ výp očet sítě N . V určitém okamžiku se N ′
nedetermini sticky rozhodne provést přec hod halt a ověří se sho da označkování sítě N
se sub -markingem M. Nak onec se řídící token zahodí přechodem trash a výpočet končí.
Nul ový mark ing je v N ′ dosažiteln ý právě tehd y, pokud je v síti N dosažiteln ý sub-
marki ng M. Jinak by nutně zůstaly tokeny buď v ri neb o pi podle toho, kde by jich bylo
více v okamžiku provedení halt.
Redukce zero-reachability na reac hability Problém zero-reac habil ity je speciálním pří-
pad em reac habil ity, redukce je trivi ální .
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Redukce reachability na sub -marking reachab ility Problém reac hab ility je speciáln ím
případ em sub-marki ng reac habili ty, redu kce je trivi ální .
Redukce zero-reachabili ty na single -place zero-reac habi lity Mějme instan ci problému
zero-r eachability, tedy Petrih o síť N = (P,T,F) a její ozna čkování M0. Nec hť T =
{t1,...,tn}. Defin ujme dále funkci f : T → a780 předpisem
f(t) =
summationdisplay
p∈P
parenleftbig
F(t,p) − F(p,t)
parenrightbig
Funkce f udává efekt přechodu na celkový počet tokenů v síti. Instan ci prob lému single-
place zero-reac hab ility N ′, M′0, p, p negationslash∈ P vytvoříme takto:
p, M′0(p) = |M0|
t1
tn
Petrih o síť N s počáte čním marki ngem M0
··
·
f(t) hran z t do p, je-li f(t) ≥ 0
−f(t) hran z p do t, je-li f(t) < 0
Místo p slouží jako počítad lo tokenů v síti N . Síť N ′ je ekvivalen tní síti N , ale navíc v p
udržuj e počet tokenů ve zbylé části sítě. Pokud ve zbylé části (v síti N ) nejsou žád né
tokeny, je i místo p prázdné.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Věta (Živ ost sítě a single- place zero-reac habil ity)
Problém sing le-place zero-reachab ility je polynomiáln ě redu kovatelný na problém živosti
sítě .
Důkaz: Nec hť Petri ho síť N = (P,T,F), označ kování M0 a p ∈ P tvoří instanci probl ému
single-place zero-reac habil ity. Označm e t1,...,tm všechny přechody sítě N a p1,...,pn
všechna místa sítě N kromě místa p. Instanci N ′, M0 problému živosti sítě vytvoříme
tak, že z místa p přidáme run-p lace hranu do všec h přechodů sítě N a dále přechody
keep, em it a místo store podle obrázku.
t1
tm
p p1 pn
keep store em it
··
· ···
Petrih o síť N s počáte čním markin gem M0
Každý výp očet sítě N lze provést i v N ′. Pokud se zejména může vypr ázdnit místo p
v N (je dosažiteln ý příslušn ý mark ing), může se vypr ázdnit i v N ′ a síť se zasta ví kvů li
run-pl ace hran ám — tedy není živá. Poku d se místo p naop ak vyp rázdn it nem ůže, vždy
lze provést přec hod keep, který umístí token do místa store. Je-li v místě store ales poň
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
jeden token, lze libovolně provádět přec hod em it a připravit tak libovolný přec hod v N ′
— síť je tedy živá.
Poznámk a (Ostatn í varian ty živosti a single-place zero-reac habili ty)
Problém single-place zero-reac hab ility lze analogic ky polynomiáln ě redu kovat na prob-
lémy neživosti sítě, živosti přec hodu i než ivosti přechodu. Živost přechodu je speciální
případ živosti sítě, lze použít toto žnou redu kci. Při redukci na neživost sítě by konstrukce
byla také totožná, změ nila by se jen interpretace výsledků : poku d instance nesplňuje
single-place zero-reachability, redukcí vznikne než ivá síť; poku d instan ce splň uje single-
place zero-reac hab ility, redu kcí vznikne síť, která nebu de neživá.
Věta (Živ ost přec hodu a dosažiteln ost)
Problém živosti přechodu je redukovateln ý (v Turingově smyslu — Turingo vým stro jem
s orákul em) na problém dosažitelnosti.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Min ského stro j
Definice (Mi nského stroj)
Minského stroj je poslou pnost instrukcí
l1 : Com 1
..
.
..
.
lm : Com m
lm+1 : halt
kde každá instru kce Com i je typu I
li: inc cj
neb o typu II
li: if cj = 0
then goto lk
else dec cj; goto ln
kde cj ∈ a780, j ∈ {1,2}, jsou dva neomez ené nezáp orné celočíse lné registr y.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Ekvivalen ce přechodových syst émů
V této části se budem e zabývat ekvi valence mi přec hodových systé mů s návěštími, které
jsou indukovány Petrih o sítěmi — defin ujeme několik typů ekvivalencí a ukážeme některé
vztah y mezi nimi.
Definice (Stopy stavu, trace- ekvi valence)
Nec hť T = (S,A,→) je přec hodový systém . Funkci Traces : S → A∗ defin ujeme před-
pisem
Traces (s) = {w ∈ A∗ | ∃s′ : s w→ s′}
Trace-ekvival enci =tr⊆ S × S defin ujeme předpi sem
s =tr t def⇐⇒ Traces(s) = Trace s(q)
Definice (Bisim ulace , bisimulační ekvivalence )
Nec hť T = (S,A,→) je přechodový systé m. Relaci R ⊆ S×S nazv eme (silnou ) bisimul ací,
jestliže pro všechna (s,t) ∈ R platí
(∀a ∈ A)(∀s′,s a→ s′)(∃t′,t a→ t′) : (s′,t′) ∈ R
(∀a ∈ A)(∀t′,t a→ t′)(∃s′,s a→ s′) : (s′,t′) ∈ R
Nejv ětší relaci bisim ulace ∼⊆ S × S (tak ová zřejmě existuj e) nazv eme bisi mul ační ekvi -
valencí . Zřejmě s ∼ t právě tehdy , když existuj e bisimulace R taková, že (s,t) ∈ R.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Poznámk a (Vztah bisimulační ekvivalence a trace -ekviv alence)
Pro každý přechodový systém T = (S,A,→) a každé dva jeho stavy s,t ∈ S zřejmě platí
s ∼ t ⇒ s =tr t
Opačná imp likace obecně neplatí. Uvažme například přechodový systém na obrázku,
který je složen ze dvou částí. Zřejmě s1 =tr s′1, ale s′2 negationslash=tr s2 ani s′2 negationslash=tr s3, takže trace-
ekviv alence není bisim ulací.
s1
s2
s3
s4
s5
a
a
b
c
s′1 s′2 s′3
a b
c
Takový přechodový systém je součas tí přechodového systém u generovaného Petriho sítí
na násle dujícím obrázku, kde stavu s1 odpovídá označ kování ozn ačkování M1 a stavu s′1
označ kování M′1 dané předp isem
M1(p) =
braceleftbigg
1 p = p1
0 jinak
M′1(p) =
braceleftbigg
1 p = p1 ∨ p = p2
0 jinak
p1 a
a
a
p2
p3
p4
p5 bc
bc
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Věta (Nerozho dnutelnost ekvi valencí)
Nec hť T = (S,A,→) je přec hodový systém indukovaný Petri ho sítí N , ≈⊆ S × S relace
taková, že ∼⊆≈ ⊆=tr. Problém, zda dvě daná označ kování M1 a M2 (sta vy přechodového
systém u) splňují M1 ≈ M2 je nerozho dnutelný.
Důkaz: Redukcí (nerozho dnutelného) probl ému zasta vení Minského stro je. Pro daný Min-
ského stro j M sestro jíme Petri ho síť N , její olab elování a dvě označ kování M1 a M2 tak,
že
M nezas taví ⇒ M1 ∼ M2 ⇒ M1 ≈ M2
M zastaví ⇒ M1 negationslash=tr M2 ⇒ M1 negationslash≈ M2
Nec hť je tedy dán Minsk ého stroj M. Petrih o síť definujeme po instru kcích následovně.
si cj
sk
i
instrukce li: inc cj; goto lk
si cj
sn sk p1 p2
di zi zi zi
instrukce li: if cj = 0 then goto lk else dec cj ; goto ln
si h p1
instrukce li: halt
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Položme
M1(p) =
braceleftbigg
1 p = s1 ∨ p = p1
0 jinak
M2(p) =
braceleftbigg
1 p = s1 ∨ p = p2
0 jinak
V takto definované síti odpovídá korektní mu výpočtu právě jeden běh. Ostatní běhy jsou
nekorektn í v tom smyslu, že některý přechod zi byl proveden v okamžiku , kdy příslušný
cj nebyl nulový.
Nec hť M nezas taví, nikdy se tedy nepr ovede instru kce halt. Ani při jednom iniciálním
označ kování se tedy v korektn ím běhu nem ůže provést přec hod h. Ostatní běhy ob-
sahují alespoň jeden nekorektn í krok. Uvažme libovolný nekorektní běh z počáteč ního
označ kování M1 a v něm prvn í nekorektn í krok zi. Z mark ingu M2 lze přesně simulo-
vat tento běh až k prvnímu nekorektní mu krok u. Místo něj (protož e příslu šné M1(cj) =
M2(cj) negationslash= 0) lze provést jiný přechod zi, kterým se přemístí token z p2 do p1 a síť se
dostan e do iden tického stavu jako v simulovaném běhu. Syme tricky pro simulování běhů
z M2 běhy z M1.
Nec hť M zastaví. V korektn ím běhu z počátečníh o označkování M1 je posledním přecho-
dem přechod h. Při simulaci tohto běhu z počáte čního označ kování M2 musí síť provádět
pouze korektn í krok y, jinak by provedla přechod zi mís to di. Místo p1 bude tedy stále
prázdné a přechod h se proto nepro vede. Z toho Trace s(M1) negationslash= Trace s(M2).
Věta (Nerozho dnutelnost inklu ze a rovnosti množin dosažiteln ých označkování)
Problém inkluze a rovnosti množin dosažiteln ých označ kování je nerozhodnuteln ý.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Důkaz: Reduk cí problému zasta vení Minského stroje. Pro daný Misk ého stro j M sestro-
jíme Petriho sítě N1 a N2 a označ kování M1 a M2 tak, aby následu jící podmínky byly
ekviv alentní
M nezas taví (a)
Reac h(N1,M1) = Reach(N2,M2) (b)
Reac h(N1,M1) ⊆ Reac h(N2,M2) (c)
Tvrzení dokážem e pomo cí tří impl ikací, přičemž (b) ⇒ (c) platí vždy.
(a) ⇒ (b) ⇒ (c) ⇒ (a)
Pro důkaz (a) ⇒ (b) reduku jme M podob ně jako v důkazu předc hozího tvrzení po in-
struk cích. Vytv ořme tedy sítě N1 a N2 a označkování M1 a M2. I když v tom to případ ě
není olab elování přec hodů podstatn é, zavedeme jej pro snazší vyjadřování. Čás ti odpoví-
dající instrukcím typu I a II jsou stejn é v obou sítích:
si cj
sk
i
instrukce li: inc cj; goto lk
si cj
sk p1 p2 sn
tzi di tnzi
instrukce li: if cj = 0 then goto lk else dec cj ; goto ln
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Instru kce li: halt se do sítě N1 zakóduje jinak než do N2.
si
ta tb
p1 p2
instrukce li: halt v síti N1
si
ta
instrukce li: halt v síti N2
Označ kování defin ujme takto (množiny mís t jsou stejn é v obou sítích):
M1(p) = M2(p) =
braceleftbigg
1 p = s1 ∨ p = p1
0 jinak
Jedin ý rozdíl mezi sítěmi N1 a N2 je přechod tb. Proto
Reac h(N2,M2) ⊆ Reac h(N1,M1)
zřejmě platí. Nec hť M ∈ Reac h(N1,M1). Ukážeme, že potom také M ∈ Reac h(N2,M2).
Roz liším e dva pířpad y.
Poku d lze v N1 dosáh nout M posloupn ostí přechodů, která neobsahuje přechod tb, lze
tutéž posloup nost provést v síti N2 a dosáhn out téhož označ kování.
Naopa k, nechť M lze v N1 dosáhnou t pouze takovými posloup nostmi přechodů, které
obsah ují přechod tb (a tento přechod je tam nejvý še jedn ou, protože se token přesune
z p1 do p2). Protož e podle (a) stroj M nezas taví, musela síť N1 ales poň jednou provést
tzi místo tnzi (nekorektn í krok). Přechod di to být nemohl , protož e pak by nebylo mož né
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
provést tb — v p1 už by nebyl token. Síť N2 mís to jedn oho takové přechodu moh la provést
přechod di a dále se opět chovat jako N1. Prot ože je v N2 již token z p1 přesunut do p2,
může N2 provést přec hod ta mís to tb v síti N1 a dostat se tak do téhož označ kování.
Místo impl ikace (c) ⇒ (a) dokážeme její obmě nu ¬(a) ⇒ ¬(c). Sítě N1 a N2 z důkazu
impl ikace (a) ⇒ (b) mo difikujeme tak, aby síť N1 po proveden í nekorektn ího kroku
výp očtu již nemohla dosáhnout označ kování odpovídajícího korektn ímu výpočtu. Každý
přechod sítí N1 a N2 kromě ta a tb mo difiku jeme podle následu jícíh o obrázku . Přitom
přechod t dává token do místa cod (přerušo vaná šipka) právě tehdy, když t = tnzi pro
něja ké i. Mo difikované sítě označm e N ′1 a N ′2. Mo difikovaná počáteč ní označ kování M′1
a M′2 jsou totožn á s M1 a M2 až na přidaný token do místa r1.
t
u1 u2
u3
r1 r2
cod
aux
sc
Petrih o síť N1 neb o N2
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
V bězích, které maximalizují počet tokenů v cod, dochází v přidané podsíti k následujícím