In this paper, we present a complete epistemic temporal logic, called BPICTL, which generalizes CTL by introducing epistemic modalities. A sound and complete inference system of BPICTL is given. We prove the finite model property of BPICTL. Furthermore, we present a model checking algorithm for BPICTL.

翻译：本文提出了一种称为BPICTL的完备认知时序逻辑，该逻辑通过引入认知模态词对CTL进行了扩展。我们给出了BPICTL的一个可靠且完备的推理系统，并证明了BPICTL具有有限模型性质。此外，本文还提出了针对BPICTL的模型检测算法。