线性Mu演算子集的判定过程

摘要

时序逻辑在程序验证和人工智能的规划领域都起着至关重要的作用。作为最具代表性的时序逻辑之一，线性时序逻辑(Linear Temporal Logic，LTL)已被广泛应用于反应系统和并发系统的性质声明和验证，以及规划问题中时序延展目标的表示。虽然LTL使用方便，但是其表达能力仅为无星正则。因此，一些重要的性质无法通过LTL公式来描述。线性μ演算(Linear Timeμ-Calculus，νTL)以最小和最大不动点操作符扩展了LTL，其语法简洁，并且能够表达所有ω正则性质。不动点不仅能够很好地刻画系统的递归和无穷行为，而且可以表达比LTL更多的时序性质。然而，不动点操作符的嵌套使得νTL的判定问题难于求解，这阻碍了νTL在实际中的应用。为此，本文研究了νTL的两个子集，G-mu和解释在有穷迹上的νTL(νTL interpreted overfinite traces，νTLf)，并且给出了这些子集的高效判定过程。
　　通过限制νTL公式中各最小不动点子公式的出现，本文定义了G-mu，给出了从任意ω正则表达式到封闭的G-mu公式的转换函数，从而证明了其表达能力为ω正则。接着，本文定义了G-mu公式的目标前进范式(Goal Progression Form，GPF)，证明了任意封闭的G-mu公式均能转化为该范式。GPF将一个公式分解为当前部分和未来部分：当前部分是原子命题或它们的非的合取式，表明当前状态应该满足的条件；未来部分是给定公式的闭包中元素的合取式，表明下一状态应该满足的条件。基于GPF，本文定义了目标前进范式图(Goal Progression Form Graph，GPG)，用以描述公式的模型，并且提出了范式图的构造算法。基于GPG，本文给出了一个用以判断G-mu公式可满足性的直观判定过程。该判定过程是通过在GPG中寻找ν-路径(即不包含最小不动点无穷展开的路径)而实现，时间复杂度为2O(|?|)。因此，G-mu和LTL的判定问题具有相同的时间复杂度。然而，相比于LTL，G-mu能够描述更多的时序性质。此外，本文给出了Kripke结构与GPG的乘积的构造算法，并且将GPG中ν-路径的概念应用到乘积图中，最后得到了一种基于GPG的模型检测方法。
　　本文研究的另一个νTL子集为νTLf，它以最小和最大不动点操作符扩展了解释在有穷迹上的LTL(LTL interpreted over finite traces，LTLf)。首先，本文定义了νTLf公式的当前未来范式(Present Future Form，PFF)，证明了任意封闭的νTLf公式均能转化为该范式，并且给出了从νTLf公式到PFF的转化算法。与GPF相似，PFF同样将一个公式分解为两部分：当前状态应该满足的条件和下一状态应该满足的条件。基于PFF，本文提出了当前未来范式图(Present Future Form Graph，PFG)的构造算法。PFG能够用于描述公式的模型。此外，本文证明了一个封闭的νTLf公式是可满足的当且仅当该公式的PFG中存在一条ε-路径。因此，νTLf公式的可满足性问题能够被转化为PFG中的ε-路径搜索问题，该问题能够被进一步转化为检查PFG中是否存在ε节点的问题。最后，得到了一个时间复杂度为2O(|?|)的基于PFG的判定过程，用以检查νTLf公式的可满足性，并且据此得到了一种相应的模型检测方法。这使得νTLf非常适用于规划问题中时序延展目标的表示。
　　奇偶博弈求解问题多项式时间内等价于μ演算模型检测问题。更好的奇偶博弈求解算法可能促进更好的模型检测器的产生。因此，本文还给出了一种求解奇偶博弈问题的改进递归算法，以减少递归调用总次数。为此，一方面，定义了原子获胜区域，给出了一个预处理算法，用以找出原子获胜区域并在这些区域给后续的递归带来不利影响之前将它们从图中删除。另一方面，在原有递归算法中的第二个递归调用之前插入了一条额外的条件语句。当该条件成立时，能够利用递归过程中产生的一些中间结果直接得到获胜区域，无需执行第二个递归调用。

目录

声明

List of Figures

List of Tables

List of Symbols

List of Abbreviations

Chapter 1 Introduction

1.1 Formal Verification

1.2 Temporal Logic

1.3 Parity Games

1.4 Contributions

1.5 The Organization of the Thesis

Chapter 2 Preliminaries

2.1 Syntax of ν TL

2.2 Semantics of ν TL

2.3 The Fragment G-mu

2.4 ν TLf

2.5 Basic Notions of Parity Games

2.6 Summary

Chapter 3 The Expressive Power of G-mu

3.1 Comparison with D-mu

3.2 Regular Expressions andω-Regular Expressions

3.3 Translatingω-Regular Expressions into G-mu Formulas

3.4 Summary

Chapter 4 A Decision Procedure for G-mu

4.1 GPF of G-mu Formulas

4.2 Goal Progression Form Graph

4.3 A Decision Procedure Based on GPG

4.4 Model Checking Based on GPG

4.5 Related Work

4.6 Summary

Chapter 5 A Decision Procedure forνTLf

5.1 PFF ofνTLf Formulas

5.2 Present Future Form Graph

5.3 A Decision Procedure Based on PFG

5.4 Model Checking Based on PFG

5.5 Summary

Chapter 6 An Improved Recursive Algorithm for Parity Games

6.1 The Recursive Algorithm for Parity Games

6.2 A Preprocessing Algorithm for Parity Games

6.3 The Recursive Algorithm with an Extra Conditional Statement

6.4 Related Work

6.5 Summary

Chapter 7 Conclusions and Future Works

7.1 Conclusions

7.2 Future Works

参考文献

致谢

Biography