微信服务号

微信订阅号

2025-4-4- 4
Home > Archive>Volume 14, Issue 10, 2003 >1672-1680
PDF HTML XML Export Cite reminder
Consistency Between the Predicate μ-Calculus and Modal Graphs
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [9]
    • |
  • Related [20]
    • | | |
  • Comments
    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.

    Reference
    [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.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:3899
  • PDF: 6050
  • HTML: 0
  • Cited by: 0
History
  • Received:January 03,2003
  • Revised:January 03,2003
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2032640Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063