Bounded Model Checking of CTL

Research paper by Zhi-Hong Tao, Cong-Hua Zhou, Zhong Chen, Li-Fu Wang

Indexed on: 14 Feb '07Published on: 14 Feb '07Published in: Journal of Computer Science and Technology


Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this paper we first present how quantified Boolean decision procedures can replace BDDs. We introduce a bounded model checking procedure for temporal logic CTL* which reduces model checking to the satisfiability of quantified Boolean formulas. Our new technique avoids the space blow up of BDDs, and extends the concept of bounded model checking.