Abstract
For temporal and epistemic property CTLK we propose a new symbolic model checking technique based on Quantified Boolean Formula(QBF). The verification approach is based on an adaption of the technique of bounded model checking. We decide the validity of a CTLK formula ψ in the finite reachable state space of a system, and reduce the validity to a QBF which is satisfiable if and only if ψ is validated. The new technique avoids the space blow up of BDDs, and sometimes speeds up the verification. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Zhou, C., Chen, Z., & Tao, Z. (2007). QBF-based symbolic model checking for knowledge and time. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4484 LNCS, pp. 389–397). Springer Verlag. https://doi.org/10.1007/978-3-540-72504-6_35
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
