模态逻辑视角下的模型检测理论

摘要

模型检测是逻辑学和计算机科学中的一个重要研究领域，作为模态逻辑的一个重要分支时间逻辑，它的繁荣发展就出现在这一领域。模型检测是关于时间逻辑判定问题的研究，其研究的两类实体一是关于刻画程序计算性质的逻辑公式，二是用来刻画程序的模型，模型检测的任务就是要校准这两种不同形式的信息——公式和模型——是否相一致。本文从模态逻辑的角度出发研究模型检测理论，并评价了它对模态逻辑的影响。