QBF encoding of temporal properties and QBF-based verification

ISCAS OpenIR

	QBF encoding of temporal properties and QBF-based verification
	Zhang, Wenhui (1); Zhang, W.(zwh@ios.ac.cn)
	2014
会议名称	7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
页码	224-239
会议日期	July 19, 2014 - July 22, 2014
会议地点	Vienna, Austria
收录类别	EI
出版地	Springer Verlag
ISSN	3029743
ISBN	9783319085869
部门归属	(1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O. Box 8718, Beijing 100190, China
摘要	SAT and QBF solving techniques have applications in various areas. One area of the applications of SAT-solving is formal verification of temporal properties of transition system models. Because of the restriction on the structure of formulas, complicated verification problems cannot be naturally represented with SAT-formulas succinctly. This paper investigates QBF-applications in this area, aiming at the verification of branching-time temporal logic properties of transition system models. The focus of this paper is on temporal logic properties specified by the extended computation tree logic that allows some sort of fairness, and the main contribution of this paper is a bounded semantics for the extended computation tree logic. A QBF encoding of the temporal logic is then developed from the definition of the bounded semantics, and an implementation of QBF-based verification follows from the QBF encoding. Experimental evaluation of the feasibility and the computational properties of such a QBF-based verification algorithm is reported. © 2014 Springer International Publishing Switzerland.; SAT and QBF solving techniques have applications in various areas. One area of the applications of SAT-solving is formal verification of temporal properties of transition system models. Because of the restriction on the structure of formulas, complicated verification problems cannot be naturally represented with SAT-formulas succinctly. This paper investigates QBF-applications in this area, aiming at the verification of branching-time temporal logic properties of transition system models. The focus of this paper is on temporal logic properties specified by the extended computation tree logic that allows some sort of fairness, and the main contribution of this paper is a bounded semantics for the extended computation tree logic. A QBF encoding of the temporal logic is then developed from the definition of the bounded semantics, and an implementation of QBF-based verification follows from the QBF encoding. Experimental evaluation of the feasibility and the computational properties of such a QBF-based verification algorithm is reported. © 2014 Springer International Publishing Switzerland.
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16591
专题	中国科学院软件研究所
通讯作者	Zhang, W.(zwh@ios.ac.cn)
推荐引用方式 GB/T 7714	Zhang, Wenhui ,Zhang, W.. QBF encoding of temporal properties and QBF-based verification[C]. Springer Verlag,2014:224-239.