symbolic model checking notations

meshmore

通常的分析方法是：list/table represent the state spacesymbolic model: represent the state space symbolically
Temoral Logic    ↓μ calculus
    ↓symbolic model  (using Bryant's Binary Decision Diagram)
对于Petri Net的分析与很多图的分析，在活性上是相通的
BDDs do not prevent explosion in all cases.solves 1020 states, usually 108
1989 BDD based algorith for CTL model checking    --  applicable to synchronous circuits, but not to asynchronous circuits, or infinite computations, such as liveness, fairness.
symbolic model       based on interative computation of fixed point 固定点的迭代计算 --- 有点像暑假里unfolding算法中确定cut point
some methods:stubborn sets methodtrace automaton methodbehavior machines methodtime Petri Nets methos Yoneda. et. al. 1989
characteristic: do not involve interleaving of actions
symbolic model solves:derive efficient decision procedure for CTL model checkingsatisfiability of linear-time temporal logic formulasstrong and weak observational equivalence of finite transition systemslanguage containment for finite ω-automata
               
               
               
               

本文来自ChinaUnix博客，如果查看原文请点：http://blog.chinaunix.net/u3/108378/showart_2128920.html