时序系统命题μ演算算法设计与实现

摘要：

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

关键词：模型检测、命题μ演算、Kripke结构、有穷系统、状态爆炸

所属期刊栏目：12

分类号：TP301(计算技术、计算机技术)

资助基金：上海市教委资助项目

在线出版日期：2006-11-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：534-538