https://vik.wiki/index.php?action=history&feed=atom&title=FormModVizsga20080528FormModVizsga20080528 - Laptörténet2026-05-12T00:46:12ZAz oldal laptörténete a wikibenMediaWiki 1.43.8https://vik.wiki/index.php?title=FormModVizsga20080528&diff=137304&oldid=prevUnknown user: Új oldal, tartalma: „{{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…”2012-10-21T19:58:13Z<p>Új oldal, tartalma: „{{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…”</p>
<p><b>Új lap</b></p><div>{{GlobalTemplate|Infoalap|FormModVizsga20080528}}<br />
<br />
==Mikor mondjuk h 2 trafó párhuzamosan független?==<br />
<br />
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.<br />
<br />
==Hogyan értelmezhető a korlátosság foglama CPN-eknél (mind a kétféle megközelítést írja le)==<br />
<br />
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.<br />
<br />
Szerintem:<br />
* n felső integer korlát: minden M in [M0>:|M(p) < n<br />
* m felső multihalmaz korlát: minden M in [M0>:M(p) < m<br />
<br />
==LTL formális szintaxisa, és p B q levezetése alapoperátorokkal==<br />
<br />
* (L1) Minden P atomi kijelentés egy kifejezés<br />
* (L2) Ha p és q egy-egy kifejezés, <math>p \wedge q</math> és <math>\neg p</math> is<br />
* (L3) Ha p és q egy-egy kifejezés, akkor pUq és Xp is<br />
<br />
<math>p B q = \neg((\neg p) U q)</math><br />
==Mi a részleges döntés elve, mikor érdemes használni==<br />
<br />
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.<br />
<br />
-- [[EszenyiViktor|dög]] - 2008.06.24.<br />
<br />
<br />
[[Category:Infoalap]]</div>Unknown user