FormModVizsga20080528

Ez az oldal a korábbi SCH wiki-ről lett áthozva. Az eredeti változata itt érhető el.

Ha úgy érzed, hogy bármilyen formázási vagy tartalmi probléma van vele, akkor kérlek javíts rajta egy rövid szerkesztéssel.

Ha nem tudod, hogyan indulj el, olvasd el a migrálási útmutatót

Mikor mondjuk h 2 trafó párhuzamosan független?

Két transzformációs lépés [math]{M_0}\xrightarrow{r_1(o_1)}{M_1}[/math] és [math]{M_0}\xrightarrow{r_2(o_2)}{M_2}[/math] párhuzamosan függetlenek, ha az [math]r_1[/math] szabály Lhs részének (baloldalának) [math]o_1[/math] illeszkedésében, és az [math]r_2[/math] szabály Lhs részének (baloldalának) [math]o_1[/math] illeszkedésében minden közös elemet megőriz mindkét transzformációs lépés. Különben a két lépés konfliktusban van.

Hogyan értelmezhető a korlátosság foglama CPN-eknél (mind a kétféle megközelítést írja le)

Első: A C betűvel jelölt színfüggvény minden egyes p helyhez hozzárendel egy [math]C(p) = \sigma \in \sum[/math] típust. A hely típusa azon színezett típusok halmazát jelenti, amiket az adott hely tartalmazhat. Ez szerepet játszik a tranzíciók engedélyezettségében is, ugyanis az a tüzelés nem válhat engedélyezetté, ami olyan token tenne ki egy kimeneti helyre, ami inkompatibilis azon hely típusával. Ebben a vonatkozásában a típus a színezetlen Petri hálóknál megismert korlátos hely fogalmára hasonlít.

Szerintem:

• n felső integer korlát: minden M in [M0>:|M(p) < n
• m felső multihalmaz korlát: minden M in [M0>:M(p) < m

LTL formális szintaxisa, és p B q levezetése alapoperátorokkal

• (L1) Minden P atomi kijelentés egy kifejezés
• (L2) Ha p és q egy-egy kifejezés, [math]p \wedge q[/math] és [math]\neg p[/math] is
• (L3) Ha p és q egy-egy kifejezés, akkor pUq és Xp is

[math]p B q = \neg((\neg p) U q)[/math]

Mi a részleges döntés elve, mikor érdemes használni

Részleges döntés esetén az alapmodell helyett egy, az általa megvalósított működést fedő, szupermodellt vizsgálunk amely nála matematikailag könnyebben kezelhető. Ha a szupermodellről belátjuk, hogy egyetlen viselkedése sem sérti a megkívánt tulajdonságot, az általa fedett eredeti modellről is bebizonyítottuk azt. A módszer az indirekt bizonyításon alapul, felírjuk a tüzelési szekvenciák algebrai alakban általános állapotegyenletét, feladatspecifikus peremfeltételeit, és a bizonyítandó állítás negáltját, és belátjuk, hgoy nincs ilyen megoldás. Előnye, hogy az állapottér kimerítő bejárása helyett csak lineáris algebrai egyenlőtlenségrendszereket kell vizsgálni. Eredménye csak a "nincs ellenpélda" vagy a "nem tudni, hogy van-e ellenpélda" alternatívák közül kerülhet ki.

-- dög - 2008.06.24.