Hardver és szoftver rendszerek verifikációja Röviden megválaszolható kérdések

Hardver és szoftver rendszerek verifikációja Röviden megválaszolható kérdések 1.

Az informatikai rendszereknél mit ellenőriznek validációnál és mit verifikációnál?

2.

A szoftver verifikációs technikák közül soroljon fel hármat!

3.

Melyek a modell-ellenőrzés fázisai és a fázisok feladata mi?

4.

Mit lehet tenni, ha a vizsgált rendszermodell túl nagy?

5.

A modell-ellenőrzés hátrányai közül soroljon fel legalább hármat!

6.

A modell-ellenőrzés előnyei közül soroljon fel legalább hármat!

7.

Adja meg az egyszerű átmeneti rendszer definícióját!

8.

Definiálja az utak konkatenációját (összefűzését)!

9.

Adja meg a címkézett átmeneti rendszer definícióját!

10. Címkézett átmeneti rendszernél definiálja az út nyomát! 11. Adja meg a paraméteres átmeneti rendszer definícióját! 12. Adjon meg egy olyan címkézett átmeneti rendszert, mely egy Boole változó alapvető működését modellezi! 13. Adjon meg egy olyan címkézett átmeneti rendszert, mely egy korlátos puffer alapvető működését modellezi! 14. Hogyan tudná modellezni címkézett átmeneti rendszerrel egy szekvenciális program működését? 15. Adja meg a közös erőforrás kizárólagos kezelését megvalósító Peterson algoritmust! 16. Egyszerű átmeneti rendszerek között definiálja a homomorfizmus fogalmát! 17. Címkézett átmeneti rendszerek között definiálja a homomorfizmus fogalmát! 18. Definiálja a paraméteres átmeneti rendszerek között a homomorfizmus fogalmát! 19. Igaz-e a következő állítás: Minden címkézett átmeneti rendszer egyben paraméteres átmeneti rendszer is. Állítását indokolja! 20. Adja meg a Petri-háló definícióját és működésének módját! 21. Definiálja Petri-hálónál a token eloszlást, illetve azt, hogy egy t tranzíció mikor tüzelhető és mi a hatása! 22. Definiálja az egyszerű átmeneti rendszerek szabad szorzatát! 23. Definiálja a címkézett átmeneti rendszerek szabad szorzatát! 24. Hogyan adható meg címkézett átmeneti rendszerek szinkronizált szorzata? 25. Definiálja a paraméteres átmeneti rendszereknek egy adott I szinkronizációs megszorítások halmaza feletti szinkronizált szorzatát! 26. Adja meg processzus algebrában a parallel művelet definícióját, szemantikáját! 27. Adja meg processzus algebrában a rekurzió művelet definícióját, szemantikáját! 28. Adja meg processzus algebránál a restrikció és a prefix műveletek definícióját, szemantikáját! 1

29. Adja meg processzus algebránál a choice művelet definícióját, szemantikáját! 30. Jelölje AP={Px | xX} az állapot atomi kijelentések halmazát, ahol X az állapot paraméterek halmaza. Definiálja az AP feletti kijelentés logika állapotformuláit! 31. Jelölje AP ={Qy | yY} az átmenet atomi kijelentések halmazát, ahol Y az átmenet paraméterek halmaza. Definiálja az AP feletti kijelentés logika átmenetformuláit! 32. Definiálja az LTL logika formuláit! 33. Definiálja az f1 U f2 LTL útformula szemantikáját! 34. Definiálja az f1 B f2 LTL útformula szemantikáját! 35. Definiálja Xf LTL útformula szemantikáját! 36. Egy út mikor elégíti ki a Gf LTL útformulát? 37. LTL logikában az operátorok {¬, , X, U} adekvát halmazába tartozó műveletek segítségével fejezze ki a Gf formulát, ahol f egy LTL formula! 38. LTL logikában az operátorok {¬, , X, U} adekvát halmazába tartozó műveletek segítségével fejezze ki a Ff formulát, ahol f egy LTL formula! 39. LTL logikában az operátorok {¬, , X, U} adekvát halmazába tartozó műveletek segítségével fejezze ki a f1 W f2 formulát, ahol f1 és f2 egy-egy LTL formula! 40. Legyen A egy (X, Y)-paraméterezett átmeneti rendszer, S0 az A kezdőállapotainak halmaza, AP = {Px| xX} az állapot atomi kijelentések halmaza, f egy AP feletti LTL formula. Mikor mondjuk, hogy az A átmeneti rendszer egy sS állapota kielégíti a f formulát? 41. Legyen A egy (X, Y)-paraméterezett átmeneti rendszer, S0 az A kezdőállapotainak halmaza, AP = {Px| xX} az állapot atomi kijelentések halmaza, f egy AP feletti LTL formula. Mikor mondjuk, hogy az A átmeneti rendszer kielégíti a f formulát? 42. Legyen A az alábbi {a, b} állapot-paraméteres átmeneti rendszer. Kielégíti-e az A átmeneti rendszer az f = G(¬b G(a ¬b)) LTL formulát? Állítását indokolja!

