论文部分内容阅读
以μ演算方法研究命题时序逻辑模型，设计实现了命题μ演算中μ演算公式输入以及对输入公式的检查、编译、分析和计算，并通过模型输入及岸演算公式算法实现规格说明验证，同时，通过CTL公式与命题μ演算公式的转换，将用CTL表示的需验证的公式转化为由μ演算公式，以验证系统的规格说明，算法复杂性为O（（｜f｜·n）^d），其中d是公式f中不动点算子μ和ν的交替长度，n为状态数。