Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Verification, Model Checking, and Abstract Interpretation

VMCAI 2003: Verification, Model Checking, and Abstract Interpretation pp 206–222Cite as

On the Expressiveness of 3-Valued Models

  • Conference paper
  • First Online:

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

Abstract

Three-valued models and logics have been recently advocated as being more suitable to reason about automatically-generated abstractions of reactive systems than traditional “2-valued” models such as standard Kripke structures or Labeled Transition Systems. Indeed, abstractions specified in 3-valued models are able to distinguish properties that are true, false and unknown of the concrete system, and hence their analysis can yield correctness proofs and counter-examples that can be both guaranteed to be sound. In this paper, we study several 3-valued modeling formalisms proposed in the literature and show that they have the same expressiveness, in the sense that any model specified in any of these formalisms can be translated into a model specified in any other. We also show that the complexity of the model checking and generalized model checking problems does not change from one formalism to the other.

Supported in part by NSF grants CCR 99010171 and CCR 02030716.

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. G. Bruns and P. Godefroid. Model Checking Partial State Spaces with 3-Valued Temporal Logics. In Proceedings of the 11th Conference on Computer Aided Verification, volume 1633 of Lecture Notes in Computer Science, pages 274–287, Trento, July1999. Springer-Verlag.

    Google Scholar 

  2. G. Bruns and P. Godefroid. Generalized Model Checking: Reasoning about Partial State Spaces. In Proceedings of CONCUR’2000 (11th International Conference on Concurrency Theory), volume 1877 of Lecture Notes in Computer Science, pages 168–182, University Park, August 2000. Springer-Verlag.

    Google Scholar 

  3. T. Ball, A. Podelski, and S. K. Rajamani. Boolean and Cartesian Abstraction for Model Checking C Programs. In Proceedings of TACAS’2001 (Tools and Algorithms for the Construction and Analysis of Systems), volume 2031 of Lecture Notes in Computer Science. Springer-Verlag, April 2001.

    Google Scholar 

  4. T. Ball and S. Rajamani. The SLAM Toolkit. In Proceedings of CAV’2001 (13th Conference on Computer Aided Verification), volume 2102 of Lecture Notes in Computer Science, pages 260–264, Paris, July 2001. Springer-Verlag.

    Google Scholar 

  5. D.R. Chase, M. Wegman, and F.K. Zadeck. Analysis of pointers and structures. In Proccedings of Conference on Programming Language Design and Implementation, pages 296–310, June 1990.

    Google Scholar 

  6. D. Dams. Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands, 1996.

    Google Scholar 

  7. S. Das, D. L. Dill, and S. Park. Experience with Predicate Astraction. In Proc. of the 11th International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, pages 160–172, Trento, July 1999. Springer Verlag.

    Google Scholar 

  8. P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based Model Checking using Modal Transition Systems. In Proceedings of CONCUR’ 2001 (12th International Conference on Concurrency Theory), volume 2154 of Lecture Notes in Computer Science, pages 426–440, Aalborg, August 2001. Springer-Verlag.

    Google Scholar 

  9. P. Godefroid and R. Jagadeesan. Automatic Abstraction Using Generalized Model Checking. In Proceedings of CAV’2002 (14th Conference on Computer Aided Verification), volume 2404 of Lecture Notes in Computer Science, pages 137–150, Copenhagen, July 2002. Springer-Verlag.

    Google Scholar 

  10. S. Graf and H. Saidi. Construction of Abstract State Graphs with PVS. In Proceedings of the 9th International Conference on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 72–83, Haifa, June 1997. Springer-Verlag.

    Google Scholar 

  11. T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages, pages 58–70, Portland, January 2002.

    Google Scholar 

  12. M. Huth, R. Jagadeesan, and D. Schmidt. Modal Transition Systems: a Foundation for Three-Valued Program Analysis. In Proceedings of the European Symposium on Programming (ESOP’2001), volume 2028 of Lecture Notes in Computer Science. Springer-Verlag, April 2001.

    Google Scholar 

  13. M. Huth, R. Jagadeesan, and D. Schmidt. A Domain Equation for Refinement of Partial Systems. Submitted to Mathematical Structures in Computer Science, 2002.

    Google Scholar 

  14. J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.

    Google Scholar 

  15. M. Huth. Model Checking Modal Transition Systems using Kripke Structures. In Proceedings of the Third International Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI’2002), volume 2294 of Lecture Notes in Computer Science, pages 302–316, Venice, January 2002. Springer-Verlag.

    Google Scholar 

  16. M. Huth. Possibilistic and Probabilistic Abstraction-based Model Checking. In Proceedings of the PAPM-Probmiv 2002 Workshop, volume 2329 of Lecture Notes in Computer Science, pages 115–134, Copenhagen, July 2002. Springer-Verlag.

    Google Scholar 

  17. S. C. Kleene. Introduction to Metamathematics. North Holland, 1987.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  19. K. G. Larsen. Modal Specifications. In J. Sifakis, editor, Workshop on Automatic Verification Methods for Finite-State Systems, volume 407 of Lecture Notes in Computer Science, pages 232–246. Springer-Verlag, June 1989. International Workshop, Grenoble, France.

    Google Scholar 

  20. K. G. Larsen and B. Thomsen. A Modal Process Logic. In Proceedings of Third Annual Symposium on Logic in Computer Science, pages 203–210. IEEE Computer Society Press, 1988.

    Google Scholar 

  21. R. Milner. A Modal Characterization of Observable Machine Behavior. In Proc. CAAP’81, volume 112 of Lecture Notes in Computer Science, pages 25–34. Springer-Verlag, 1981.

    Google Scholar 

  22. M. Muller-Olm, D. Schmidt, and B. Steffen. Model Checking: A Tutorial Introduction. In Proceedings of the 6th International Static Analysis Symposium (SAS’99), volume 1694 of Lecture Notes in Computer Science, pages 331–354, Berlin, September 1999. Springer-Verlag.

    Google Scholar 

  23. M. Sagiv, T. Reps, and R. Wilhelm. Parametric Shape Analysis Via 3-Valued Logic. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages, January 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DePaul University, USA

    Patrice Godefroid

  2. Bell Laboratories, Lucent Technologies, USA

    Radha Jagadeesan

Authors
  1. Patrice Godefroid
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Radha Jagadeesan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, New York University, 715 Broadway (7th floor), NY 10003, NewYork, USA

    Lenore D. Zuck

  2. College of Computer Science, Northeastern University, 360 Huntington Ave., 02115, Boston, MA, USA

    Paul C. Attie

  3. Computer Science Department, Venice University C’Foscari, Via Torino 155, 30170, Mestre-Venezia, Italy

    Agostino Cortesi

  4. Department of Computer Science and Electrical Engineering, West Virginia University, 26505, Morgantown, WV, USA

    Supratik Mukhopadhyay

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Godefroid, P., Jagadeesan, R. (2003). On the Expressiveness of 3-Valued Models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2003. Lecture Notes in Computer Science, vol 2575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36384-X_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-36384-X_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00348-9

  • Online ISBN: 978-3-540-36384-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation