Unknown user: Új oldal, tartalma: „{{GlobalTemplate|Infoalap|FormModVizsgaModEll}} %TOC{depth="3"}% ==Elmélet== ===Tableau módszer (szintaktikus): === * Fa sturktúra, csomópontokban formulák …”

2012-10-21T19:58:23Z

Új oldal, tartalma: „{{GlobalTemplate|Infoalap|FormModVizsgaModEll}} %TOC{depth="3"}% ==Elmélet== ===Tableau módszer (szintaktikus): === * Fa sturktúra, ** csomópontokban formulák ** …”

Új lap

{{GlobalTemplate|Infoalap|FormModVizsgaModEll}}

%TOC{depth="3"}%
==Elmélet==
===Tableau módszer (szintaktikus): ===
* Fa sturktúra,
** csomópontokban formulák
** él: továbblépési lehetőség
** gyökérben a bizonyítandó állítás negáltja.
* szabályok:
** és:
** vagy:
** aUb=b∨(a∧X(aUb))
** aRb=b∧(a∨X(aRb))
** Fa=a∨X(Fa)
** Ga=a∧X(Ga)
* Terminálás:
** zárt ág
** nyílt ág
** teljesség
** helyesség

'''Összefoglaló általános tanácsok a tabló módszerrel kapcsolatban:'''
A tabló-bizonyításos példa elég gyakori. Azt, hogy hogyan kell megcsinálni, ki lehet találni a =modelcheck=.* -ból

Ami onnan se derül ki, de fontos: ha egy G(p -> Fq) jellegű kifejezést akarsz
bebizonyítani, akkor a tablóban '''KÖR''' alakulhat ki, vagyis visszajutsz oda, hogy
ugyanazt az állítást kell bebizonyítanod, mint amit elkezdtél mar egyszer bebizonyítani. Ilyenkor, ha a tabló minden ága zárt, akkor két esetet kell megkülönböztetni. Ha nem zárt egy ág, akkor nyilván sikertelen a bizonyítás és hamis az állítás.
* Ha a kapott kör tényleges ciklust fejez ki a Kripke-struktúrán (!) is, mint ahogy a =modelcheck= végén van, akkor a bizonyítás ''SIKERTELEN'' , mert találtál egy soha nem terminálódó ágat, amin nem jutsz ellentmondásra (=> nem zárt), és tudsz mutatni egy utat (a Kripkében), amire nem teljesül az LTL kifejezés.
* Ha a kapott kör nem fejez ki tényleges kört a Kripke-struktúrán (ilyenre példa a G(érkezik -> F átmehet) a vasúti kereszteződés vizsgafeladatnál, ahol nyilvánvaló, hogy igaz, hiszen nem eshet végtelen ciklusba), akkor a bizonyítás ''SIKERES'' , mert azt mondhatod, hogy minden úton a zárt ágakba fogsz eljutni, és a tablóban lévő körök nem fejeznek ki valódi ciklust a Kripke-struktúrán. Ezt az utóbbi mondatot oda is kell írni a bizonyítás végére, különben pontot vonnak le.

===Szemantikus módszer===
===Automataelméleti megközelítés===

==Kérdések==

===1.===
'''Modellellenőrzést végzünk a tabló (tableau) módszer segítségével, melynek során az s |= X(Fp ^ q) LTL formulához jutottunk. Add meg a következő alkalmazandó tablóépítési szabályt!''' 
s-ből továbblépünk minden állapotba, ahova a Kripke struktúrában vezet él. Legyenek ezek s1,s2,... ekkor a következő szabály: s1|=(Fp ^ q) és s2=(Fp ^ q) ...

===2.===
'''Szimbolikus modellellenőrzést végzünk, melynek során az [[EFp]] CTL formulához jutottunk. Add meg mind fixpont, mind halmaziterációs alakban az adott CTL forumla kiszámításának általános módját.''' 

===3.===
'''Modellellenőrzést végzünk a tabló módszer segítségével, melynek során az s |= (Fp) R (-q) LTL formulához jutottunk. Add meg a következő lépésben alkalmazandó tablóépítési szabályt!(3 pont)'''
 
s |= (Fp) R (¬q) = 
¬(¬(Fp) U q) = 
''¬q és X((Fp) U q)'' 
Felhasználva, hogy pRq= ¬(¬pU¬q) és pUq= q v X(pUq). 

Vagy akár 
s |= Fp, ¬q s = ¬q, X( (Fp) R (¬q) )

==Igaz/Hamis==
==Példák==

-- [[AdamO|adamo]] - 2006.06.12.

[[Category:Infoalap]]

Modellellenőrzés - Laptörténet

Unknown user: Új oldal, tartalma: „{{GlobalTemplate|Infoalap|FormModVizsgaModEll}} %TOC{depth="3"}% ==Elmélet== ===Tableau módszer (szintaktikus): === * Fa sturktúra, ** csomópontokban formulák ** …”

Unknown user: Új oldal, tartalma: „{{GlobalTemplate|Infoalap|FormModVizsgaModEll}} %TOC{depth="3"}% ==Elmélet== ===Tableau módszer (szintaktikus): === * Fa sturktúra, csomópontokban formulák …”