Institutional Repository
| QBF encoding of temporal properties and QBF-based verification | |
| Zhang, Wenhui (1); Zhang, W.(zwh@ios.ac.cn) | |
| 2014 | |
| Conference Name | 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 |
| Pages | 224-239 |
| Conference Date | July 19, 2014 - July 22, 2014 |
| Conference Place | Vienna, Austria |
| Indexed Type | EI |
| Publish Place | Springer Verlag |
| ISSN | 3029743 |
| ISBN | 9783319085869 |
| Department | (1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, P.O. Box 8718, Beijing 100190, China |
| English Abstract | 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. |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16591 |
| Collection | 中国科学院软件研究所 |
| Corresponding Author | Zhang, W.(zwh@ios.ac.cn) |
| Recommended Citation GB/T 7714 | Zhang, Wenhui ,Zhang, W.. QBF encoding of temporal properties and QBF-based verification[C]. Springer Verlag,2014:224-239. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment