命题动态逻辑模型检测技术及应用研究

摘要

命题动态逻辑(propositional dynamic logic.简称PDL)最初是由Fischer和Ladner在上世纪70年代末引入的,已成为计算机科学中一种有价值的理论工具。PDL不但用于程序形式化描述和推理,而且还能够提供合适的形式框架对动作进行刻画和推理,是在此基础上进行规划求解的一种有效工具。PDL模型检测是对程序或动作进行形式化规约和验证的有效方式,现有的模型检测算法是基于关系矩阵表示和实现。基于 OBDD的符号技术极大的提高了模型检测的效率,在时态逻辑模型检测中取得了成功的应用。为了使符号技术应用于命题动态逻辑模型检测,提高PDL模型检测的效率,本文对PDL符号模型检测技术进行了研究。在此基础上,针对PDL规划问题,本文研究了符号模型检测技术在PDL规划求解中的应用。本文的具体研究成果如下:
　　(1)给出了基于OBDD的PDL模型检测算法。在分析其他逻辑符号模型检测方法的基础上,建立了基于OBDD的PDL符号模型;给出了基于OBDD的PDL模型检测算法;证明和实例验证该算法是正确可行的;实验说明,PDL规范可以采用符号技术进行有效的验证。
　　(2)设计并实现了PDL符号模型检测工具。借鉴时态逻辑模型检测工具的实现方法,设计并实现了PDL符号模型检测工具,能够对正则PDL公式进行模型检测;实验表明,PDL符号模型检测工具的效率优于现有的PDL模型检测工具。
　　(3)提出了基于模型检测求解PDL规划算法。应用PDL去描述规划问题,论证了PDL规划可以通过模型检测的方法求解;给出基于模型检测的PDL规划符号算法;结合实例验证算法的正确性。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪 论

§1.1 研究背景及意义

§1.2 研究目的及内容

§1.3国内外研究现状

§1.4 论文安排

第二章 预备知识

§2.1 命题动态逻辑

§2.2有序二叉决策图（OBDD）

§2.3集合的OBDD表示

§2.4 BuDDy软件包

第三章 命题动态逻辑符号模型检测

§3.1引言

§3.2PDL模型的OBDD 表示

§3.3 PDL符号模型检测算法

§3.4 PDL模型检测过程示例

§3.5 实验结果

§3.6 小结

第四章 PDL符号模型检测工具的设计与实现

§4.1 引 言

§4.2 PDL符号模型检测工具的体系结构

§4.3 PDL模型规约语言

§4.4 Lex 和 Yacc

§4.5 PDL符号模型检测工具的实现

§4.6 PDL符号模型检测工具效率分析

§4.7 小结

第五章 基于模型检测的命题动态逻辑规划

§5.1 引言

§5.2 规划表示

§5.4 基于模型检测求解PDL规划

§5.5 小结

第六章 结束语

§6.1主要研究成果

§6.2 相关研究展望

参考文献

致谢

附录：读研期间所完成的学术论文