A Complete Epistemic Temporal Logic for Intelligent Agent

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.