命题投影时序逻辑的判定性、复杂性、表达性及模型检测

发布时间：2022-01-26 11:33

　　基于区间的时序逻辑,如区间时序逻辑（ITL）和投影时序逻辑（PTL）,在并发系统的规范与验证方面有着重要的应用价值。然而,当前基于区间时序逻辑的程序验证主要是应用定理证明技术,自动化的模型检测技术尚未得到深入的研究。其原因是这类逻辑的模型理论不够完善,特别是它们的判定性、复杂性和表达性等问题尚未得到解决。因此,本文研究命题投影时序逻辑（PPTL）的判定性、复杂性、表达性以及模型检测算法。进一步,为了使用基于区间的时序逻辑来验证开放系统（Open Systems）,本文提出了交互式区间时序逻辑（AITL）和交互式投影时序逻辑（APTL）,并给出了相应的判定算法和模型检测方法。另外,为了提高模型检测的效率,缓解状态空间爆炸问题,本文给出了目前最好的打结不变（Stutter-Invariant）命题线性时序逻辑（PLTL）产生算法,以及新的抽象精化模型检测算法。本文的主要贡献如下：（1）定义了PPTL的正则形,证明了任意的PPTL公式都可以被转换成正则形。在正则形的基础上,定义了PPTL公式的正则图和带标记的正则图,证明了正则图和带标记的正则图的有穷性,进而证明了该逻辑的可满足性是可判定的,... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：169 页

【学位级别】：博士

【部分图文】：

尸VQ的NFG

第5章PPTL的表达性L(ehop)〔L(next，e卜op)C门L(ehop，ehop*)CL(next，ehop，prj④)=}}L(neXt，ehop，ehop*，pFj)=L(next，prj)门L(next，ehop，ehop*)}}L(next，prj，ehop*)=L(next，prj，prj④)L(next，ehop，ehop*，prj④)}}L(next，ehop，e卜op*，prj，prj④)图5.5PPTL及子集的关系Star一freeregularIanguage

并进一步构造出二尸的B位chi自动机A一，。我们可以通过构造A，和A一，的积自动机，然后判断该积自动机所接收的语言是否为空来验证系统是否满足期望的性质，如图6.1所示。如果积自动机可接收的语言为空，那么系统就满足期望的性质，否则图6.1基于自动机的PPTL模型检测系统不满足期望的性质，并给出一个反例。SPIN已经实现了一个将线性时序逻辑公式自动转换为永非断言的转换器。为了在SPIN中实现基于PPTL的模型检测，我们也提供了一个由PPTL公式向永非断言转换的转换器，如图6.2所示。根据前面的章节中提出的算法，我们已经用C++实现了该转换器，并成功地将其集成到了原始的SPIN中。6.2复杂性讨论在第四章中，我们通过将不带星表达式的判空问题{86」规约到PPTL公式的可满足性问题


本文编号：3610420