- Stahuj zápisky z přednášek a ostatní studijní materiály
- Zapisuj si jen kvalitní vyučující (obsáhlá databáze referencí)
- Nastav si své předměty a buď stále v obraze
- Zapoj se svojí aktivitou do soutěže o ceny
- Založ si svůj profil, aby tě tví spolužáci mohli najít
- Najdi své přátele podle místa kde bydlíš nebo školy kterou studuješ
- Diskutuj ve skupinách o tématech, které tě zajímají
Studijní materiály
Zjednodušená ukázka:
Stáhnout celý tento materiáloperacím. Pro každý přechod původní sítě, který je různý od tnzi pro všechna i, je počet
tokenů v cod zdvojnásob en. Provede-li se v původní síti přechod tnzi pro nějaké i, pak
je nejp rve jeden token do cod přidán a potom je počet zdvojnásoben. Binár ní zápis
počtu tokenů v cod tedy udává, kdy byl v poslou pnosti přec hodů původní sítě proveden
přechod tnzi pro nějak é i (a to od prvního provedení takového přechodu).
Ukážeme, že existuje označ kování M takové, že platí M ∈ Reach(N ′1,M1) a zároveň
M negationslash∈ Reach(N ′2,M2). Nec hť označkování M odpovídá korektn ímu výpočtu sítě N′1, který
maximalizuj e počet tokenů v cod, po provedení přechodu tb. Zejména tedy platí M(p1) =
0 a M(p2) = 1. Aby se síť N ′2 mohla dostat do takového označkování, musela někde
provést přechod di. Ukážeme, že po provedení takového přec hodu se již nikdy nedostane
do označ kování odpovídajícího korektn ímu výp očtu.
Síť N ′2 musela přechod di provést místo nějak ého přechodu tnzi sítě N ′1. Místo přec hodu tzi
to nebylo možné, protože uvažujeme korektní výp očet sítě N ′1 — přechod tzi se provádí
pouze v případě, že je příslušné mís to cj prázdné. Zatímc o se tedy v N ′1 přidá do cod
token a potom se jejich počet vynásobí dvěma, v síti N ′2 dojde pouze k vyn ásobení dvěma.
Poku d toto nenastane při prvním provedení některého z přechodů tnzi v síti N ′1, počty
tokenů v cod se již nikdy nebu dou shodovat — zřejmé z významu jejic h binární ho zápi su.
Poku d to ovšem nastane při prvn ím proveden í některého ze všec h tnzi , pak by se ještě
počty tokenů sho dovat mohly, protože místo cod sítě N ′2 zůstá vá prázdn é. Síť N ′2 tak může
provést ještě nějak é výp očty neobsahující žádný přechod tnzi a potom přesně simulovat
výsky ty ne nutn ě stejných přechodů tnzi . V takovém případě se ovšem budou ales poň o
jedn a lišit počty v mís tě sc — síť N2 musela provést alespoň přechod di navíc.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Mo del-checking Petri ho sítí
Násle dující obráze k znázorň uje hierarchii jedn otliv ých fragme ntů temp oráln ích logi k vzh-
ledem k vyjadřovací síle.
lineární µ-kalku l
LTL
LTL U
LTL F LTL G
µ-kalku l
CTL ∗
CTL
CB
EF EG
H.M . logik a
Ukážeme nerozho dnutelnost mo del-c heckingu pro LTL F a EG a EF fragme nty CT L, z če-
hož bude plynou t nerozhodnuteln ost všech logik silnějšíc h než některý z těchto fragme ntů.
Mo del-c hecking pro LTL G a H.M. logiku je rozho dnutelný.
Poznámk a (Logik y LTL F a LTL G)
Fragme nt LTL F obsah uje pouze tem porální operátor F a negac e je omezena pouze na
atomic ké prop ozic e. Fragm ent LTL G má podobn ě omezenou negac i, z operátorů obsahuje
pouze G. Temp orální operátory F a G jsou duální , negace proto musí být ome zena, aby
fragme nt neobsahoval oba tyto operátor y.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Poznámk a (Séman tika temp orální ch logik pro Petrih o sítě)
Séman tika je defin ována nad přechodovým systém em indukovaným Petriho sítí N =
(P,T,F) a jejím počátečním označkováním M0. Protože u state-base d logik , kterými se
budeme zabývat, nezálež í na návěštích přechodů, jsou všechny indukované přechodové
systém y z pohledu temp orální ch logi k totož né.
Séman tiku atomic kých propozic a jejic h valuaci je pro mo del-checking Petrih o sítí nutno
ome zit, jinak by pomo cí vhodně zvolené valuace atomic kých prop ozic moh l být neroz hod-
nutelný i model-c hecking pouze jediné atomic ké prop ozice. Přirozené ome zení je násle-
dující. Ke každém u místu s Petrih o sítě zvolíme (jedinečnou) atomic kou prop ozic i ps.
Valuaci, vzhledem k níž se definuje séman tika logik, defin ujeme pro atomic kou prop ozici
p a stav přechodového systém u (označ kování) M takt o
M ∈ ν(p) def⇐⇒ ∃s ∈ P : p = ps ∧ M(s) > 0
Připomeňme jen, že platn ost atomic ké prop ozic e p pro běh α (logi ky lineárního času),
resp. ve stavu M (logi ky větvícího se času) je defin ována vztah y
α |= p def⇐⇒ α(0) ∈ ν(p) (LTL)
M |= p def⇐⇒ M ∈ ν(p) (CTL)
kde α(0) je počáteční stav běhu α a ν je funkce přiřazující atomic kým prop ozicím množin u
stavů, v nichž plat í.
Je-li séman tika defino vána uveden ým způsobem a platí -li formule ¬ps ve stavu M, zna-
mená to, že M(s) = 0.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Věta (Nerozho dnutelnost LTLF)
Mo del-c hecking LTL F vlastn ostí je pro Petriho sítě nerozhodnuteln ý.
Důkaz: Redukcí problém u zasta vení Minsk ého stroje. Kon strukce Petrih o sítě N a jejíh o
počátečníh o marki ngu M0 bude podob ná jako v předchozíc h případec h — tran sformace
jedn otlivých instrukcí je na následu jícím obrázku. Počáteční marking bude mít pouze
jeden token v mís tě s1.
si cj
sk
i
instrukce li: inc cj; goto lk
si
s′k
sk
cj
sn
li: if cj = 0 then goto lk else dec cj ; goto ln
si = halt
li: halt
Instru kce halt byla mo difikována tak, aby korektn í běh systé mu byl nekonečný. Do sítě
byly přidány stavy s′k, aby bylo mož né LTL formulí rozpoznat běhy, které neodpovída jí
korektn ímu výpočtu simulovaného Minsk ého stro je. Tato form ule, označme ji ψ, má tvar
ψ ≡
logicalordisplay
instr ukce typu 2
(pcj ∧ p′ki)
Defin ujme nyní form uli ϕ takto
ϕ ≡ F(phalt ∨ ψ)
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Pro každý běh α začínající v M0 platí α |= ϕ právě tehdy , když simulovaný Minského
stro j zasta ví. Mo del-c hecking této vlastnosti je tedy neroz hodnuteln ý.
Věta (Nerozho dnutelnost EG-fragmen tu CTL)
Mo del-c hecking vlastn ostí EG-frag mentu CTL je pro Petrih o sítě nerozho dnutelný.
Důkaz: EG-fra gment CTL obsah uje duální operát or AF, je tedy nerozho dnutelný ze stej-
ného důvodu jako LTL F.
Věta (Nerozho dnutelnost EF-fragm entu CTL)
Mo del-c hecking vlastn ostí EF-fragmen tu CTL je pro Petrih o sítě nerozho dnutelný.
Důkaz: Důkaz provedeme redu kcí prob lému inkluze množin dosažiteln ých označ kování.
Pro dan é sítě N1 = (P,T1,F1) a N2 = (P,T2,F2) a jejich počáteční označkování M1
a M2 defin ujeme síť N s počáte čním označkováním M0 a vlastnost ϕ EF-fragmen tu
CTL tak, aby M0 |= ϕ právě tehdy, kdy ž Reach(N1,M1) ⊆ Reach(N2,M2). Nechť T1 =
{u1,...,um}, T2 = {v1,...,vn} a P = {s1,...,sl}. Konstr ukce N a defin ice M0 je
znázorněna na následujícím obrázku.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
u1 um v1 vn
t1 tl
s1 sl ¯s1 ¯sl
r1 r r2
em pty
··· ···
···
··· ···
N1, M1 N2, M2
Sítě N1 a N2 byly spojeny pomocí čtyř run-place míst r1, r, r2 a em pty. Dok ud je řídící
token v r1, počítá N1. Jakmile se řídící token přemístí do r, síť N1 už nebude moci
provést žádný přechod. Místo r je přidán o z jedi ného důvodu — aby bylo mož no form ulí
určit okamž ik, kdy přestala počítat N1 a začne počítat N2. Z mís ta r se token musí
okamž itě přesunou t do r2, čímž se umož ní běh sítě N2, která se „snažícsquotedblright dostat do stejného
označ kování, v jakém se nachází N1. Ve vhodném okamžiku se řídící token přesune do
em pty, v něm ž se srovnají označ kování sítí N1 a N2. Protože v logice je k dispozic i pouze
test na prázdnost místa, umožň uje konstru kce vyp rázdni t všechna místa s1,...,sl právě
tehd y, pokud jsou označkování totož ná.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Pro form uli ϕ,
ϕ ≡ AG
parenleftbig
pr ⇒ EF(
llogicalanddisplay
i=1
(¬si ∧ ¬¯si)
parenrightbig
platí M0 |= ϕ právě tehdy , když Reac h(N1,M1) ⊆ Reach(N2,M2).
Poznámk a (EF-fragm ent CT L bez zanoření tem porál ních operátorů)
Form ule ϕ z předc hozíh o důkazu má zanoř ené temp orální operátor y. Vlas tnosti EF-
fragme ntu CTL bez zanořen ých temp orální ch operátor ů jsou pro Petrih o sítě rozhod-
nutelné.
Poznámk a („Action -basedcsquotedblright logik y)
V předchozí části jsm e se zabývali tzv. state-base d logik ami. Pro action-base d logi ky,
v nichž sém antika není defin ována nad stavy, ale nad návěštími přechodů, jsou výsle dky
podob né s výjimkou LTL, která je pro action -based logik y rozho dnutelná.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Klas ické techniky analýzy Petrih o sítí
Poznámk a (Omez ení pro klasic ké techniky anal ýzy)
Pro účely této kapitol y se omez íme pouze na sítě bez násobn ých hran a se slab ě souvi slým
graf em. Ve všech dalšíc h definicíc h a tvrze ních budeme tedy předp oklád at, že Petri ho síť
N = (P,T,F) splňuje
F : P × T ∪ T × P → {0,1}
a má slab ě, tj. bez ohledu na orientaci hran, souv islý graf.
Definice (Incid enční matice)
Nec hť N = (P,T,F) je Petrih o síť. Inci den ční maticí N : P × T → {−1,0,1} rozumíme
funkci udávající efekt přechodu t ∈ T na místo p ∈ P, tj. danou vztahem
N(p,t) = F(t,p) − F(p,t)
Definice (Kr onec kerovo delta)
Pro snadnější zápis některých vztahů je vhodné závést tzv. Kroneckerovo delta, funkci
defin ovanou vztahem
δij =
braceleftbigg
1 pro i = j
0 jinak
Poznámk a (Notace vektorů , označkování jako vektory)
Tato kapitola využív á apar át lineárn í algebry. Bud eme použív at následu jící konvence.
Vektor y budeme cháp at jako sloupcové matice, které budeme často zapisovat parametri -
zovaně vectoru = (ui)ni=1 . Označkování budeme formálně chápat jako vektory M = (M(p))p∈P ,
kde P je množina mís t.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Příkl ad (Incid enční matice)
p1
p2
p3
p4
p5
t1 t2
t3
t4
t5
Pro síť z předc hozího obrázku má incidenční matice tvar
t1 t2 t3 t4 t5
s1 1 −1 0 0 0
s2 −1 1 0 0 0
s3 0 1 −1 0 1
s4 0 0 1 −1 −1
s5 0 −1 0 1 0
Poku d N(p,t) = 0, neznamená to, že by mezi p a t nevedla žádn á hran a, ale že počet
hran z místa p do přechodu t je roven počtu hran z t do p. Prot ože uvažujem e pouze sítě
bez násobn ých hran, může tento počet být buď 0 neb o 1.
Nec hť ti ∈ T je připraven při označkování M. Všim něme si, že platí
M ti→ M′ ⇔ M′ = M + N · (δij)nj=1
Definice (Parikův obraz)
Buď N = (P,T,F) Petriho síť, kde T = {t1,...,tn}. Nechť σ ∈ T∗ je posloup nost
přechodů. Parikový m obrazem posloupnosti σ rozumíme vektor
vectorσ = (σ1,...,σn)T
kde σi je počet výskytů ti v σ.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Věta (Nu tná podmín ka dosažiteln osti)
Nec hť N = (P,T,F) je Petrih o síť s incid enční maticí N. Nechť označ kování M′ je
dosažitelné z M, M σ→ M′, kde σ ∈ T∗. Potom existuje řešení rovnice
M′ = M + NX
a řešením je i vectorσ.
Důkaz: Nec hť T = {t1,...,tn}. Ukážem e-li, že vectorσ je řešením uvedené rovnice, bude tím
záro veň dokázána i existence řešení. Ind ukcí vzhl edem k délce posloupnosti přechodů σ.
Pro σ = ε je vectorσ = 0, tedy Nvectorσ = 0 a skuteč ně M′ = M.
Uvažm e nyní M σ→ M′ ti→ M′′ a označme ̺ = σti. Tedy vector̺ = vectorσ + (δij)nj=1 . Z indukčního
předpokladu platí M′ = M + Nvectorσ. Efekt přechodu ti na označkování M′ je určen vek-
torem (N(p,ti))p∈P = N · (δij)nj=1 . Celkem platí
M′′ = M′ + N · (δij)nj=1
= M + Nvectorσ + N · (δij)nj=1
= M + N ·
parenleftbig
vectorσ + (δij)nj=1
parenrightbig
= M + Nvector̺
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
S-invarianty
Příkl ad (Mot ivace pro S-invarian ty)
S-in varian ty jsou vlastně globál ní vlastnosti sítí. Neformálně se jedná o vektor určující
váhy jednotl ivýc h míst tak, aby vážené součty označ kování dosaž itelných z dan ého ini-
ciální ho mark ingu byly stejné. Písmeno „Scsquotedblright značí, že S-invarianty vypovídají o stavech
(z něme ckého die Stel le). Pro síť na následu jícím obrázku jsou S-invarianty napří klad
vektory (1,1,2)T, (1,0,1)T, (0,1,1)T, (0,0,0)T.
s1 s2
s3
t1
t2
Přitom nulový vektor je S-in variantem pro každou síť. Povolíme -li jako váhy (koeficien ty)
racion ální čísla neb o libovolné jiné pole a80, budou S-in varian ty sítě s n mís ty tvořit vek-
toro vý podprostor a80n — jsou uzavřen y na násobení skalárem i součet.
Uvedená intuiti vní definice nevyp ovídá nic o tom, jak S-in varianty vytvořit pro dan ou
síť. Proto se definují jinak.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Definice (S-invarian t)
Nec hť N = (P,T,F) je Petri ho síť s incidenční maticí N. Vektor I ∈ a81|P| nazv eme
S-invari ant, jestliže I je řešením rovnice
XT · N = 0T
Příkl ad (Určení S-in varian tů)
Mějme (mrt vou) síť danou násle dujícím obrázk em
s1
s2
Incid enční matice této sítě je N = (0,−1)T. S-in varian ty jsou tedy řešením rovnice
(x1,x2)
parenleftbigg
0
−1
parenrightbigg
= (0,0)
−x2 = 0
x2 = 0
I ∈ {(k,0)T | k ∈ a81}
Vzhledem k intuiti vní defin ici S-in variantů by však každý vektor I ∈ a812 měl být S-
invariantem, protože síť je mrtvá — má pouze jedin é dosažite lné označ kování. Formální
defin ice nep okrýv á všechny S-invarian ty podle intuiti vní definice . Řeš ení rovnice z for-
mální defin ice totiž nejsou na rozdíl od intuitivn í definice závislá na iniciáln ím markin gu
— jsou to S-invarianty pro každé počáteč ní označ kování. Om ezením se na konk rétní ini-
ciální označkování a mark ingy z něj dosažitelné, se množina uvažovaných označ kování
zmenší a proto se může zvětšit množina S-in variantů.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Věta (Alt ernativ ní defin ice S-in varian tů)
Nec hť N = (P,T,F) je Petriho síť. Vektor I ∈ a81|P| je S-invarian t sítě N právě tehd y,
když ∀t ∈ T platí summationdisplay
s∈ •t
I(s) =
summationdisplay
s∈t•
I(s)
kde I(s) je složka vektor u I pro místo s, tj. žádný přechod nez mění vážený součet oz-
načkování.
Důkaz: Nec hť I je řešením rovnice XTN = 0T, kde N je incidenční matice sítě N . Označme
vectortj j-tý sloup ec N. Vektor I je S-invarian t právě tehd y, když ITvectortj = 0 pro každé j.
Roz epišme levou stran u rovnosti. Nec hť |P| = m.
ITvectortj =
msummationdisplay
i=1
I(si)N(si,tj) =
msummationdisplay
i=1
I(si)
parenleftbig
F(tj,si) − F(si,tj)
parenrightbig
=
msummationdisplay
i=1
I(si)F(tj,si) −
msummationdisplay
i=1
I(si)F(si,tj)
Protože síť podle předpokladů neobsah uje násobn é hrany, pro všechna i platí F(tj,si) ∈
{0,1} a F(si,tj) ∈ {0,1}, přičemž
F(tj,si) = 1 ⇔ si ∈ t•
F(si,tj) = 1 ⇔ si ∈ •t
odkud
msummationdisplay
i=1
I(si)F(tj,si) =
summationdisplay
s∈t•j
I(s)
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
msummationdisplay
i=1
I(si)F(si,tj) =
summationdisplay
s∈ •t j
I(s)
Celkem dostá váme pro každé tj ∈ T
0 = ITvectortj =
summationdisplay
s∈t•j
I(s) −
summationdisplay
s∈ •t j
I(s)
Vektor I je tedy S-in variant právě tehd y, když pro všechna tj ∈ T platí
summationdisplay
s∈ •t j
I(s) =
summationdisplay
s∈t•j
I(s)
Věta (Alt ernativ ní nutná podmín ka dosažiteln osti)
Pro Petrih o síť N = (P,T,F) s iniciáln ím markingem M0 a incidenční maticí N jsou
následu jící podmín ky ekvivalen tní
pro každý S-invariant I platí ITM0 = ITM (a)
rovnice M0 + NX = M má řešení v a81 (b)
Důkaz: (b) ⇒ (a) Nechť I je libovolný S-invarian t sítě N , tedy platí ITN = 0T. Tedy
M = M0 + NX
ITM = IT(M0 + NX) = ITM0 + ITNX = ITM0 + 0TX
ITM = ITM0
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
(a) ⇒ (b) S-invarianty jsou řeše ním rovnice XTN = 0T. Nechť I1,...,In je báze prostoru
řešení této rovnice. Pokud n = 0, nee xistuje žádn ý S-invariant a impl ikace platí triviál ně.
Nec hť tedy n > 0.
Označme A = (ITi )ni=1 matici, jejíž řádky tvoří jedn otliv é bázo vé S-in varianty. Tedy
platí A · N = 0 a sloup ce matice N generuj í prostor řešení rovnice
AX = 0
Je-li totiž m velikost nejv ětší lineárn ě nezávislé množin y tvořené slou pci N, potom n =
|P| − m. Protože řádk y matic e A jsou tvořen y bází, jsou lineárn ě nezávislé a dimenze
prostoru řešení rovnice AX = 0 je |P|− n = m. Přitom každý sloupec N je řešením a je
mezi nimi m lineárně nez ávislýc h — báze prostoru řešení.
Podle (a) pro všechna i, 1 ≤ i ≤ n, platí
ITi M0 = ITi M
ITi (M0 − M) = 0
A(M − M0) = 0
Vektor M − M0 je tedy řeše ním rovnice AX = 0 a lze jej proto vyjád řit jako lineárn í
kombinace slou pců N, které tento prostor generují. Pro vhodné R tedy platí
M − M0 = NR ⇒ M = M0 + NR
Posledn í rovnost lze chápat i tak, že R je řešením rovnice
M = M0 + NX
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Definice (Semip ozitivn í a pozitivn í S-in varianty)
S-in varian t I sítě N = (P,T,F) se nazýv á semi pozitivní , jestliže I(s) ≥ 0 pro všec hna
s ∈ P a existuje s0 ∈ P takové, že I(s0) > 0. S-in variant I se nazýv á pozitivní , jestliže
I(s) > 0 pro všec hna s ∈ P.
Věta (Nu tná podmín ka živosti sítě)
Nec hť N = (P,T,F) je Petrih o síť s počátečním označ kováním M0. Je-li (N,M0) živá,
pak pro každý semip ozitivní S-invariant I platí
ITM0 > 0
Důkaz: Síť N je živá, jestliže pro každý dosaž itelný mark ing M a každ ý přechod t ∈ T
existuj e mar king M′ dosažiteln ý z M, v němž je t uschopn ěný. Před pokládejme nyní
sporem, že ITM0 = 0. Případ ITM0 < 0 nem ůže nastat, prot ože pro všechna s ∈ P platí
I(s) ≥ 0 z předpokladu a M0(s) ≥ 0 z defin ice.
Protože I je semip ozitivn í, existu je s0 ∈ P takové, že I(s0) > 0. Neb oť uvažuj eme pouze
sítě se slabě souvislým grafem, existu je přechod t ∈ T takový, že t ∈ •s0 neb o t ∈ s0•.
Síť N je živá, tedy existuje označkování M dosažitelné z M0, v něm ž je přechod t uschop-
něn. Označíme-li M′ označ kování, do nějž se síť dostane z označkování M provedením
přechodu t, potom ITM > 0 neb o ITM′ > 0, protože M(s0) > 0 neb o M′(s0) > 0. Tedy
I není S-invariant — spor.
Věta (Postačuj ící podmínka ohraniče nosti sítě)
Nec hť N = (P,T,F) je Petriho síť. Má-li N pozitivní S-in varian t, pak je ohraničená pro
všechna počátení označkování.
Důkaz: Sporem. Nec hť má síť pozitiv ní S-in variant I, ale není ohraničená, tj. existuje
neohr aničené místo p ∈ P. Nec hť M je označ kování sítě. Protože p není ohran ičené,
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
existuj e dosažite lný markin g M′ takový, že
M′(p) > I
TM
I(p)
Potom, protože I je poziti vní, a místa nemoh ou obsaho vat záp orný počet tokenů, platí
ITM′ ≥ I(p)M′(p) > ITM
Tedy I nen í S-invariant — spor.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
T-invarianty
Poznámk a (Mot ivace pro T-in varianty)
S-in varian ty jsou definovány jako řešení rovnice XTN = 0T. Je přirozené zajímat se o
vlastn osti řešení duální rovnice NX = 0 a pokusit se je interpr etovat.
Definice (T-in variant, semip ozitivn í a pozitivn í T-invarian t)
T-invariantem Petri ho sítě N s incidenční maticí N nazv eme každé řešení v a81 rovnice
NX = 0
T-invariant J se nazývá semi pozitivní , jestliže J(t) ≥ 0 pro všechna t ∈ T a existuj e
t0 ∈ T, pro nějž J(t0) > 0. T-iv arian t J se nazýv á pozitivní , jestliže J(t) > 0 pro všechna
t ∈ T.
Věta (Alt ernativ ní defin ice T-invarian tu)
Nec hť N = (P,T,F) je Petriho síť. Funkce J : T → a81 je T-in variant právě tehdy, když
pro každé místo p ∈ P platí summationdisplay
t∈ •p
J(t) =
summationdisplay
t∈p•
J(t)
Důkaz: Důkaz je analogi cký důkazu alterna tivn í defini ce S-invariantu.
Věta (Parikův obraz poslou pnosti přechodů jako T-in variant)
Nec hť je posloupnost přechodů σ ∈ T∗ proveditelná v síti N = (P,T,F) z označ kování M.
Pak vectorσ je T-invarian t právě tehd y, když M σ→ M.
Důkaz: Přímý důsledek nutné podmínky dosažitelnosti.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Věta (Nu tná podmín ka živosti a ohran ičenosti — pozitivní T-in variant)
Nec hť je Petriho síť N = (P,T,F) s iniciálním marki ngem M0 živá a ohraničená. Potom
existuj e pozitivní T-in variant sítě N .
Důkaz: Protož e (N,M0) je živá, lze z každého označ kování připravit libovolný pře-
chod. Z každ ého označkování tedy existuje proveditelná posloupn ost přec hodů, která
obsah uje každý přechod ales poň jedn ou. Defin ujme reku rzívně označ kování Mi, 0 ≤ i.
Označ kování M0 je počáteční označ kování sítě. Označkování Mi+1 vznik ne poslou pností
přechodů σi z označ kování Mi, kde σi obsah uje každ ý přechod ales poň jednou .
Protože (N,M0) je ohraničená, existuje pouze konečně mnoho různ ých označkování, oz-
načme jejich počet n. Mezi výše definovanými označkováními Mi, 0 ≤ i ≤ n,
Vloženo: 24.04.2009
Velikost: 591,86 kB
Komentáře
Tento materiál neobsahuje žádné komentáře.
Copyright 2024 unium.cz