Modellellenőrzés

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

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

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) )

Példák

-- adamo - 2006.06.12.