[討論] 正規方法考題
老師上課有說要考什麼我大概抄了一下，有些太趕沒抄到，大家有抄的話把他補齊吧!
1. theorem-proving problem 好像是考一整個流程 give formula construct
Helbrand...
2. model checking problem 似乎是要考期末project做的東西的原理? p83
3. one problem from Chap 3 about theorem proving 上次考的要再考一次的樣子
只是我上次這個都不會寫 囧rz
4. Interpretation of formula in Kripke structure (Chap4 p46s頁附近的東西)
5. State Postcondition (rule for command 3 ? ) [Chap4 p27p28]
Caculation of the post state after the while loop after one iteration
6. write single program for the Kripke structrure [Chap4 p39,p40]
7. Greastest fix point analysis [Chap4 p88,p89]
Kripke structure safety analysis(label which node is reachable by formula)
8. symbolic precondition ( symbolic liveness analysis ) [Chap4 p98]
(given the formula of ita) <-ita 就是長的像n那個符號
9. Intersecting (composition) of two Buchi automata [Chap4 p150-152]
10. write LTL spec, write CTL spec, write CTL* spec, build trees to
discriminate CTL* formulas
contruct a tree that is satisfy by one formula but not satisfy
by another formula
11. Buchi automata translation of CPTL formulas [Chap5 p113,p125]
Labeling algorithm of CTL formulas
-------------------------------------------------
接下來是不確定會不會考出來的東西，老師好像覺得太多題了
symbolic model checking with BDD p139
Timed automata description (give spec draw timed automata) 6-35
TCTL spec.
Region construction 6-61,62
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 140.112.42.245
※ 編輯: wolftail 來自: 140.112.42.245 (06/25 15:51)
※ 編輯: wolftail 來自: 140.112.42.245 (06/25 16:16)