论文标题
QCTL模型检查使用QBF求解器
QCTL model-checking with QBF solvers
论文作者
论文摘要
量化的CTL（QCTL）扩展了时间逻辑CTL，并具有对原子命题的定量。已知该扩展非常表现力：QCTL使我们能够在Kripke结构上表达复杂的特性（它与MSO一样表达）。有几种量化的语义：在这里，我们与结构语义合作，其中额外的命题标记了kripke结构（而不是其执行树），并且已知模型检查问题在此框架中是pspace-complete。我们提出了一种基于QBF降低的QCTL的新模型检查算法。我们考虑了几种还原策略，并将它们与不同示例的原型（基于几个QBF求解器）进行了比较。
Quantified CTL (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 new 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 several QBF solvers) on different examples.