43. Definiálja a HML logika állapotformuláit adott A véges címkehalmaz felett! 44. Legyen A egy véges címkehalmaz, f egy A feletti HML formula. Definiálja a f HML formula szemantikáját! 45. Legyen A egy véges címkehalmaz, f egy A feletti HML formula. Fejezze ki az operátorok {¬, }{ | aA} halmazába tartozók segítségével a [a]f HML formulát! 46. Adja meg egy (X, Y)-paraméterezett átmeneti rendszer feletti HML logikában a [g]f formula szemantikáját, ahol g átmenetformula, az f HML formula! 47. Címkézett átmeneti rendszernél mi a [a]f HML formula szemantikája, illetve mi mit jelöl a formulában? 48. Definiálja a Dicky logika állapotformuláit! 2

49. Definiálja a Dicky logika átmenetformuláit 50. Legyen g a Dicky logika egy átmenetformulája. Adja meg az tgt(g) állapotformula szemantikáját! 51. Legyen g a Dicky logika egy átmenetformulája. Adja meg az src(g) állapotformula szemantikáját! 52. Legyen f a Dicky logika egy állapotformulája. Adja meg az out(f) átmenetformula szemantikáját! 53. Legyen f a Dicky logika egy állapotformulája. Adja meg az in(f) átmenetformula szemantikáját! 54. Fejezze ki Dicky logikában a f HML formulát (a átmenet címke)! 55. Adjon meg olyan állapotformulát a Dicky logikában, melyet kielégítő állapotokból indul ki átmenet! 56. Adjon meg olyan állapotformulát a Dicky logikában, melyet kielégítő állapotokba nem vezet átmenet! 57. Legyen A egy (X, )-paraméterezett átmeneti rendszer, melyben minden állapotnak van rákövetkezője. Definiálja az A feletti számítási fákat! 58. Adja meg az AP (állapot atomi kijelentések halmaza) feletti CTL logika szimbólumait! 59. Definiálja az AP (állapot atomi kijelentések halmaza) feletti CTL logika formuláit! 60. Legyen A egy (X, )-paraméterezett átmeneti rendszer, AP={Px | xX}, s az A egy állapota, f egy AP feletti CTL formula. Definiálja A, s|= EXf kielégítési relációt! 61. Legyen A egy (X, )-paraméterezett átmeneti rendszer, AP={Px | xX}, s az A egy állapota, f egy AP feletti CTL formula. Definiálja A, s|= AXf kielégítési relációt! 62. Legyen A egy (X, )-paraméterezett átmeneti rendszer, AP={Px | xX}, s az A egy állapota, f1 és f2 egy-egy AP feletti CTL formula. Definiálja A, s|= EU(f1, f2) kielégítési relációt! 63. Legyen A egy (X, )-paraméterezett átmeneti rendszer, AP={Px | xX}, s az A egy állapota, f1 és f2 egy-egy AP feletti CTL formula. Definiálja A, s|= AU(f1, f2) kielégítési relációt! 64. Jelölje AP az atomi kijelentések halmazát és legyen f és g AP feletti CTL állapotformulák. Mikor mondjuk, hogy f a g formulával ekvivalens (vagyis f  g)? 65. CTL logikában az operátorok {¬, , EX, EG, EU} adekvát halmazába tartozó műveletek segítségével fejezze ki az EFf formulát, ahol f egy CTL formula! 66. CTL logikában az operátorok {¬, , EX, EG, EU} adekvát halmazába tartozó műveletek segítségével fejezze ki az AGf formulát, ahol f egy CTL formula! 67. Legyen A az alábbi {a, b} állapot-paraméteres átmeneti rendszer. Adja meg az A átmeneti rendszer f = AU(¬Pa, Pb) CTL formulát kielégítő állapotainak Sf halmazát! Állítását indokolja!

