Abstract
We introduce a technique for model checking multi-agent systems against CTL*K specification using quantified Boolean formulas (QBF). We first define a bounded semantics for the logic CTL*K, and present a QBF encoding of the corresponding model checking problem. Based on this, we also implemented a tool which supports automated translation of model checking problems into QBFs, embedded in a tool chain with a QBF-solver providing certificates. We run our toolkit under different scenarios and present the experimental results obtained.