This paper presents an approach to the verification of temporal epistemic logic in synchronous multi-Agent systems via bounded model checking (BMC). By incorporating epistemic modalities into temporal logic CTL*, a temporal epistemic logic ECKL_n is introduced, and it is interpreted under the semantics of synchronous interpreted system. The temporal epistemic expressive power of ECKL_n is greater than that of Penczek and Lomuscio’s logic CTLK. Agents’ knowledge interpreted under synchronous semantics can be skillfully attained by the state position function, which avoids extending the encoding of the states and the transition relation of plain temporal epistemic model for time domain. The technical details and the correctness of the BMC method for logic AECKL_n/EECKL_n (the universal or existential fragment of ECKL_n) are given. A case study of train controller system is presented to illustrate the processing of the BMC method.