Modal Transition Systems: A Foundation for Three-Valued Program Analysis

  • Michael Huth
  • Radha Jagadeesan
  • David Schmidt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


We present Kripke modal transition systems (Kripke MTSs), a generalization of modal transition systems [27,26], as a foundation for three-valued program analysis. The semantics of Kripke MTSs are presented by means of a mixed power domain of states; soundness and consistency are proved. Two major applications, model checking partial state spaces and three-valued program shape analysis, are presented as evidence of the suitability of Kripke MTSs as a foundation for three-valued analyses.


Model Check Modal Logic Slot Machine Label Transition System Kripke Structure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    T. Ball, A. Podelski, and S. K. Rajamani. Boolean and Cartesian Abstraction for Model Checking C Programs. Personal communication, December 2000.Google Scholar
  2. 2.
    J. C. Bradfield. Verifying Temporal Properties Of Systems. Birkhäuser, Boston, Mass., 1991.Google Scholar
  3. 3.
    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. Springer Verlag, July 1999.CrossRefGoogle Scholar
  4. 4.
    G. Bruns and P. Godefroid. Gernalized 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. Springer Verlag, August 2000.Google Scholar
  5. 5.
    J. R. Burch, E. M. Clarke, D. L. Dill K. L. McMillan, and J. Hwang. Symbolic model checking: 1020 states and beyond. Proceedings of the Fifth Annual Symposium on Logic in Computer Science, June 1990.Google Scholar
  6. 6.
    D. Chase, M. Wegman, and F. Zadeck. Analysis of pointers and structures. In SIGPLAN Conf. on Prog. Lang. Design and Implementation, pages 296–310. ACM Press, 1990.Google Scholar
  7. 7.
    E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, 1994.CrossRefGoogle Scholar
  8. 8.
    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs. In Proc. 4th ACM Symp. on Principles of Programming Languages, pages 238–252. ACM Press, 1977.Google Scholar
  9. 9.
    P. Cousot and R. Cousot. Temporal abstract interpretation. In Conference Record of the Twenty seventh Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 12–25, Boston, Mass., January 2000. ACMPress, New York, NY.Google Scholar
  10. 10.
    M. Dam. CTL✻ and ECTL✻ as Fragments of the Modal mu-Calculus. Theoretical Computer Science, 126:77–96, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    D. Dams. Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands, 1996.zbMATHGoogle Scholar
  12. 12.
    R. de Nicola and F. Vaandrager. Three Logics for Branching Bisimulation. Journal of the Association of Computing Machinery, 42(2):458–487, March 1995.zbMATHGoogle Scholar
  13. 13.
    M. Fitting. Many-valued modal logics. Fundamenta Informaticae, 17:55–73, 1992.MathSciNetzbMATHGoogle Scholar
  14. 14.
    R. Ghiya and L. J. Hendren. Is it a Tree, a DAG, or a Cyclic Graph? A Shape Analysis for Heap-Directed Pointers in C. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1–15, 1996.Google Scholar
  15. 15.
    C. Gunter. The mixed power domain. Theoretical Computer Science, 103:311–334, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    M. Hecht. Flow Analysis of Computer Programs. Elsevier, 1977.Google Scholar
  17. 17.
    R. Heckmann. Power domains and second order predicates. Theoretical Computer Science, 111:59–88, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    M. C. B. Hennessy and Robin Milner. Algebraic laws for non-determinism and concurrency. JACM, 32:137–161, 1985.Google Scholar
  19. 19.
    M. Huth. A Unifying Framework for Model Checking Labeled Kripke Structures, Modal Transition Systems, and Interval Transition Systems. In Proceedings of the 19th International Conference on the Foundations of Software Technology & Theoretical Computer Science, Lecture Notes in Computer Science, pages 369–380, IIT Chennai, India, December 1999. Springer Verlag.CrossRefGoogle Scholar
  20. 20.
    M. Huth, R. Jagadeesan, and D. Schmidt. Modal transition systems: new foundations and new applications. To appear as a KSU-CIS Techreport, August 2000.Google Scholar
  21. 21.
    D. Jackson, I. Schechter, and I. Shlyakhter. Alcoa: the alloy constraint analyzer. In Proc. International Conference on Software Engineering, Limerick, Ireland, 2000.Google Scholar
  22. 22.
    N.D. Jones and S. Muchnick. Flow analysis and optimization of LISP-like structures. In Proc. 6th. ACM Symp. Principles of Programming Languages, pages 244–256, 1979.Google Scholar
  23. 23.
    J. Kam and J. Ullman. Global data flow analysis and iterative algorithms. J. ACM, 23:158–171, 1976.zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    P. Kelb. Model checking and abstraction: a framework preserving both truth and failure information. Technical Report Technical report, OFFIS, University of Oldenburg, Germany, 1994.Google Scholar
  25. 25.
    D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    K. G. Larsen. Modal Specifications. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 232–246. Springer Verlag, June 12-14 1989. International Workshop, Grenoble, France.Google Scholar
  27. 27.
    K. G. Larsen and B. Thomsen. A Modal Process Logic. In Third Annual Symposium on Logic in Computer Science, pages 203–210. IEEE Computer Society Press, 1988.Google Scholar
  28. 28.
    F. Levi. A symbolic semantics for abstract model checking. In Static Analysis Symposium: SAS’98, volume 1503 of Lecture Notes in Computer Science. Springer Verlag, 1998.Google Scholar
  29. 29.
    R. Milner. A modal characterisation of observable machine behaviours. In G. Astesiano and C. Böhm, editors, CAAP `81, volume 112 of Lecture Notes in Computer Science, pages 25–34. Springer Verlag, 1981.Google Scholar
  30. 30.
    O. Morikawa. Some modal logics based on a three-valued logic. Notre Dame J. of Formal Logic, 30:130–137, 1989.zbMATHCrossRefMathSciNetGoogle Scholar
  31. 31.
    S. Muchnick and N.D. Jones, editors. Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.Google Scholar
  32. 32.
    F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer Verlag, 1999.Google Scholar
  33. 33.
    A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In J.W. de Bakker, editor, Current Trends in Concurrency, volume 224 of Lecture Notes in Computer Science, pages 510–584. Springer-Verlag, 1985.Google Scholar
  34. 34.
    T. Reps. Program analysis via graph reachability. In J. Maluszynski, editor, Proc. Int’l. Logic Prog. Symp.’97, pages 5–19. MIT Press, 1997.Google Scholar
  35. 35.
    M. Sagiv, T. Reps, and R. Wilhelm. Parametric Shape Analysis via 3-Valued Logic. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, pages 105–118, January 20-22, San Antonio, Texas 1999.Google Scholar
  36. 36.
    D. A. Schmidt. Binary relations for abstraction and refinement. Elsevier Electronic Notes in Computer Science, November 1999. Workshop on Refinement and Abstraction, Osaka, Japan. To appear.Google Scholar
  37. 37.
    K. Segerberg. Some modal logics based on a three-valued logic. Theoria, 33:53–71, 1967.zbMATHMathSciNetCrossRefGoogle Scholar
  38. 38.
    C. Stirling. Modal logics for communicating systems. Theoretical Computer Science, 39:331–347, 1987.Google Scholar
  39. 39.
    D. J. Walker. Bisimulation and divergence. Information and Computation, 85(2):202–241, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  40. 40.
    J. Whaley and M. Rinard. Compositional pointer and escape analysis for Java programs. In Proc. OOPSLA’99, pages 187–206. ACM, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Michael Huth
    • 1
  • Radha Jagadeesan
    • 2
  • David Schmidt
    • 1
  1. 1.Computing and Information SciencesKansas State UniversityUSA
  2. 2.Department of Mathematics and Computer ScienceLoyola University of ChicagoUSA

Personalised recommendations