3

68. Legyen A az alábbi {a, b} állapot-paraméteres átmeneti rendszer. Adja meg az A átmeneti rendszer f = EU(Pa, (¬Pa  AU(¬Pa, Pb))) CTL formulát kielégítő állapotainak Sf halmazát! Állítását indokolja!

69. Legyen A az alábbi X={a, b, c} állapot-paraméteres átmeneti rendszer és f = EGPb egy CTL formula. Adja meg az A átmeneti rendszer azon állapotainak Sf halmazát, melynek elemei az f CTL állapotformulát kielégítik! Állítását indokolja!

70. Definiálja az AP állapot atomi kijelentések halmaza felett a CTL* logika szimbólumait! 71. Definiálja az AP állapot atomi kijelentések halmaza felett a CTL* logika állapotformuláit! 72. Definiálja az AP állapot atomi kijelentések halmaza felett a CTL* logika útformuláit! 73. Legyen A egy (X, )-paraméterezett átmeneti rendszer, AP={Px | xX}, s az A egy állapota, g egy AP feletti CTL* útformula. Definiálja A, s|= Eg kielégítési relációt! 74. Legyen A egy (X, )-paraméterezett átmeneti rendszer, AP={Px | xX}, c az A egy végtelen útja, g egy AP feletti CTL* útformula. Definiálja A, c |= Xg kielégítési relációt! 75. Legyen A egy (X, )-paraméterezett átmeneti rendszer, AP={Px | xX}, c az A egy végtelen útja, g1 és g2 egy-egy AP feletti CTL* útformula. Definiálja A, c |= U(g1, g2) kielégítési relációt! 4

76. Mit értünk egy logika kifejezőerején? Igaz-e a következő állítás: Az LTL kifejező ereje kisebb, mint a CTL kifejezőereje. Állítását indokolja! 77. Mit értünk egy logika kifejezőerején? Igaz-e a következő állítás: Az LTL kifejező ereje kisebb, mint a CTL* kifejezőereje. Állítását indokolja! 78. Mit értünk egy logika kifejezőerején? Igaz-e a következő állítás: A CTL és a CTL* kifejezőereje nem hasonlítható össze. Állítását indokolja! 79. Legyen AP az állapot atomi kijelentések halmaza, f egy AP feletti LTL állapotformula. Adja meg azt az AP feletti CTL* állapotformulát, mely ekvivalens az f formulával! 80. Legyen f és g AP atomi kijelentések halmaza feletti LTL, CTL, CTL* állapotformulák. Mikor mondjuk, hogy f és g ekvivalensek egymással? 81. Definiálja az időzített átmeneti rendszert! 82. Definiálja (időzített automatákkal kapcsolatban) az órák egy C halmaza feletti órafeltételek halmazát! 83. Mikor mondjuk (időzített automatákkal kapcsolatban) az órák egy C halmaza feletti g1 és g2 órafeltételekről, hogy ekvivalensek? 84. Definiálja egy C órahalmaz feletti időzített automatánál, hogy egy g órafeltételt egy v óra értékelés mikor elégít ki (v╞ g)! 85. Definiálja a C órák halmaza és az A akciók halmaza felett az időzített automata fogalmát! 86. Időzített automatáknál mik a helyinvariánsok? 87. Időzített automatáknál egy átmenet hogyan adható meg? 88. Legyen M = (L, l0, E, I) egy időzített automata valamely A akciók halmaza és C órák halmaza felett. Definiálja az M időzített automatához rendelt A feletti T(M) időzített átmeneti rendszer állapotait és a kezdőállapotait! 89. Legyen M = (L, l0, E, I) egy időzített automata valamely A akciók halmaza és C órák halmaza felett. Definiálja az M időzített automatához rendelt A feletti T(M) időzített átmeneti rendszer átmeneteit! 90. Hogyan valósul meg az időzített automaták hálózatában a komponensek közötti kommunikáció? 91. Definiálja a C órák, Ch csatornák és az A akciók halmaza feletti M = <M1, …, Mn>

időzített automaták hálózata működését megadó T(M) átmeneti rendszer állapotait és kezdőállapotát!

92. Definiálja a C órák, Ch csatornák és az A akciók halmaza feletti M = <M1, …, Mn>

