摘要
以μ演算方法研究命题时序逻辑模型,设计实现了命题μ演算中μ演算公式输入以及对输入公式的检查、编译、分析和计算,并通过模型输入及μ演算公式算法实现规格说明验证.同时,通过CTL公式与命题μ演算公式的转换,将用CTL表示的需验证的公式转化为由μ演算公式,以验证系统的规格说明,算法复杂性为O((|f|.n)d),其中d是公式f中不动点算子μ和ν的交替长度,n为状态数.
Kripke models of temporal logic systems are initialized and analyzed using propositional μ-calculus. Check, compilation, analysis and calculation of the input formulas are implemented with a fixed-point algorithm. A model checking method is applied to check the specification of the model in the system. At the same time, computational tree logic (CTL) formulas are transformed into propositional μ-calculus formulas. The specifications can easily be checked using model checking based on propositional μ-calculus. The complexity is O(( |f|· n)^d), where d is the alternate length of μ and ν, and n is the number of states.
出处
《上海大学学报(自然科学版)》
CAS
CSCD
北大核心
2006年第5期534-538,共5页
Journal of Shanghai University:Natural Science Edition
基金
上海市教委E研究院-上海高校网格资助项目