Symbolic Model Checking : IO * ’ States and Beyond *
Symbolic Model Checking : IO * ’ States and Beyond *
复制标题
符号模型检查：IO *’状态及其他*
DOI：
--
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
L. Hwang
中科院分区：
文献类型：
--
作者：
J. Burch;E. Clarke;K. McMillan;D. Dill;L. Hwang
通过检查系统行为的状态图模型，已经设计了许多不同的方法来自动验证有限状态系统。我们描述了一种代表状态空间对称/y而不是明确的方法。规格语言。检查算法可用于得出有效的CTL模型检查，线性时间临时逻辑公式的满意度，强和弱的观测有限的过渡系统和有限的W-Automata的语言遏制有时是复杂的。讨论如何使用简单的同步管道电路
Many different methods have been devised for automatically verifying finite state systems by examining state-graph models of system behavior. These methods all depend on decision procedures that explicitly represent the state space using a list or a table that grows in proportion to the number of states. We describe a general method that represents the state space symbolical/y instead of explicitly. The generality of our method comes from using a dialect of the Mu-Calculus as the primary specification language. We describe a model checking algorithm for MuCalculus formulas that uses Bryant’s Binary Decision Diagrams (Bryant, R. E., 1986, IEEE Trans. Comput. C-35) to represent relations and formulas. We then show how our new Mu-Calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satistiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment for finite w-automata. The fixed point computations for each decision procedure are sometimes complex. but can be concisely expressed in the Mu-Calculus. We illustrate the practicality of our approach to symbolic model checking by discussing how it can be used to verify a simple synchronous pipeline circuit. 1%’ 1992 Academic Press. Inc