ctlmodelchecking-免費閱讀
【正文】 CTL Model Checking 張文輝 CTL Model Checking 遷移系統(tǒng) Kripke結(jié)構(gòu) CTL CTL Ｍ |= ? Ｍ |= ? 標(biāo)號算法 CTL Only consider CTL formulas with propositions, negation, disjunction, EX, EG, EU ? == p |?? | ??? |EX ? | EG ? | E(? U ?) Model Checking by Labeling Model Checking by Labeling Given M=S,R,I,L and ? Extend L(s) to contain all subformulas of ? that holds on s. Model Checking by Labeling (1) For a propositional subformula, nothing needs to be done. (2) For ??, add ?? to L(s), if ? ?L(s) Model Checking by Labeling (3) For ???, add ??? to L(s), if ? ?L(s) or ? ?L(s) (4) For EX?, add EX? to L(s), if ? ?L(s’) for some (s,s’)?R Model Checking by Labeling (5) For E(?U?), a) add E(?U?) to L(s), if ? ?L(s) b) add E(?U?) to L(s), if
范文總結(jié)相關(guān)推薦
鄂ICP備17016276號-1