FormModVizsga20080528 forrásának megtekintése

{{GlobalTemplate|Infoalap|FormModVizsga20080528}}

==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.

-- [[EszenyiViktor|dög]] - 2008.06.24.


[[Category:Infoalap]]