直觉线性μ-演算

线性mu-演算(μtl)是线性时序逻辑(ltl)的不动点扩展.ltl是一个便于规范和论证反应式系统的方法.μtl作为比ltl表达能力更强的逻辑,用ltl表示的性质度可由μtl表示.类似于ltl的直觉线性时序逻辑(ltl),提出一种基于直觉解释的μtl,称为直觉μtl(iμtl).确立了iμtl和iltl的关系,比较了它们之间的表达能力.讨论了使用iμtl与安全性质和活性描述的关系以及描述“假设-保证”规范的问题.