A Framework for Model Checking Against CTLK Using Quantified Boolean Formulas.
FTSCS(2019)
摘要
We present a novel bounded model checking (BMC) tool chain for multi-agent systems. This framework automatically translates the verification of system models against properties formulated in computation tree logics with epistemic modalities (CTLK) into quantified Boolean formulas (QBFs). Our framework exploits recent QBF technology for solving those verification problems and for certifying the result, making the implementation of a dedicated CTLK solver obsolete. The translation to QBF is based on existing theoretical work and implemented in our novel tool which extends the open-source model checker MCMAS. First experimental results are very promising and indicate the practical feasibility of our approach. Furthermore we provide novel benchmarks to the QBF community.
更多查看译文
关键词
model checking,ctlk
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络