文章基本信息

标题：From Quantified CTL to QBF
本地全文：下载
作者：Akash Hossain ; Fran{\c{c}}ois Laroussinie
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：147
页码：1-20
DOI：10.4230/LIPIcs.TIME.2019.11
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：QCTL extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over Kripke structures (it is as expressive as MSO). Several semantics exist for the quantifications: here, we work with the structure semantics, where the extra propositions label the Kripke structure (and not its execution tree), and the model-checking problem is known to be PSPACE-complete in this framework. We propose a model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies, and we compare them with a prototype (based on the SMT-solver Z3) on several examples.
关键词：Model-checking; Quantified CTL; QBF solvers; SAT based model-checking