Skip to main content
SpringerLink
Log in

Model Checking with Multi-valued Logics

  • Conference paper
Automata, Languages and Programming (ICALP 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3142))

Included in the following conference series:

Abstract

In multi-valued model checking, a temporal logic formula is interpreted relative to a structure not as a truth value but as a lattice element. In this paper we present new algorithms for multi-valued model checking. We first show how to reduce multi-valued model checking with any distributive DeMorgan lattice to standard, two-valued model checking. We then present a direct, automata-theoretic algorithm for multi-valued model checking with logics as expressive as the modal mu-calculus. As part of showing correctness of the algorithm, we present a new fundamental result about extended alternating automata, a generalization of standard alternating automata.

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

Access this chapter

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 189.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 239.00
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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bolc, L., Borowik, P.: Many-Valued Logics. Springer, Heidelberg (1992)

    MATH  Google Scholar 

  2. Bruns, G., Godefroid, P.: Generalized Model Checking: Reasoning about Partial State Spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 168. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  3. Bruns, G., Godefroid, P.: Temporal Logic Query Checking. In: Proc. of LICS 2001, pp. 409–417. IEEE, Los Alamitos (2001)

    Google Scholar 

  4. Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Bruns, G., Godefroid, P.: Model checking with multi-valued logics. Technical Report BL03.00018, Bell Labs, Lucent Technologies (May 2003)

    Google Scholar 

  6. Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  7. Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model checking. Tech. Report 448, Comp. Sys. Res. Group, Univ. of Toronto (2001)

    Google Scholar 

  8. Chechik, M., Easterbrook, W.: A framework for multi-valued reasoning over inconsistent viewpoints. In: Proc. of ICSE 2001 (2001)

    Google Scholar 

  9. Chechik, M., Easterbrook, W., Gurfinkel, A.: Model exploration with temporal logic query checking. In: Proc. of FSE 2002, ACM, New York (2002)

    Google Scholar 

  10. Chechik, M., Devereux, B., Gurfinkel, A.: Model-checking infinite state-space systems with fine-grained abstractions using SPIN. In: Proc. of SPIN Workshop on Model-Checking Software (2001)

    Google Scholar 

  11. Davey, B.A., Priestly, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)

    MATH  Google Scholar 

  12. Emerson, E.A.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, pp. 995–1072. Elsevier, Amsterdam (1990)

    Google Scholar 

  13. Fitting, M.: Many-valued modal logics I. Fund. Informaticae 15, 235–254 (1992)

    MathSciNet  Google Scholar 

  14. Fitting, M.: Many-valued modal logics II. Fund. Informaticae 17, 55–73 (1992)

    MATH  MathSciNet  Google Scholar 

  15. Fecht, C., Seidl, H.: A Faster Solver for General Systems of Equations. Sci. Comp. Programming 35(2), 137–161 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  16. Godefroid, P., Jagadeesan, R.: On the Expressiveness of 3-Valued Models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 206–222. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Gurfinkel, A., Chechik, M.: Multi-valued model checking via classical model checking. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 266–280. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Huth, M., Pradhan, S.: Lifting assertion and consistency checkers from single to multiple viewpoints. Technical report 2002/11, Dept. of Computing, Imperial College, London (2002)

    Google Scholar 

  19. Konikowska, B., Penczek, W.: Reducing model checking from multi-valued CTL* to CTL*. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, p. 226. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Kozen, D.: Results on the Propositional Mu-Calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  21. Kupferman, O., Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Branching-Time Model Checking. JACM 47(2), 312–360 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  22. Stirling, C.: Modal and temporal logics for processes. Notes for Summer School in Logic Methods in Concurrency, C.S. Dept., Åarhus University, Denmark (1993)

    Google Scholar 

  23. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. of Maths 5, 285–309 (1955)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Bell Laboratories, Lucent Technologies,  

    Glenn Bruns & Patrice Godefroid

Authors
  1. Glenn Bruns
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Patrice Godefroid
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departament de Llenguatges i Sistemes Informatics, Universitat Politecnica de Catalunya, Campus Nord - Ed. Omega, 240 Jordi Girona Salgado, 1-3 E-08034, Barcelona

    Josep Díaz

  2. Department of Mathematics and Turku Centre for Computer Science TUCS, University of Turku, 20014, Turku, Finland

    Juhani Karhumäki

  3. Department of Mathematics, University of Turku, Turku, Finland

    Arto Lepistö

  4. Laboratory for Foundations of Computer Science, University of Edinburgh,  

    Donald Sannella

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bruns, G., Godefroid, P. (2004). Model Checking with Multi-valued Logics. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds) Automata, Languages and Programming. ICALP 2004. Lecture Notes in Computer Science, vol 3142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27836-8_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27836-8_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22849-3

  • Online ISBN: 978-3-540-27836-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation