模型检验 OK Finite-state mode or Model Checker Error trace (→◇9) Line 12 Line 15 Temporal logic formula Line 21. Line Line 27
模型检验 Finite-state model Temporal logic formula Model Checker (F W) OK Error trace or Line 5: … Line 12: … Line 15:… Line 21:… Line 25:… Line 27:… … Line 41:… Line 47:…
模型: 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 有穷状态集合 s0S 初始状态 RS S 状态迁移 L: S→2AP 状态上的成真命题
Kripke Structure -Error start oven open door close door open door 器 start Close ERror ERror open do close door start oven start cooking cHeat -Heat Erro
Kripke Structure
Temporal logics Express properties of event orderings in time Branching Time Linear Time Every moment has several Every moment has a unique successors successor Infinite tree Infinite sequences(words) Computation Tree LogIc(CTL) Linear Temporal LogIc(LTL)
Temporal Logics ◼ Express properties of event orderings in time ◼ Linear Time ◼ Every moment has a unique successor ◼ Infinite sequences (words) ◼ Linear Temporal Logic (LTL) ◼ Branching Time ◼ Every moment has several successors ◼ Infinite tree ◼ Computation Tree Logic (CTL)
Path quantifiers and Temporal operators Path quantifiers o a(for all computation path o e(for some computation path) Temporal operators O XFG.UR Software Engineering Group 20
◼ Path quantifiers and Temporal operators ◼ Path quantifiers: A ( for all computation path ) E ( for some computation path ) ◼ Temporal operators: X, F, G, U, R Software Engineering Group 20