ctlmodelchecking(存儲(chǔ)版)
【正文】 ? ?L(s) and E(?U?) ?L(s’) for some (s,s’)?R (c) repeat b until L does not change Model Checking by Labeling (6) For EG ?, a) pute S’={s | ? ?L(s)} b) pute nontrivial SCCs of the subgraph induced by S’。 for every s in such an SCC, add EG? to L(s). c) add EG ? to L(s), if s ?S’ and EG ?L(s’) for some (s,s’)?R (d) repeat c until L does not change Model Checking by Labeling M,s |= ? iff ? ?L(s) M |= ? iff ? ?L(s) for every s ? I. CTL Symbolic Model Checking 遷移系統(tǒng) Kripke結(jié)構(gòu) CTL CTL 狀態(tài)集合 Ｍ |= ? Ｍ |= ? I ? [[?]] Fixpoint Model Checking by Fixpoint (1) For a propositional subformula p, [[p]] = { s | p ?L(s) } (2) For ??, [[??]] = S \ [[?]] Model Checking by Fixpoint (3) For ???, [[???]] =[[?] ? [[?]] (4) For EX?, [[EX?]] = ex([[?]])
范文總結(jié)相關(guān)推薦
鄂ICP備17016276號(hào)-1