基于谓词μ演算和空间逻辑的模型检测算法研究
模型检测是近二十几年来最成功的自动验证技术之一,一直以来主要用于检测时态逻辑,人们很少注意空间逻辑的模型检测问题,而在分布式系统领域,为了能够描述系统的空间结构性质,已经广泛地采用空间逻辑来描述.本文以带赋值符号迁移图和扩展的模态图分别作为并发系统和谓词μ演算的空间逻辑公式的语义模型来实现模型检测工具的工作.根据嵌套谓词等式系,将给出了公式转化成扩展的模态图,并根据模型检测算法来判断系统是否具有所描述的性质.同时结合实际例子说明如何利用嵌套谓词等式系将给定公式转化成扩展模态图.
模型检测 带赋值符号迁移图 谓词μ演算 空间逻辑 模态图
许梅 曹子宁
南京航空航天大学 信息技术学院,江苏 南京 210016
国内会议
南宁
中文
139-144
2009-09-18（万方平台首次上网日期，不代表论文的发表时间）