无穷模型下PPTL公式可满足性判定算法
需积分: 10 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的模型检查和可满足性判定。这对于确保并发系统的正确性和安全性具有深远的意义,也为未来的理论研究和工程实践奠定了坚实的基础。
138 浏览量
106 浏览量
125 浏览量
2021-05-18 上传
104 浏览量
2021-01-22 上传
130 浏览量
105 浏览量
weixin_39841856
- 粉丝: 491
- 资源: 1万+
最新资源
- MFC2000-3A型微机厂用电快速切换装置使用说明书
- JavaScript+语言精髓与编程实践.pdf
- Pascal基础教程
- VC++6.0 MFC类库(中文版)
- router OS 功能介绍
- 电脑 小技巧 (让你使用电脑更轻松)
- 多线程编程指南.pdf
- ASP.NET与Web Service实例剖析中文版
- Optimizations od a MIMO relay network
- C案例分析-开发综合程序
- Iterative waterfilling for Gaussian vector multiple access channel
- 非常实用和详细介绍的mib信息库文件
- Infrastructure relay transmission with cooperative MIMO
- 巨著《管理学原理》PDF版
- oracle sql 优化
- Mutual information and minimum mean sqaured error in Gaussian channel