időzített automaták hálózata működését megadó T(M) átmeneti rendszer átmeneteit!

93. Definiálja az AP állapot atomi kijelentések halmaza és C órahalmaz felett a TCTL logika

szimbólumait! 94. Definiálja az AP állapot atomi kijelentések és a C órahalmaz felett a TCTL állapotformulákat! 95. Időzített átmeneti rendszerben definiálja az idő-divergens utakat! 96. Mikor nevezünk egy időzített automatát idő-divergensnek? 97. Legyen M egy időzített automata az A akcióhalmaz, C órahalmaz és AP állapot tulajdonság halmaz felett, T(M) az M-hez rendelt időzített átmeneti rendszer, q állapot a T(M)-ben. Definiálja a  AP-re a T(M), q |= a relációt! 5

98. Legyen M egy időzített automata az A akcióhalmaz, C órahalmaz és AP állapot tulajdonság halmaz felett, T(M) az M-hez rendelt időzített átmeneti rendszer, q állapot a T(M)-ben. Definiálja g  AB(C)-re T(M), q |= g relációt! 99. Legyen M egy időzített automata az A akcióhalmaz, C órahalmaz és AP állapot tulajdonság halmaz felett, T(M) az M-hez rendelt időzített átmeneti rendszer, q állapot a T(M)-ben, f1 és f2 TCTL formulák. Definiálja T(M), q |= EUJ(f1, f2) relációt! 100. Legyen M egy időzített automata az A akcióhalmaz, C órahalmaz és AP állapot tulajdonság halmaz felett, T(M) az M-hez rendelt időzített átmeneti rendszer, q állapot a T(M)-nek, f1 és f2 TCTL formulák. Definiálja T(M), q |= AUJ(f1, f2) relációt! 101. TCTL logikában adja meg a szemantikáját az AF formulát jelöl! Mi lehet a formulában a k?

k

f formulának, ahol f egy TCTL

102. TCTL logikában adja meg az EUk (f, g) formula szemantikáját, ahol f és g egy-egy tetszőleges TCTL formula! Mi lehet a formulában a k? 103. Legyen M egy időzített automata az A akcióhalmaz, C órahalmaz és AP állapot tulajdonság halmaz felett, T(M) az M-hez rendelt időzített átmeneti rendszer, f egy TCTL formula az AP állapot atomi kijelentések és a C órahalmaz felett. Definiálja a T(M) |= f relációt! 104. Legyen M egy időzített automata az A akcióhalmaz, C órahalmaz és AP állapot tulajdonság halmaz felett, T(M) az M-hez rendelt időzített átmeneti rendszer, f egy TCTL formula az AP állapot atomi kijelentések és a C órahalmaz felett. Definiálja a M |= f relációt! 105. Mi a feladata a lokális, illetve a globális modell-ellenőrzésnek? 106. Mi a CTL modell-ellenőrzés feladata? 107. A CTL modell-ellenőrzés hogyan határozza meg adott átmeneti rendszer felett az EXf CTL formulát kielégítő állapotok halmazát? 108. A CTL modell-ellenőrzés hogyan határozza meg adott átmeneti rendszer felett az EU(f1, f2) CTL formulát kielégítő állapotok halmazát? 109. A CTL modell-ellenőrzés hogyan határozza meg adott átmeneti rendszer felett az EGf CTL formulát kielégítő állapotok halmazát? 110. Adja meg a CTL modell-ellenőrzést megvalósító címkéző eljárás időigényét! 111. Mit nevezünk modell-ellenőrzésnél állapotrobbanásnak? 112. Milyen modell-ellenőrzést nevezünk szimbolikus modell-ellenőrzésnek? 113. Definiálja adott változók halmaza felett a bináris döntési fát (BDF)! 114. Definiálja adott változók halmaza felett a bináris döntési diagramot (BDD)! 115. Adja meg az RBDD (vagyis redukált bináris döntési diagram) definícióját! 116. Definiálja adott változók halmaza felett a rendezett bináris döntési diagramot (OBDD)! 117. Definiálja adott változók halmaza felett a redukált rendezett bináris döntési diagramot (ROBDD)! 118. Definiálja változók egy X= {x1,…, xn}halmaza feletti t BDF által reprezentált t Boole-

függvényt!

6

