State explosion problem is the main obstacle of model checking. This problem is addressed in the paper from a coalgebraic point of view. By coninduction principle, the paper proves that: (1) Given any class of Kripke Structures (denoted by K), there exists a unique smallest Kripke structure (denoted by K₀) with respect to bisimilarity which describes all behaviors of the Kripke structures with no redundancy. (2) For any Kripke Structure M∈K (the state space of M may be infinite), there exists a unique concrete smallest Kripke structure K_M. Base on this idea, an algorithm is established for minimization of Kripke Structures. A naive implementation of this algorithm is developed in Ocaml. One of its applications is that instead of M, K_M can be used with a smaller state space to verify properties for M in the process of Model Checking.