模型: Kripke Model Kripke Structure labeling function o Atomic Proposition,AP为原子命题集合 o Kripke Model: M=(S, So, R, L) 有穷状态集合 Sn∈S 初始状态 RcS×S 状态迁移 L:S→2AP 状态上的成真命题模型：Kripke Model ◼ Kripke Structure + Labeling Function  Atomic Proposition，AP为原子命题集合.  Kripke Model: M = (S, s0 , R, L) S 有穷状态集合 s0S 初始状态 RS  S 状态迁移 L: S→2AP 状态上的成真命题