通常的分析方法是：list/table represent the state space
symbolic 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 method
trace automaton method
behavior machines method
time Petri Nets methos Yoneda. et. al. 1989
characteristic: do not involve interleaving of actions
symbolic model solves:
derive efficient decision procedure for CTL model checking
satisfiability of linear-time temporal logic formulas
strong and weak observational equivalence of finite transition systems
language containment for finite ω-automata
阅读(355) | 评论(0) | 转发(0) |