119. Definiálja változók egy X= {x1,…, xn} halmaza feletti t BDD által reprezentált t Boole-

függvényt!

120. Adja meg azt a H halmazt, illetve  Boole-függvényt, melyet az alábbi f ROBDD reprezentál!

121. Adja meg az alábbi f ROBDD x2=0 szerinti projekcióját, vagyis az f[x2=0] ROBDD-t!

122. Adja meg az alábbi t1 OBDD-vel ekvivalens t ROBDD-t a redukáló algoritmus alapján!

123. Adja meg az alábbi f ROBDD x2= 1 szerinti projekcióját, vagyis f[x2= 1] ROBDD-t!

7

124. Adja meg, hogy a CTL szimbolikus modell-ellenőrzés hogyan reprezentálja az átmeneti rendszer állapotait és átmeneteit! 125. Definiálja az LTL modell-ellenőrzés alapfeladatát! 126. Definiálja a (kiterjesztett) Büchi-automatát és adott állapotból kiinduló számítási sorozatot egy végtelen szóhoz! 127. Legyen B = (Q, ,  , I, F) egy (kiterjesztett) Büchi-automata, ahol F={F1,…, Fk}, minden 1  i  k-ra Fi  Q és v  . Definiálja, hogy a v  szót mikor fogadja el a B Büchi-automata! 128. Ha megadhatók olyan Büchi-automaták, melyek az L1, illetve az L2 nyelvet ismerik fel, akkor megadható-e L1L2 nyelvet felismerő Büchi-automata? 129. Eldönthető-e minden Büchi-automata esetén, hogy az általa felismert nyelv üres-e vagy nem? 130. Milyen az LTL automata-elméleti alapú modell-ellenőrzés időbonyolultsága? 131. Adja meg az alábbi M Büchi-automata által felismert L(M) nyelvet!

132. Adja meg az alábbi M Büchi-automata által felismert L(M) nyelvet!

133. Legyen M = (S, T, , , Sx1,…, Sxn) egy (X, )-paraméteres átmeneti rendszer (X={x1, …, xn}), melyben minden sS állapotra van rákövetkező állapot és AP = {Px | x  X}. Milyen P(AP) feletti szót nevezünk egy c = s0, s1,… M-beli végtelen út lenyomatának? 134. Adja meg az alábbi {a, b} állapot tulajdonságok halmaza feletti A átmeneti rendszerhez azt a BA Büchi-automatát, melynek nyelve az A átmeneti rendszer kezdőállapotaiból induló végtelen utak lenyomatai (LTL modell-ellenőrzés 1. lépése alapján)! 8

135. Legyen f egy AP állapot tulajdonságok halmaza feletti LTL formula. Definiálja az f formulát kielégítő P(AP) feletti végtelen szavak halmazát (szavak(f))! 136. Adja meg az AP={a, b} feletti a LTL formulához azt a Ba Büchi-automatát, melyre teljesül, hogy L(Ba) = {v(P(AP)) | c végtelen út, c lenyomata v, c |= a}( az LTL modell-ellenőrzési algoritmus 2. lépése alapján)! 137. Adja meg az AP={a} feletti Xa LTL formulához azt a BXa Büchi-automatát, melyre teljesül, hogy L(BXa) = {v(P(AP)) | c végtelen út, c lenyomata v, c |= Xa }( az LTL modell-ellenőrzési algoritmus 2. lépése alapján)! 138. Adja meg az AP={a, b} feletti ab LTL formulához a Bab Büchi-automatát, melyre teljesül, hogy L(Bab) = {v( P(AP)) | c végtelen út, c lenyomata v, c |= ab }( az LTL modell-ellenőrzési algoritmus 2. lépése alapján)! 139. HML tabló-módszer alapú modell-ellenőrzésnek mi az alapfeladata? 140. HML tabló-módszer alapú modell-ellenőrzési algoritmus szerint az M, s |= f kielégítési relációhoz konstruálható szemantikus fa csúcsai mivel vannak címkézve? 141. HML tabló-módszer alapú modell-ellenőrzési algoritmus szerint az M, s |= f kielégítési relációhoz konstruálható szemantikus fát mikor nevezzük zártnak? 142. HML tabló-módszer alapú modell-ellenőrzési algoritmus szerint az M, s |= f kielégítési relációhoz konstruálható szemantikus fát mikor nevezzük nyitottnak? 143. Milyen következtetés vonható le, ha a HML tabló-módszer alapú modell-ellenőrzési algoritmus szerint az M, s |= f kielégítési relációhoz konstruált szemantikus fa nyitott? 144. Milyen következtetés vonható le, ha a HML tabló-módszer alapú modell-ellenőrzési algoritmus szerint az M, s |= f kielégítési relációhoz konstruált szemantikus fa zárt? 145. HML tabló-módszer alapú modell-ellenőrzésnél az M, s |= f kielégítési relációhoz hány szemantikus fa konstruálható, illetve ha több is konstruálható, akkor ezek között mi a kapcsolat? 146. Mi a TCTL modell-ellenőrzés alapfeladata? 147. A TCTL modell-ellenőrzés 1. lépése szerint hogyan eliminálhatók a vizsgált formulában előforduló operátorok idő-paraméterei? 148. Milyen formulák halmazát jelöli a TCTL0 a TCTL modell-ellenőrzés 1. lépésénél? 149. Definiálja a TCTL modell-ellenőrzés 2. lépésében alkalmazott óra-ekvivalencia relációt (o) a V(C) óraértékelések halmaza felett! 150. A TCTL modell-ellenőrzés 2. lépésében az óra-ekvivalencia reláció szerint egy osztályba tartozó óraértékelések az órafeltételek kielégítése szempontjából milyen tulajdonságúak? 151. A TCTL modell-ellenőrzés 2. lépésében az óra-ekvivalencia reláció szerinti osztályok száma milyen korlátok között van? 9

