论文部分内容阅读
本论文主要研究形式规范语言命题动态逻辑(PropositionalDynamicLogic)的可分解（组合）性及其递归扩展，以及相关的一些判定性问题。
命题动态逻辑是一个经典的形式规范语言，它在七十年代末由Fischer和Ladner引入，用来描述程序的推理。命题动态逻辑使用正规表达式来描述程序，可以描述一定的路径递归模式。
可满足性问题是指对于给定的命题动态逻辑公式，是否存在模型，其中的某个状态满足给定公式。对于命题动态逻辑的可满足性问题，经典的判定算法是:在给定命题的Fischer-Ladner闭包的基础上构造模型，逐渐删除存在不协调的状态，最终得到一个协调的模型。对于可满足的命题，算法可以给出一个模型，使得目标命题在其中某个状态得到满足。我们给出该算法的一个不同的正确性证明。基于我们的证明，不仅可以给出可满足命题的模型，而且对于不可满足的命题，我们可以给出其逆命题的一个推导证明。由此我们可以得到一个命题动态逻辑的推演系统的完备性的构造性证明。
分解与组合问题所要解决的问题是将一个联合系统的规范降低为系统的组成部分的规范，以及将系统组成部分的规范组合成整个系统的规范的问题。（正规）命题动态逻辑的程序用正规表达式描述，其可分解问题可解，但是程序的大小会出现一个指数级的膨胀。本论文中，我们研究自动机命题动态逻辑，它用自动机代替正规表达式，来描述命题动态逻辑的程序。由于正规自动机与正规表达式之间存在一一对应的关系，因此自动机命题动态逻辑与（正规）命题动态逻辑的表达能力等价。我们证明，自动机命题动态逻辑在一大类上下文下具有很好的可分解（组合）性。
通常对于一个规范语言，一方面我们希望它的表达能力很强，能够表示更多的性质，另一方面我们又希望它不要太复杂，以方便对于它所表示的性质进行分析验证。命题动态逻辑虽然表达能力比较弱，但是它将命题和程序分开表示，清晰易懂，分析与验证也很简单。因此我们希望在保持命题动态逻辑的优点的基础上，一定程度的增强其表达能力。在本论文中，我们在自动机命题动态逻辑的基础上，用递归命题对其进行扩展，增强它的表达能力，扩展后的逻辑我们称为递归命题动态逻辑。在递归命题动态逻辑中，我们将原子命题扩充为两类:一类是与原来一样，由模型定义其语义的原子命题;另一类是由递归声明定义的命题变量。我们可以证明，通过这样的扩展之后得到的逻辑，表达能力比计算树逻辑要强，同时也没有超过μ一演算的一层迭代子集。经过扩展后的递归命题动态逻辑在单空上下文下，依然具有很好的可分解（组合）性。
对于递归命题动态逻辑的一类我们称为简单公式的子集，我们给出一个优化的可满足性判定算法。这个判定算法的最坏时间复杂度与命题的大小成指数级别相关，与程序的大小成多项式级别相关。简单命题可以描述各种互模拟等价类（强互模拟等价～、弱互模拟等价≈、分支互模拟等价≈b等等）。因此我们可以结合递归命题动态逻辑的可分解（组合）性，用上面的算法来求解互模拟等价方程。同时，对于递归命题动态逻辑中的正命题，都存在一个相对应的简单命题，因此我们可以把正命题翻译到简单命题之后来求解它的可满足性。