位置：成果数据库 > 期刊 > 期刊详情页
直觉线性μ-演算
  • ISSN号：1000-9825
  • 期刊名称：《软件学报》
  • 时间：0
  • 分类：TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
  • 作者机构：[1]中国科学院软件研究所计算机科学重点实验室,北京100190, [2]中国科学院研究生院信息与工程学院,北京100049, [3]Department of Computer Science, Government College University, Lahore, Pakistan
  • 相关基金：Supported by the National Natural Science Foundation of China under Grant Nos.60421001, 60573012 （国家自然科学基金）; the National Basic Research Program of China under Grant No.2002eb312200 （国家重点基础研究发展计划（973）The authors thank anonymous referees for their comments that helped improving this paper.
作者： KAZMI Syed Asad Raza[1,2,3], 张文辉[1]
关键词： 命题线性时序逻辑, 直觉线性μ-演算, propositional linear temporal logic, intuitionistic linear time μ-calculus
中文摘要：

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

英文摘要：

Linear time mu-calculus （μTL） is an extension of linear-time temporal logic （LTL） by fixed points, which is a convenient way to specify and reasoning about reactive systems. As μTL being more expressible than LTL, the properties specified by LTL could be determined by μTL. Similar to the intuitionistic linear-time temporal logic （ILTL）, we propose an intuitionistic variant of μTL as intuitionistic linear time mu-calculus （IμTL）. We have established a correspondence between IμTL and ILTL, and compared their expressive power. Using IμTL to specify safety and liveness properties, and assumption-guarantee specifications are also discussed.

同期刊论文项目
软件形式化方法
期刊论文 36 会议论文 33 著作 2
开放反应系统的模型检测与合成
期刊论文 13 会议论文 15
同项目期刊论文
Handling Synchronization Probl
On an Open Problem of Amadio a
Model-Based Testing of Concurr
约束求解与优化技术的结合
并发Java程序同步操作的有效删除
Property-preserving Compositio
UML活动图的时序逻辑语义
Model Checking Data Consistenc
Compositional Verification for
Eigenvariables, bracketing and
Refining and verifying a class
多线程程序数据竞争的静态检测
一种求解混合约束问题的快速完备
基于约束的主动规则终止性分析
Symbolic Test Generation Using
Computing along the axon
Deriving Non-determinism from
On String Languages Generated
约束问题求解
Symbolic Model Checking of Fin
The inductive approach to stra
Combining search space partiti
基于迁移的扩展Buchi自动机到Buc
A note on the characterization
Structure of Proofs and the Co
Facilitating formal specificat
Linear Tabling Strategies and
有限精度时间自动机的可达性检测
基于共享位置的Petri网系统综合与保性
有限精度时间自动机的时钟表示
从基于迁移的扩展Büchi自动机到Büchi自动机
Intuitionistic Linear-time μ-Calculus
The Complexity of Dual Models Problem of Propositional Linear Temporal Logic
一种基于监控理论的软件设计方法：状态性质变换方法
Combining search space partition and abstraction for LTL model checking
基于迁移的扩展Buchi自动机到Buchi自动机的有效转换
Structure of Proofs and the Complexity of Cut Elimination
A polynomial dynamic system approach to software design for attractivity requirement
命题线性时序逻辑的对偶模型问题的复杂性
从基于迁移的扩展Büchi自动机到Büchi自动机
Improved Bounded Model Checking for the Universal Fragment of CTL
直觉线性μ-演算中的合成推理
期刊信息
  • 《软件学报》
  • 北大核心期刊（2011版）
  • 主管单位:中国科学院
  • 主办单位:中国科学院软件研究所 中国计算机学会
  • 主编：赵琛
  • 地址：北京8718信箱中国科学院软件研究所
  • 邮编：100190
  • 邮箱：jos@iscas.ac.cn
  • 电话：010-62562563
  • 国际标准刊号：ISSN：1000-9825
  • 国内统一刊号：ISSN：11-2560/TP
  • 邮发代号:82-367
  • 获奖情况:
  • 2001年入选中国期刊方阵“双百期刊”,2000年荣获中国科学院优秀科技期刊一等奖
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,美国数学评论（网络版）,波兰哥白尼索引,德国数学文摘,荷兰文摘与引文数据库,美国工程索引,美国剑桥科学文摘,英国科学文摘数据库,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊（2004版）,中国北大核心期刊（2008版）,中国北大核心期刊（2011版）,中国北大核心期刊（2014版）,中国北大核心期刊（2000版）
  • 被引量:54609