Advertisement

A Model Checker for Value-Passing Mu-Calculus Using Logic Programming

  • C. R. Ramakrishnan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1990)

Abstract

Recent advances in logic programming have been successfully used to build practical verification toolsets, as evidenced by the XMC system. Thus far, XMC has supported value-passing process languages, but has been limited to using the propositional fragment of modal mucalculus as the property specification logic. In this paper, we explore the use of data variables in the property logic. In particular, we present valuepassing modal mu-calculus, its formal semantics and describe a natural implementation of this semantics as a logic program. Since logic programs naturally deal with variables and substitutions, such an implementation need not pay any additional price- either in terms of performance, or in complexity of implementation- for having the added flexibility of data variables in the property logic. Our preliminary implementation supports this expectation.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [CES86]
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.Google Scholar
  2. [Cha00]
    William Chan. Temporal logic queries. In Computer Aided Verification (CAV), 2000.Google Scholar
  3. [CW96]
    W. Chen and D. S. Warren. Tabled evaluation with delaying for general ogic programs. Journal of the ACM, 43(1):20–74, January 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [FGK+96]
    J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M Sighireanu. CADP (CAESAR/ALDEBERAN development package): protocol validation and verification toolbox. In Computer Aided Verificaon (CAV), volume 1102 of Lecture Notes in Computer Science, pages 437–440, 1996.Google Scholar
  5. [GL88]
    M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In International Conference on Logic Programming, pages 1070–1080, 1988.Google Scholar
  6. [Koz83]
    D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  7. [Mat98]
    R. Mateescu. Local model checking of an alternation-free value-based modal mu-calculus. In Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI), 1998.Google Scholar
  8. [Mil89]
    R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.Google Scholar
  9. [MRRV00]
    M. Mukund, C. R. Ramakrishnan, I. V. Ramakrishnan, and R. Verma. Symbolic bisimulation using tabled constraint logic programming. In International Workshop on Tabulation in Parsing and Deduction (TAPD), 2000.Google Scholar
  10. [RH97]
    J. Rathke and M. Hennessy. Local model checking for value-passing processes. In International Symposium on Theoretical Aspects of Computer Software, 1997.Google Scholar
  11. [RRR+97]
    Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. L. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV’ 97), Haifa, Israel, July 1997. Springer-Verlag.Google Scholar
  12. [RRS+00]
    C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, Y. Dong, X. Du, A. Roychoudhury, and V.N. Venkatakrishnan. XMC: A logicprogramming-based verification toolset. In Computer Aided Verification (CAV), 2000. XMC is available from http://www.cs.sunysb.edu/$¡m$lmc.
  13. [vRS91]
    A. van Gelder, K. A. Ross, and J. S. Schlipf. The well-founded semantics for general logic programs. Journal of the ACM, 38(3), 1991.Google Scholar
  14. [XSB]
    The XSB logic programming system. Available from http://xsb.sourceforge.net.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • C. R. Ramakrishnan
    • 1
  1. 1.Department of Computer ScienceSUNY at Stony BrookStony BrookUSA

Personalised recommendations