无穷模型下PPTL公式可满足性判定算法

需积分: 10 0 下载量 186 浏览量 更新于2024-07-17 收藏 636KB PDF 举报
本文主要探讨了命题投影时序逻辑(PPTL)在无限模型范围内的可满足性判定问题。PPTL是一种广泛应用于并发系统规格说明和验证的强大工具,特别是在处理区间时序逻辑(Interval Temporal Logic,ITL)的问题上。ITL的多个公理体系被提出,用于分析并发系统的性质,但传统的可验证性方法可能在面对无限模型时面临挑战。 在本文中,作者段振华和田聪首先提出了PPTL公式的标准范式(Normal Form, NF),这是一种标准化的形式化表示,有助于简化决策过程。标准范式图(Normal Form Graph, NFG)的概念也被引入,作为一种可视化工具,用于构建PPTL公式的有效结构,从而辅助判定其在无限模型中的可满足性。通过定义这些概念,作者设计了一个算法来构造PPTL公式的NFG,这个算法是解决可满足性问题的关键步骤。 决策过程的核心在于将复杂的PPTL公式转化为NFG,然后通过图的性质来判断是否存在一个无限模型使得公式成立。这涉及到对公式结构的深入理解,包括如何分解、合并和分析时间间隔的交互作用,以及如何处理无限时间序列的可能性。 举例说明部分展示了决策算法的具体应用,通过实际案例展示如何通过NFG的构建和分析来确定PPTL公式在无限模型中的可满足性。这种方法不仅适用于有限模型,而且对于那些包含无限行为的系统也具有普适性,因为NFG能够有效地处理无限时间的潜在复杂性。 这篇论文提供了一个重要的理论框架和实践方法,帮助研究人员和工程师更有效地在无限模型的背景下进行PPTL的模型检查和可满足性判定。这对于确保并发系统的正确性和安全性具有深远的意义,也为未来的理论研究和工程实践奠定了坚实的基础。