| 时序系统命题μ演算算法设计与实现 |
| |
| 引用本文： | 王平,沈云付,陈牧之.时序系统命题μ演算算法设计与实现[J].上海大学学报(自然科学版),2006,12(5):534-538. |
| |
| 作者姓名： | 王平 沈云付 陈牧之 |
| |
| 作者单位： | 上海大学,计算机工程与科学学院,上海,200072 |
| |
| 摘 要： | 以μ演算方法研究命题时序逻辑模型,设计实现了命题μ演算中μ演算公式输入以及对输入公式的检查、编译、分析和计算,并通过模型输入及μ演算公式算法实现规格说明验证.同时,通过CTL公式与命题μ演算公式的转换,将用CTL表示的需验证的公式转化为由μ演算公式,以验证系统的规格说明,算法复杂性为O((|f|.n)d),其中d是公式f中不动点算子μ和ν的交替长度,n为状态数.
|
| 关 键 词： | 模型检测 命题μ演算 Kripke结构 有穷系统 状态爆炸 |
| 文章编号： | 1007-2861(2006)05-0534-05 |
| 修稿时间： | 2005年9月19日 |
Propositional μ-Calculus Design and Implementation for Temporal Logic Systems |
| |
| WANG Ping,SHEN Yun-fu,CHEN Mu-zhi.Propositional μ-Calculus Design and Implementation for Temporal Logic Systems[J].Journal of Shanghai University(Natural Science),2006,12(5):534-538. |
| |
| Authors: | WANG Ping SHEN Yun-fu CHEN Mu-zhi |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
