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

摘要

基于区间的时序逻辑,如区间时序逻辑(ITL)和投影时序逻辑(PTL),在并发系统的规范与验证方面有着重要的应用价值。然而,当前基于区间时序逻辑的程序验证主要是应用定理证明技术,自动化的模型检测技术尚未得到深入的研究。其原因是这类逻辑的模型理论不够完善,特别是它们的判定性、复杂性和表达性等问题尚未得到解决。
　　 因此,本文研究命题投影时序逻辑(PPTL)的判定性、复杂性、表达性以及模型检测算法。进一步,为了使用基于区间的时序逻辑来验证开放系统(Open Systems),本文提出了交互式区间时序逻辑(AITL)和交互式投影时序逻辑(APTL),并给出了相应的判定算法和模型检测方法。另外,为了提高模型检测的效率,缓解状态空间爆炸问题,本文给出了目前最好的打结不变(Stutter-Invariant)命题线性时序逻辑(PLTL)产生算法,以及新的抽象精化模型检测算法。
　　 本文的主要贡献如下:
　　 (1)定义了PPTL的正则形,证明了任意的PPTL公式都可以被转换成正则形。在正则形的基础上,定义了PPTL公式的正则图和带标记的正则图,证明了正则图和带标记的正则图的有穷性,进而证明了该逻辑的可满足性是可判定的,并给出了判定过程。作为判定算法的补充,给出了PPTL到单后继单项二阶逻辑(S1S)的转换,使得PPTL可以继承S1S成熟的理论结果。
　　 (2)通过将不带星的表达式的判空问题归约到PPTL的可满足性问题,证明了PPTL和PITL的复杂性是非基本的(non-elementary)。因此,本文给出的判定算法的复杂度也是非基本的。
　　 (3)给出了PPTL公式,打结Büchi自动机以及扩展的正则表达式之间的等价转换,证明了PPTL具有表达完全正则语言的能力。另外,研究了PPTL的一些子集,包括PITL,的表达能力,并将这些子集划分为五个不同的语言类。
　　 (4)在PPTL判定过程的基础上,通过进一步将带标记的正则图转换为Büchi自动机,给出了基于自动机理论的PPTL模型检测算法。应用该算法,开发了基于著名的模型检测工具SPIN的PPTL模型检测器。
　　 (5)以PTL的可执行子集,建模、仿真、验证语言MSVL,为系统建模语言,PPTL为性质描述语言,提出了基于可满足性(SAT)的统一框架模型检测方法。
　　 (6)通过将正则形技术应用于命题线性时序逻辑(PLTL),得到了目前最好的打结不变PLTL公式的产生算法。该算法在偏序规约模型检测中有着重要的应用价值。
　　 (7)给出了一个新的抽象精化模型检测算法,该算法不仅避免了抽象精化中的NP难问题,而且可以得到更小的精化模型,是对抽象模型检测的重要贡献。
　　 (8)为了使用基于区间的时序逻辑来对开放系统进行验证,将PITL和PPTL扩展到并发博弈结构,提出了交互式区间时序逻辑(AITL)和交互式投影时序逻辑(APTL),通过定义它们的正则形和正则图,给出了公式可满足性的判定算法和模型检测方法。