Bounded model checking for branching-time temporal logic

CORC > 北京大学 > 信息科学技术学院

	Bounded model checking for branching-time temporal logic
	Zhou Conghua ; Tao Zhihong ; Ding Decheng ; Wang Lifu
刊名	chinese journal of electronics
	2006
关键词	bounded model checking quantified Boolean formula (QBF) computation tree logic (CTL)
英文摘要	Bounded model checking (BMC) has been recently introduced as an efficient verification method for reactive systems. Propositional satisfiability (SAT)-based bounded model checking methods consists in searching for a counter- example of a particular length and generating a propositional formula that is satisfiable iff such a counterexample exists. Until now, SAT-based bounded model checking only concerns with universal properties. In this paper we focus on bounded model checking for Computation tree logic (CTL). We present how quantified Boolean decision procedures like Davis & Putnam Procedure can replaces Binary decision diagrams (BDDs). Our basic idea is to decide the validation of a CTL formula phi in finite executions of a system and reduce the validation to a Quantified Boolean formula (QBF) psi which is satisfiable if and only if phi is valid in finite executions of the system. QBF solvers based on Davis & Putnam Procedure do not blow up in space. Therefore, our new technique avoids the space blow up of BDDs, and sometimes speeds up the verification.; Engineering, Electrical & Electronic; SCI(E); EI; 1; ARTICLE; 4; 675-678; 15
语种	英语
内容类型	期刊论文
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/398270]
专题	信息科学技术学院
推荐引用方式 GB/T 7714	Zhou Conghua,Tao Zhihong,Ding Decheng,et al. Bounded model checking for branching-time temporal logic[J]. chinese journal of electronics,2006.
APA	Zhou Conghua,Tao Zhihong,Ding Decheng,&Wang Lifu.(2006).Bounded model checking for branching-time temporal logic.chinese journal of electronics.
MLA	Zhou Conghua,et al."Bounded model checking for branching-time temporal logic".chinese journal of electronics (2006).