| 直觉线性μ-演算 |
| |
| 引用本文： | KAZMI Syed Asad Raz,张文辉.直觉线性μ-演算[J].软件学报,2008,19(12):3122-3133. |
| |
| 作者姓名： | KAZMI Syed Asad Raz 张文辉 |
| |
| 作者单位： | 1. 中国科学院,软件研究所,计算机科学重点实验室,北京,100190;中国科学院,研究生院,信息与工程学院,北京,100049;Department of Computer Science, Government College University, Lahore, Pakistan
2. 中国科学院,软件研究所,计算机科学重点实验室,北京,100190 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China under Grant Nos.60421001, 60573012 (国家自然科学基金); the National Basic Research Program of China under Grant No.2002cb312200 (国家重点基础研究发展计划(973)) |
| |
| 摘 要： | 线性mu-演算(μTL)是线性时序逻辑(LTL)的不动点扩展.LTL是一个便于规范和论证反应式系统的方法.μTL作为比LTL表达能力更强的逻辑,用LTL表示的性质度可由μTL表示.类似于LTL的直觉线性时序逻辑(ILTL),提出一种基于直觉解释的μTL,称为直觉μTL(IμTL).确立了IμTL和ILTL的关系,比较了它们之间的表达能力.讨论了使用IμTL与安全性质和活性描述的关系以及描述"假设-保证"规范的问题.
|
| 关 键 词： | 命题线性时序逻辑 直觉线性μ-演算 intuitionistic linear time μ-calculus |
| 收稿时间： | 2007/8/16 0:00:00 |
| 修稿时间： | 2007/12/6 0:00:00 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
