- 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álPetriho sítě
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Poznámk a autora
Tento materiál vznik l podle kur zu Pet riho sítě vyu čovaného doc. RNDr . Antonínem
Kučerou , Ph.D. v podzim ním semes tru 2003 na Faku ltě informati ky Masarykovy uni-
verzity v Brně. Zdrojem byly především zápisky z předn ášek mne a Pavla Šime čka. Na
některý ch míste ch byly použit y materiály poskytn uté Tomáše m Krato chvílou.
Protože měl tento materiál sloužit k mé přípravě na zkoušku, dělal jsem vše pro to, aby
neobsah oval chyby a nepřesnosti. To však nez namená, že je obsahovat nemůže — nenesu
žádno u odpovědnost za škody vzni klé použitím tohoto textu.
Up ozornění na chyby, překlepy, špatn é form ulace, námě ty a připomínk y, jakož i ocenění,
poděkování nebo dotazy na číslo mého účtu pro konkrétn ější ocenění můžete poslat na
holecek [at] informatics .muni.cz
Hon za Holeč ek
8. 3. 2004
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Obsah
Základní pojmy
Definice : Petrih o síť
Pozná mka: Neprázdn ost množin míst a přechodů Petriho sítě
Not ace : Mn ožiny uzlů, které „beroucsquotedblright a „dávajícsquotedblright do uzlu Petri ho sítě
Příkl ad: Jedn oduchá Petriho síť
Definice : Označ kování, uschopn ěný přechod
Pozná mka: Vyj adřo vací síla Petriho sítí
Definice : Přechodový systém Petri ho sítě
Příkl ad: Producent-konzument s neohraničenou vyro vnávací pamětí
Příkl ad: Producent-konzument s ohrani čenou vyrovnávací pamětí
Příkl ad: Mo del chemic ké reakce
Příkl ad: Systém s omezujícími podmín kami
Anal ýza Petriho sítí
Definice : Dosaž itelné označ kování
Not ace : Mn ožina dosaž itelných označkování
Definice : Živost přechodu, živost sítě
Definice : Mrtvé místo, mrtvý přechod
Definice : Problém y pro Petrih o sítě
Problém dosažiteln osti (reachab ility)
Problém sub -marking reachab ility
Problém zero-reac hab ility
Problém single- place zero-reac habil ity
Problém pokrytelnosti
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Problém ohraničenosti místa
Problém k-ohr aniče nosti místa
Problém ohraničenosti sítě
Problém k-ohr aniče nosti sítě
Problém inkluze množin dosažiteln ých označkování
Problém rovnosti množin dosažiteln ých označkování
Problém živosti přechodu
Problém živosti sítě
Problém uváznutí sítě (mrtvost sítě)
Strom pokry telnosti
Definice : Roz šířené označkování
Definice : Strom pokry telnosti
Pozná mka: Roz hodnuteln ost problému pokryteln osti
Příkl ad: Strom pokrytelnosti Petrih o sítě
Lemma : Nekonečná neklesající podposloupnost
Lemma : Dicksonovo lemma, Dickson’ s Lem ma
Věta: Ukončení konstru kce stromu pokrytelnosti
Funk ce, které nejsou primiti vně reku rzívní
Definice : Ram seova funkce
Věta: Rams eova věta
Definice : Hilb ert-Ac kermann ova funkce
Složi tost konstr ukce strom u pokrytelnosti
Věta: Velikost stromu pokrytelnosti
Hierarc hie problém ů vzhledem k redukci
Věta: Polynomiáln í ekvivalence reac hability problém ů
Redukce sing le-place zero-reac hab ility na sub-m arking reachab ility
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Redukce sub -mark ing reac hability na zero-r eachability
Redukce zero-reachab ility na reachab ility
Redukce reachabi lity na sub -mark ing reac habil ity
Redukce zero-reachab ility na single-place zero-reac habili ty
Věta: Živost sítě a single-place zero-reac habili ty
Pozná mka: Ostatní varianty živosti a singl e-place zero-reac hab ility
Věta: Živost přechodu a dosažitelnost
Minsk ého stroj
Definice : Min ského stro j
Ekvivalence přechodových systémů
Definice : Stop y stavu, trace -ekviv alence
Definice : Bisimulace, bisimulačn í ekvi valence
Pozná mka: Vztah bisim ulační ekvi valence a trace -ekvivalence
Věta: Neroz hodnuteln ost ekviv alencí
Věta: Nerozho dnutelnost inklu ze a rovnosti množin dosaž iteln ých označ kování
Mo del-checking Petriho sítí
Pozná mka: Logiky LTLF a LTL G
Pozná mka: Séman tika tem porál ních logik pro Petrih o sítě
Věta: Neroz hodnuteln ost LTL F
Věta: Neroz hodnuteln ost EG-fragmen tu CTL
Věta: Neroz hodnuteln ost EF-fragm entu CTL
Pozná mka: EF-fragm ent CT L bez zanoření tem porál ních operátorů
Pozná mka: „Ac tion-basedcsquotedblright logiky
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Klasické techniky analýzy Petriho sítí
Pozná mka: Ome zení pro klasické techniky analý zy
Definice : Inciden ční mati ce
Definice : Kron eckerovo delta
Pozná mka: Notace vektorů , označkování jako vektor y
Příkl ad: Incid enční matice
Definice : Parikův obraz
Věta: Nut ná podmínk a dosažitelnosti
S-invarianty
Příkl ad: Moti vace pro S-invarian ty
Definice : S-in varian t
Příkl ad: Urče ní S-in variantů
Věta: Altern ativn í defin ice S-in variantů
Věta: Altern ativn í nutn á podmínk a dosažitelnosti
Definice : Semip ozitivní a pozitivní S-invarianty
Věta: Nut ná podmínk a živosti sítě
Věta: Postač ující podmín ka ohran ičenosti sítě
T-invarianty
Pozná mka: Moti vace pro T-in varianty
Definice : T-invarian t, semip oziti vní a pozitivní T-in variant
Věta: Altern ativn í defin ice T-invarian tu
Věta: Parikův obraz posloup nosti přechodů jako T-in variant
Věta: Nut ná podmínk a živosti a ohraničenosti — poziti vní T-in variant
Věta: Nut ná podmínk a živosti a ohraničenosti — silná souvislost
S-sys témy
Definice : S-sys tém
Věta: Nut ná podmínk a dosažitelnosti v S-sys tému — zachování počtu tokenů
Lemma : Nut ná podmínk a siln é souvislosti graf u S-sys tém u
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Věta: Živost S-systém ů
Lemma : Postač ující podmín ka dosaž iteln osti v S-systém u
Věta: Ohrani čenost živých S-systém ů
Věta: Dosaž itelnost v živém S-sys tému I
Věta: Char akte rizac e S-invariantů
Věta: Dosaž itelnost v živém S-sys tému II
T-sys témy
Definice : T-systé m
Příkl ad: Neohran ičený T-s ystém
Definice : Cyklu s
Příkl ad: T-systém s cykly
Věta: Nut ná podmínk a dosažitelnosti v T-systé mu
Důs ledek : Nut ná podmínk a neohrani čenosti mís ta v T-s ystém u
Věta: Živost T-s ystém ů
Příkl ad: Ilustrace k důkazu charakt eristické podmínky živosti T-sys témů
Důs ledek : Složitost problém u živosti T-s ystém ů
Věta: Char akte rizac e T-in variantů
Příkl ad: Živý 1-ohr aničen ý T-systé m
Věta: Ohrani čenost živých T-s ystém ů
Lemma : Vlastnosti řešení nutn é podmín ky dosažite lnosti pro T-s ystém y
Lemma : Celočíselné řešení nutné podmínk y dosaž itelnosti pro T-systé my
Věta: Dosaž itelnost v živém T-systé mu
Free-choice systém y
Definice : Free-choice systém
Věta: Altern ativn í defin ice free- choice systé mů
Definice : Cluster uzlu
Pozná mka: Clustery v obecné Petriho sítí a ve free-choice systé mu
Věta: Roz klad na clustery
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Příkl ad: Roz klad na clustery
Definice : Stab ilní predikáty — sifony a pasti
Pozná mka: Význam pojmů sifon a past vzhledem k označ kování
Věta: Sifon v uváznuté síti
Věta: Postač ující podmín ka neuv áznutí
Lemma : Nutn á podmín ka pro existenci mrtv ého přec hodu free-choice systém u
Lemma : Nutn á podmínk a neživýc h free-choice systé mů
Věta: Postač ující podmín ka živosti free-choice systém u
Pozná mka: Existence největšího sifonu a nejv ětší pasti
Definice : Alok ace, doména
Lemma : Nekonečná posloup nost přec hodů k alokaci
Definice : Alok ace bez cyk lů vzhledem k množin ě mís t
Lemma : Existence alokace bez cyklů v Petriho síti pro danou množinu míst
Věta: Nut ná podmínk a živosti free- choice systému
Věta: Com mon erova věta
Důs ledek : Složitost problém u živosti a než ivosti
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Seznam obrázků
Příklad jedn oduché Petrih o sítě
Mo del pro ducent-konzumen t s neome zenou pamětí
Mo del pro ducent-konzumen t s koneč nou pamětí
Mo del chemic ké reakce
Příklad systém u s omezujícími podmín kami
Příklad stromu pokrytelnosti
Petri ho síť pro výp očet A0 (Hil bert-Ac kermann ova funkce)
Petri ho síť pro výp očet Ai+1 (Hil bert-Ac kerman nova funkce)
Reduk ce sub -mar king reac hability na zero-reachability
Reduk ce zero-reachab ility na single-place zero-reac habil ity
Reduk ce single-place zero-reac hability na živost
Rozdíl mezi bisimulací a trace -ekviv alencí — přechodový systém
Rozdíl mezi bisimulací a trace -ekviv alencí — Petrih o síť
Nerozho dnutelnost ekviv alencí — redu kce Min ského stro je
Rovnost množin označ kování — redukce instrukcí typu I a II Minsk ého stroje
Rovnost množin označ kování — redukce instrukce halt Minského stroje
Inkluze množin označ kování — reduk ce Minsk ého stroje
Hierar chie tem porál ních logik vzhl edem k vyjad řovací síle
Mo del-c hecking LTL — redukce Minsk ého stroje
Mo del-c hecking EF-fragm entu CTL — redukce Minského stro je
Příklad Petrih o sítě a její incid enční matice
Příklad Petrih o sítě a jejích S-invariantů
Příklad Petrih o sítě a výpočtu jejích S-in variantů
Ilustrace k důkazu nutné podmínk y živosti a ohra niče nosti
Příklad neohr aniče ného T-sys tému
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Příklad T-systé mu s cykly
Ilustrace k důkazu charak teristické podmínky živosti T-systé mů
Příklad živého 1-ohr aničeného systém u
Clu stery v obecné Petriho síti a free-choice systé mec h
Rozklad Petri ho sítě na clustery
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Základn í pojmy
Moti vací pro vznik Petriho sítí bylo modelo vat řídící systém y. Neformálně je Petrih o síť
graf se dvěma typy uzlů (míst y a přec hody) s násobnými hranami. Hrany jsou přitom
pouze mezi uzly různých typů. Ob ecně žádná další ome zení nejsou, zejmé na tedy nem usí
být vyváženy vstup ní a výstu pní stupně uzlů.
Definice (Petri ho síť)
Pet riho síť je tro jice N = (P,T,F), kde P negationslash= ∅ je konečná množina míst (places ), T negationslash= ∅
je koneč ná množina přec hodů (transiti ons) a F je přechodová funkce (float )
F : (P × T) ∪ (T × P) → a780
Poznámk a (Neprá zdnost množin míst a přechodů Petriho sítě)
Zde jsem se dopu stil největší odchylky od poznámek z přednáše k, kde toto ome zení na
Petrih o sítě nebylo klad eno. Vše chny „za jímavécsquotedblright sítě jej však jistě splň ují. Toto ome zení
je nutné při anal ýze free-choice systé mů a zavést jej přímo v hlavní defin ici mi připadalo
nejr ozumnější. Platnost ostatn ích tvrze ní tím jistě nebude ovliv něna — jedn á se o strikt ní
ome zení množin y petriho sítí.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Not ace (Mn ožiny uzlů , které „beroucsquotedblright a „dávajícsquotedblright do uzlu Petri ho sítě)
Nec hť N = (P,T,F) je Petri ho síť. Pro každý přechod t ∈ T a pro každé místo p ∈ P
defin ujeme množin y
t• = {p ∈ P | F(t,p) > 0}
•t = {p ∈ P | F(p,t) > 0}
p• = {t ∈ T | F(p,t) > 0}
•p = {t ∈ T | F(t,p) > 0}
Notace se přiroze ně rozšiřu je na množiny přec hodů a míst.
Pro mís to p ∈ P je p• nefor málně množina přechodů, z nichž mís to může získat token,
a •p množina přechodů, do nichž může token odevzda t (viz níže).
Příkl ad (Jedn oduchá Petriho síť)
Na následuj ícím obrázku je příklad jedno duché sítě, kde
P = {p1,p2,p3}
T = {t1,t2,t3}
F = {(p1,t1,1),(p3,t3,2),(t3,p1,0,...)}
F(p1,t2) = 1
F(p3,t3) = 2
F(t3,p1) = 0
{p1,p2}• = {t1,t2}
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
p1
p2
p3
t1
t2
t3
Definice (Označ kování, uschop něný přechod)
Nec hť N = (P,T,F) je Petriho síť. Označkování (mar king ) je funkce M : P → a780.
Přechod t ∈ T je uschopněn v M, pokud
∀p ∈ t• : M(p) ≥ F(p,t)
Neformáln ě lze označ kování chápat jako distrib uci tokenů v síti: udává počet tokenů
v jedn otliv ých místec h.
Poznámk a (Vyj adřovací síla Petriho sítí)
V defin ici uschop něného přechodu je klíčové použití relac e ≥ mís to =. Při použití rovnosti
by Petriho sítě byly stejn ě silné jako Turingovy stro je a mnoh o vlastností sítí by bylo
nerozho dnuteln ých. Cílem je přitom umožnit efektiv ní verifikaci dostateč ně velké třídy
systém ů — s rovností by třída byla příliš velká.
Definice (Přechodový systém Petriho sítě)
Nec hť N = (P,T,F) je Petriho síť a A je množina návěští (ab eceda). Nec hť je dán a
funkce l : T → A přiřazuj ící přechodům ne nutně vzájemně různá návěští. Přechodový
systém s návěštími pro Petriho síť N s olabelováním l defin ujeme jako TN = (S,A,→),
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
kde S je množina všech označ kování, →⊆ S × A × S a M a→ M′ právě tehd y, když
existuj e přechod t ∈ T uschopn ěný v M takový, že l(t) = a a
∀p ∈ P : M′(p) = M(p) − F(p,t) + F(t,p)
Příkl ad (Produce nt-konzument s neohraničenou vyro vnávací pamětí)
produce store
produce store
cache
fetch consume
Význam tokenů je verzatiln í. Zatímc o v místě cache tokeny repreze ntují výpočetní zdro je
(data), tokeny v ostatn ích míste ch udávají tok řízení (uschop ňují přec hody odpovída jící
jedn otlivým akcím).
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Příkl ad (Produce nt-konzument s ohraničenou vyro vnávací pamětí)
produce store
produce store
cache
capa city
fetch consume
Počet tokenů v místě capa city udává velikost volné vyrovnávací paměti. Přec hody store
mohou být odpáleny (provedeny) jen tehdy, pokud je v místě capa city ales poň jeden token
— v paměti je mís to pro ulože ní. Přechod fetch vybírá data z pamě ti, takže přidává jeden
token do místa capa city. Iniciáln í počet tokenů v místě capa city udává velikost vyrovnávací
paměti.
Příkl ad (Mo del chemic ké reakce)
Nec hť v systém u mohou probíh at následuj ící reak ce:
H2C2O4 → 2CO 2 + 2H+ + 2e−
2e− + 2H+ + H2O2 → 2H2O
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Petrih o síť mo delující takový systém je na následu jícím obrázku . Iniciáln í markin g udává
iniciální počet jednotlivýc h molekul v systé mu. Jedna reak ce je reprezentována jedním
přechodem.
H2C2O4 (2 molekuly )
CO 2
H+
e−
H2O2 (4 mole kuly)
H2O
Příkl ad (Systém s omezují cími podmín kami)
okna příčky omítk a elektřina top ení
insta lace oken příček omítky elektro top ení
Petrih o síť z předchzího obrázku popisuje závislosti mezi jednotli vými pracemi při stavbě
dom u. Platí-li pro přechod t a místo p vztah F(p,t) = F(t,p) = 1, mís to p tvoří omezu jící
podmínku pro přec hod t — odpálení přechodu t nezm ění distrib uci tokenů v místě p,
ale vyžadu je přítomnost ales poň jedn oho. V některých případ ech se hovoří o run-place
hranác h.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Ve větším systé mu je možné analy zovat, zda je projekt realizo vatelný (dosaž itelnost kon-
cového marki ngu z iniciálního), které části jsou kritické apod. V tom to případě není
nutná ani dosažitelnost (umožňuje specifikovat přesný počet tokenů v dan ém mís tě), ale
stač í pokryteln ost — v každém místě musí být alespoň nějak ý počet tokenů (zde jeden
token).
Mo del lze navíc modifikovat tak, aby v každém místě mohl být nejvý še jeden token.
Mo difikace je analogic ká omez ení vyrovnávací paměti v mo delu producent-konzumen t.
nehotová práce
provedení práce
hotová práce
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Analýza Petrih o sítí
Základ ní prob lémy řešené u všec h formáln ích mo delů jsou dosažitelnost, ukončení a
živost. Aby byl model efektiv ně analyzo vatelný, musí být tyto vlastnosti rozhodnutelné.
Dalším stup něm je rozho dnutelnost obecnějšíc h temp oráln ích vlastností (for mulí tem-
poráln í logiky) a nejvy šším stup něm je plná formáln í verifikace (ověření ekvivalence vůči
dan é specifik aci).
Definice (Dosaž itelné označ kování)
Označ kování M′ je dosažitel né z M v Petriho síti N = (P,T,F), jestliže je v přechodovém
systém u indukovaném sítí N stav M′ dosažiteln ý z M.
Not ace (Mn ožina dosažite lných označkování)
Pro Petriho síť N a její označ kování M defin ujeme funkci
Reach(N,M) = {označ kování M′ sítě N | M′ je dosaž itelné z M}
Definice (Živ ost přec hodu, živost sítě)
Buď N = (P,T,F) Petriho síť, M0 její označ kování. Přechod t ∈ T je živý pro M0, jestliže
pro každé M dosažitelné z M0 existuj e M′ dosažitelné z M tak, že t je uschop něný v M.
Petrih o síť nazveme živou pro mar king M0, pokud je pro M0 živý každý její přechod.
Definice (Mr tvé místo, mrtvý přechod)
Nec hť N = (P,T,F) je Petriho síť. Místo p ∈ P se nazývá mrtvé v mar kingu M, poku d
pro všechna označkování M′ dosažitelná z M platí M′(s) = 0. Přechod t ∈ T se nazýv á
mrtvý, není -li připravený v žádném označ kování dosaž itelném z M.
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Definice (Probl émy pro Petri ho sítě)
Probl ém dosažiteln osti (reachability)
Instan ce: Petriho síť N = (P,T,F) a její označkování M, M′.
Otázk a: Je označ kování M′ dosažitelné z M v N ?
Probl ém sub -marking reachab ility
Instan ce: Petriho síť N = (P,T,F), její označ kování M0 a částeč né označkování M.
Otázk a: Existuj e označ kování M′ sítě N dosažitelné z M0 takové, že kdykoli je pro p ∈ P
defin ováno M(p), potom M′(p) = M(p)?
Probl ém zero -reachab ility
Instan ce: Petriho síť N = (P,T,F) a její označkování M0.
Otázk a: Je z M0 dosažitelné nulové označkování sítě N (síť neobsah uje žádn é tokeny)?
Probl ém single-pl ace zero-reac hab ility
Instan ce: Petriho síť N = (P,T,F), její označ kování M0 a místo p ∈ P.
Otázk a: Je z M0 v síti N dosažitelné označkování M takové, že M(p) = 0?
Probl ém pokry telnosti
Instan ce: Petriho síť N = (P,T,F) a její označkování M, M′
Otázk a: Existu je označkování M′′ dosažitelné v Petriho síti N z markingu M takové, že
∀p ∈ P : M′′(p) ≥ M′(p)?
Probl ém ohrani čenost i míst a
Instan ce: Petriho síť N = (P,T,F), její označ kování M a místo p
Otázk a: Existuj e k ∈ a780 takové, že pro každé označ kování M′ dosažitelné z M v N platí
M′(p) ≤ k?
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Probl ém k-ohran ičenosti místa
Instan ce: Petriho síť N = (P,T,F), její označ kování M, mís to p a k ∈ a780
Otázk a: Platí pro každé ozna čkování M′ dosažitelné z M v N nero vnost M′(p) ≤ k?
Probl ém ohrani čenost i sítě
Instan ce: Petriho síť N = (P,T,F) a její označkování M
Otázk a: Je každé místo sítě ohraničené? Altern ativn ě (množin a míst je konečná): Existuj e
k ∈ a780 tak, že každé místo je k-ohra niče né?
Probl ém k-ohran ičenosti sítě
Instan ce: Petriho síť N = (P,T,F), její označ kování M, k ∈ a780
Otázk a: Je každé místo sítě k-ohran ičené?
Probl ém inklu ze množin dosaž itelných označkování
Instan ce: Petriho sítě N1 = (P,T1,F1), N2 = (P,T2,F2) nad stejn ou množin ou míst
a jejic h počáteční označ kování M1, M2.
Otázk a: Platí Reach(N1,M1) ⊆ Reac h(N2,M2)?
Probl ém rovnost i množin dosažiteln ých označ kování
Instan ce: Petriho sítě N1 = (P,T1,F1), N2 = (P,T2,F2) nad stejn ou množin ou míst
a jejic h počáteční označ kování M1, M2.
Otázk a: Platí Reach(N1,M1) = Reach(N2,M2)?
Probl ém živosti přechodu
Instan ce: Petriho síť N = (P,T,F), její označ kování M0 a přechod t ∈ T.
Otázk a: Je přechod t živý pro M0 v N ?
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Probl ém živosti sítě
Instan ce: Petriho síť N = (P,T,F) a její označkování M0.
Otázk a: Je síť N živá pro M0? (Je živý každý její přechod pro M0?)
Probl ém uváznutí sítě (mrtv ost sítě)
Instan ce: Petriho síť N = (P,T,F) a její označkování M0.
Otázk a: Existuj e pro (N,M0) dosažitelné označkování M takové, že (N,M) je mrtv á,
tj. není připraven žádn ý přechod?
Obsah
ObrÆzky
Rejstłj237k
Dopłedu
Zpj236t
Strom pokryteln osti
Definice (Rozš ířené označ kování)
Rozšíř ené označkování M Petri ho sítě N = (P,T,F) je funkce M : P → a780 ∪ {ω}, kde
defin ujeme ∀a ∈ a780
ω ± a = ω
a < ω
ω ≤ ω
Definice (Strom pokrytelnosti)
Strom pokry telnost i (cover ability tree, Karp- Mil ler tree) pro danou Petri ho síť N =
(P,T,F) a její markin g M0 je strom, který vznikne následu jící iterati vní konstrukcí.
Každý uzel x strom u pokrytelnosti je oho dnocen právě jedním rozš ířeným označ kováním
sítě N . V každém okamžiku konstru kce strom u pokry telnosti má každý uzel právě jeden
z následuj
Vloženo: 24.04.2009
Velikost: 591,86 kB
Komentáře
Tento materiál neobsahuje žádné komentáře.
Copyright 2024 unium.cz