Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Practical Aspects of Declarative Languages

PADL 2001: Practical Aspects of Declarative Languages pp 1–13Cite as

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

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((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.

Research supported in part by NSF grants EIA-9705998 and CCR-9876242.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. William Chan. Temporal logic queries. In Computer Aided Verification (CAV), 2000.

    Google Scholar 

  3. W. Chen and D. S. Warren. Tabled evaluation with delaying for general ogic programs. Journal of the ACM, 43(1):20–74, January 1996.

    Article  MATH  MathSciNet  Google Scholar 

  4. 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. 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. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  7. 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. R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

    Google Scholar 

  9. 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. 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. 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. 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. 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. The XSB logic programming system. Available from http://xsb.sourceforge.net.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, SUNY at Stony Brook, NY 11794-4400, Stony Brook, USA

    C. R. Ramakrishnan

Authors
  1. C. R. Ramakrishnan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, State University of New York, Stony Brook, 11794, NY, USA

    I. V. Ramakrishnan

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ramakrishnan, C.R. (2001). A Model Checker for Value-Passing Mu-Calculus Using Logic Programming. In: Ramakrishnan, I.V. (eds) Practical Aspects of Declarative Languages. PADL 2001. Lecture Notes in Computer Science, vol 1990. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45241-9_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-45241-9_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41768-2

  • Online ISBN: 978-3-540-45241-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation