模型检测原理：dual-language approach Yes or Real-world system Finite-state model X No Model checker AGb1ow吧 Desired property Logic formula more detailed 工 more abstract “implementation" “specification'" (system model) (system property) 'satisfies","implements","refines" (satisfaction relation)模型检测原理：dual-language approach 9/112