微信服务号

微信订阅号

2025年5月17日 1:29 星期六
首页 > 过刊浏览>2003年第14卷第10期 >1672-1680
PDF HTML阅读 XML下载 导出引用 引用提醒
谓词μ演算和模态图的语义一致性
作者:
基金项目:

Supported by the National Natural Science Foundation of China under Grant No.69833020 (国家自然科学基金)


Consistency Between the Predicate μ-Calculus and Modal Graphs
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [9]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    模态图是谓词μ演算的一种有效的图形表示形式.证明了谓词μ演算和模态图的语义一致性,详细讨论了谓词μ演算公式、嵌套谓词等式系和模态图之间的关系,并给出了一种优化的从线性公式到嵌套谓词等式系的转换算法.

    Abstract:

    The modal graphs are effective graph forms for the predicate μ-calculus. The consistency between the predicate μ-calculus and the modal graphs is strictly established. Moreover, the relationship among the predicate μ-calculus, nested predicate equations and the modal graphs is discussed in detail. An optimized transformation algorithm from predicate μ-calculus formulae to nested predicate equations is presented.

    参考文献
    [1]Lin HM. Model checking value-passing processes. In: Proceedings of the 8th Asia-Pacific Software Engineering Conference. Macao: IEEE Press, 2001. 3～10.
    [2]Lin HM. Symbolic transition graphs with assignment. In: Montanari U, Sassone V, eds. Proceedings of the CONCUR'96. LNCS 1119, Heidelberg: Springer-Verlag, 1996. 50～65.
    [3]Mader, A. Verification of modal properties using Boolean equation systems [Ph.D. Thesis]. TMU, 1997.
    [4]Cleaveland R, Klein M, Steffen B. Faster model checking for the modal Mu-calculus. In: Bochmann GV, Probst DK, eds. Proceedings of the CAV'92. LNCS 663, Heidelberg: Springer-Verlag, 1992. 410～422.
    [5]Andersen HR. Model checking and Boolean graphs. Theoretical Computer Science, 1994,126(1):3～30.
    [6]Andersen HR. Verification of temporal properties of concurrent systems [Ph.D. Thesis]. Aarhus: Aarhus University, 1993.
    [7]Liu X, Ramakrishnan CR, Smolka SA. Fully local and efficient evaluation of alternating fixed points. In: Steffen B, ed. Proceedings of the TACAS'98. LNCS 1384, Heidelberg: Springer-Verlag, 1998. 5～19.
    [8]Bhat GS, Cleaveland R. Efficient model checking via the equational (-calculus. In: Clarke EM, ed. Proceedings of the 11th Annual Symposium on Logic in Computer Science. New Jersey: IEEE Computer Society Press, 1996. 304～312.
    [9]Vergauwen B, Lewi J. Efficient local correctness checking for single and alternating Boolean equation systems. In: Abiteboul S, Shamir E, ed. Proceeding of the ICALP'94. LNCS 820, Heidelberg: Springer-Verlag, 1994. 304～315.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

刘剑,林惠民.谓词μ演算和模态图的语义一致性.软件学报,2003,14(10):1672-1680

复制
分享
文章指标
  • 点击次数:3913
  • 下载次数: 6114
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2003-01-03
  • 最后修改日期:2003-01-03
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19945541位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号