ctlmodelchecking-資料下載頁
2025-07-15 18:16本頁面
【正文】 Decision Diagram (ROBDD) Shared substructures No nodes have its left and right subtrees point to the same substructures Operations of ROBDD ?A A?B A?B A?B ? Propositional Formulas and OBDD Propositional Formula F ? OBDD(F) ? ROBDD(F) Kripke Structure and OBDD Given M=S,R,I,L and AP = { p1,p2,…,pk } S ? propositional formula R ? propositional formula I ? propositional formula [[p1]] ? propositional formula …, [[pk]] ? propositional formula Symbolic Model Checking Set operations are performed by corresponding ROBDD operations ex(..) .. \ .. .. ? .. .. ? .. [[?]]： Manipulation of OBDD CTL Symbolic Model Checking Kripke結構 OBDD([[?]]) 邏輯公式 OBDD OBDD運算 Ｍ |= ? OBDD(I) ? OBDD([[?]]) Variable Ordering Questions?
范文總結相關推薦
鄂ICP備17016276號-1