152. Definiálja a TCTL modell-ellenőrzés szerint az óra-régió leszármazott régióját! 153. Definiálja a TCTL modell-ellenőrzés szerint, hogy egy óra-régió mikor elégít ki egy órafeltételt! 154. Legyen C={x, y}, cx=2, cy=1 (cx az x, illetve cy az y órákra vonatkozó legnagyobb konstans az automatában és az adott formulában). Hány óra-régiója lesz az óraértékeléseknek a TCTL modell-ellenőrzés szerint? 155. Legyen C={x, y}, cx=2, cy=1 (cx az x, illetve cy az y órákra vonatkozó legnagyobb konstans az automatában és az adott formulában). Adjon meg legalább 5 óra-régiót a TCTL modell-ellenőrzés szerint! 156. Legyen C={x, y}, cx=2, cy=1 (cx az x, illetve cy az y órákra vonatkozó legnagyobb konstans az automatában és az adott formulában). Adja meg a TCTL modell-ellenőrzés szerint a [x=2, y1] óra-régió leszármazott régióját ([x=2, y1])! 157. Legyen C={x, y}, cx=2, cy=1 (cx az x, illetve cy az y órákra vonatkozó legnagyobb konstans az automatában és az adott formulában). Adja meg a TCTL modell-ellenőrzés szerint a [0<x<1, 0
174. Promela-ban milyen csatorna parancsok vannak, ezek működése hogyan történik? 175. Promela-ban az else, a timeout, a _pid változók jelentését adja meg! 176. Promela-ban hogyan lehet a rendszer folyamatait létrehozni? 177. Sorolja fel a Promela alaputasításait! 178. Adja meg a Promela nem-determinisztikus választást biztosító utasításnak a szintaxisát és működését! 179. Adja meg a Promela ciklikus nem-determinisztikus választást biztosító utasításának szintaxisát és működését! 180. Adja meg a Promela megszakíthatatlan (atomic) utasításának szintaxisát és működését! 181. Spin-ben az előrehaladási (progress) címke szerepe, illetve Non-progress módban mit vizsgál verifikációnál? 182. Spin-ben az elfogadási (accept) címke szerepe, a rendszer működésére vonatkozóan milyen tulajdonság vizsgálható alkalmazásakor? 183. Spin-ben az végállapot (end) címke szerepe, a rendszer működésére vonatkozóan milyen tulajdonság vizsgálható alkalmazásakor? 184. Spin-ben mi a soha-állítások (never claim) szerepe, mit lehet segítségükkel a rendszerre vonatkozóan vizsgálni? 185. Spin-ben milyen verifikációs módok vannak, az egyes verifikációs módokban a rendszer milyen tulajdonsága vizsgálható? 186. Milyen rendszereket nevezünk gyenge fair tulajdonságúnak? 187. Milyen rendszereket nevezünk erős fair tulajdonságúnak?

11