ctlmodelchecking(編輯修改稿)
2024-08-11 18:16 本頁(yè)面
【文章內(nèi)容簡(jiǎn)介】 Model Checking by Fixpoint (5) For E(?U?), [[E(?U?)]] = ?Z.([[?]]?([[?]] ? ex(Z))) (6) For EG ?, [[EG ?]] = ?Z.([[?]] ? ex(Z)) Model Checking by Fixpoint M,s |= ? iff s ? [[?]] M |= ? iff I ? [[?]] Symbolic Model Checking CTL Symbolic Model Checking Kripke結(jié)構(gòu) OBDD([[?]]) 邏輯公式 OBDD OBDD運(yùn)算 Ｍ |= ? OBDD(I) ? OBDD([[?]]) Binary Decision Diagram (BDD) BDD = N,E,n0,L Labeling function: L: N L Root Edges: E: N N2 Nodes L ={a,…,c} a b c 1 0 Terminal Nodes: {0, 1} ? N 1 0 Intuitive Meaning [[w]] = (?a ? [[x]]) ? (a ? [[y]]) a y x w [[.]]: the meaning function Terminal node: [[0]] = 0 Terminal node: [[1]] = 1 Models Subset of L?L A model represents a state in a discrete system. M is a model of a BDD,
范文總結(jié)相關(guān)推薦
鄂ICP備17016276號(hào)-1