摘要
模型检测是逻辑学和计算机科学中的一个重要研究领域,作为模态逻辑的一个重要分支时间逻辑,它的繁荣发展就出现在这一领域。模型检测是关于时间逻辑判定问题的研究,其研究的两类实体:一是关于刻画程序计算性质的逻辑公式,二是用来刻画程序的模型,模型检测的任务就是要校准这两种不同形式的信息——公式和模型——是否相一致。
Model checking theory is a cross-cutting areas of Logic and Computer Science.Temporal logic acts as an important branch of modal logic,its spectacular development appeared in this area.Model checking is about the study of decision problem of temporal logic,and two types of entities are involved,one is logic formula used to discribe a programs computational properties,the other is the model used to describe a program.The task of model checking is to calibrate these two different forms of information—the formula and the model—is conformed or not.This paper studies model checking theory from the point of modal logical view,and evaluate its affect on modal logical.
