Abstract: Model checking of hyperproperties is an important research topic in formal verification. HyperCTL* extends Computation Tree Logic (CTL*) by explicitly quantifying properties over multiple execution paths of a system. To address the issue of high time complexity in HyperCTL* model check- ing, this study first proposes a bounded semantics for HyperCTL*, followed by a bounded model check- ing algorithm based on quantified Boolean formulas. The correctness of this algorithm  is analyzed, and finally, a prototype system for HyperCTL* bounded model checking tool, named Hybmc, was implemented. Experimental results demonstrate that the efficiency of Hybmc’s bounded model checking significantly outperforms that of HyperQube, a bounded model checking tool for HyperLTL.

Key words: Hyper computation tree logic(HyperCTL*), bounded model checking, quantified Boolean formula(QBF)