Temporal abstract interpretation

ABSTRACT

We study the abstract interpretation of temporal calculi and logics in a general syntax, semantics and abstraction independent setting. This is applied to the @@@@-calculus, a generalization of the &mgr;-calculus with new reversal and abstraction modalities as well as a new time-symmetric trace-based semantics. The more classical set-based semantics is shown to be an abstract interpretation of the trace-based semantics which leads to the understanding of model-checking and its application to data-flow analysis as incomplete temporal abstract interpretations. Soundness and incompleteness of the abstractions are discussed. The sources of incompleteness, even for finite systems, are pointed out, which leads to the identification of relatively complete sublogics, à la CTL.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: BEN-ARI, M., MANNA, Z., AND PNUELI, A. The temporal logic of branching time. Acta Informat. 20 (1983), 207-226.
• 3: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 4: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 5: Rance Cleaveland , S. Purushothaman Iyer , Daniel Yankelevich, Optimality in Abstractions of Model Checking, Proceedings of the Second International Symposium on Static Analysis, p.51-63, September 25-27, 1995
• 6: COUSOT, P. Semantic foundations of program analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick & N. Jones, Eds. Prentice-Hall, 198 l, 303-342.
• 7: Patrick Cousot, Types as abstract interpretations, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.316-331, January 15-17, 1997, Paris, France [doi>10.1145/263699.263744]
• 8: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 9: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 10: Patrick Cousot , Radhia Cousot, Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.269-295, August 26-28, 1992
• 11: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 12: Dennis Dams , Rob Gerth , Orna Grumberg, Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.253-291, March 1997 [doi>10.1145/244795.244800]
• 13: David L. Dill , Howard Wong-Toi, Verification of Real-Time Systems by Successive Over and Under Approximation, Proceedings of the 7th International Conference on Computer Aided Verification, p.409-422, July 03-05, 1995
• 14: E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
• 15: Roberto Giacobazzi , Francesco Ranzato , Francesca Scozzari, Complete Abstract Interpretations Made Constructive, Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science, p.366-377, August 24-28, 1998
• 16: Susanne Graf , Claire Loiseaux, A Tool for Symbolic Program Verification and Abstration, Proceedings of the 5th International Conference on Computer Aided Verification, p.71-84, June 28-July 01, 1993
• 17: Nicolas Halbwachs , Yann-Erick Proy , Patrick Roumanoff, Verification of Real-Time Systems using Linear Relation Analysis, Formal Methods in System Design, v.11 n.2, p.157-185, Aug. 1997 [doi>10.1023/A:1008678014487 ]
• 18: KOZEN, D. Results on the propositional #-calculus. Theoret. Comput. Sci. 27 (1983), 333-354.
• 19: A. Browne , E. M. Clarke , S. Jha , D. E. Long , W. Marrero, An improved algorithm for the evaluation of fixpoint expressions, Theoretical Computer Science, v.178 n.1-2, p.237-255, May 30, 1997 [doi>10.1016/S0304-3975(96)00228-9 ]
• 20: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 21: Laurent Mauborgne, Binary Decision Graphs, Proceedings of the 6th International Symposium on Static Analysis, p.101-116, September 22-24, 1999
• 22: David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268950]
• 23: Bernhard Steffen, Generating data flow analysis algorithms from modal specifications, Science of Computer Programming, v.21 n.2, p.115-139, Oct. 1993

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Design, Theory