QCTL model-checking with QBF solvers
Abstract
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.
Keywords
Cite
@article{arxiv.2010.03185,
title = {QCTL model-checking with QBF solvers},
author = {A. Hossain and F. Laroussinie},
journal= {arXiv preprint arXiv:2010.03185},
year = {2020}
}
Comments
31 pages. arXiv admin note: substantial text overlap with arXiv:1906.10005