During the past two decades Model Checking based on Kripke Semantics Structure has proven its efficacy and powerful in circuit design，network protocol analysis，program verification and bug bunting．Recently there has been considerable research on Model Checking without OBDDs such as using SAT Solver or Bounded Model Checking (BMC). A Dynamic Kxipke Semantics Structure is introduced through allow the AP set changed．Based on this method．a new direct model checking algodthm is proposed．