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.
Supported by the National Natural Science Foundation of China under Grant No. 61272135 and the 973 Program of China under Grant No. 2014CB340701.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS/ETAPS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Biere, A., Cimmatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers, vol. 58. Academic Press (2003)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. LICS, pp. 428–439 (1990)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A New Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press (1999)
Duan, Z., Tian, C., Yang, M., He, J.: Bounded Model Checking for Propositional Projection Temporal Logic. In: Du, D.-Z., Zhang, G. (eds.) COCOON 2013. LNCS, vol. 7936, pp. 591–602. Springer, Heidelberg (2013)
Emerson, E.A., Clarke, E.M.: Using Branching-time Temporal Logics to Synthesize Synchronization Skeletons. Sci. of Comp. Prog. 2(3), 241–266 (1982)
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “Not Never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)
Goultiaeva, A., Van Gelder, A., Bacchus, F.: A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas. In: IJCAI 2011, pp. 546–553 (2011)
Hoffmann, J., Gomes, C.P., Selman, B., Kautz, H.A.: SAT Encodings of State-Space Reachability Problems in Numeric Domains. In: IJCAI 2007, pp. 1918–1923 (2007)
Holzmann, G.J.: The model checker Spin. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Kemper, S.: SAT-based verification for timed component connectors. Sci. Comput. Program. 77(7-8), 779–798 (2012)
Kontchakov, R., Pulina, L., Sattler, U., Schneider, T., Selmer, P., Wolter, F., Zakharyaschev, M.: Minimal Module Extraction from DL-Lite Ontologies Using QBF Solvers. In: IJCAI 2009, pp. 836–841 (2009)
Penczek, W., Wozna, B., Zbrzezny, A.: Bounded Model Checking for the Universal Fragment of CTL. Fundamenta Informaticae 51, 135–156 (2002)
Wozna, B.: ATCL* properties and Bounded Model Checking. Fundam. Inform. 63(1), 65–87 (2004)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher (1993)
Peled, D.A.: Software Reliability Methods. Springer (2001)
Peterson, G.L.: Myths About the Mutual Exclusion Problem. Information Processing Letters 12(3), 115–116 (1981)
Zhang, W.: Bounded Semantics of CTL and SAT-based Verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 286–305. Springer, Heidelberg (2009)
Zhang, W.: Bounded Semantics of CTL. Institute of Software, Chinese Academy of Sciences. Technical Report ISCAS-LCS-10-16 (2010)
Zhang, W.: VERDS modeling language, http://lcs.ios.ac.cn/~zwh/verds/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Zhang, W. (2014). QBF Encoding of Temporal Properties and QBF-Based Verification. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-08587-6_16
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08586-9
Online ISBN: 978-3-319-08587-6
eBook Packages: Computer ScienceComputer Science (R0)