An optimizing compiler for batches of temporal logic formulas

ABSTRACT

Model checking based on validating temporal logic formulas has proven practical and effective for numerous software engineering applications. As systems based on this approach have become more mainstream, a need has arisen to deal effectively with large batches of formulas over a common model. Presently, most systems validate formulas one at a time, with little or no interaction between validation of separate formulas. This is the case despite the fact that, for a wide range of applications, a certain level of redundancy between domain-related formulas can be anticipated.This paper presents an optimizing compiler for batches of temporal logic formulas. A component of the Carnauba model checking system, this compiler addresses the need to handle batches of temporal logic formulas by leveraging the framework common to optimizing programming language compilers. Just as traditional optimizing compilers attempt to exploit redundancy and other solvable properties in a program to reduce the demand on a runtime system, this compiler exploits similar properties in groups of formulas to reduce the demand on a model checking engine. Optimizations are performed via a set of distinct, interchangeable optimization passes operating on a common intermediate representation. The intermediate representation captures the full modal mu-calculus, and the optimization techniques are applicable to any temporal logic subsumed by that logic. The compiler offers a unified framework for expressing some well understood single-formula optimizations as well as numerous inter-formula optimizations that capitalize on redundancy, logical implication, and, optionally, model-specific knowledge. It is capable of working either in place of, or as a preprocessor for, other optimization algorithms. The result is a system that, when applied to a potentially heterogeneous collection of formulas over a common problem domain, is able to measurably reduce the time and space requirements of the subsequent model checking engine.

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: Michael Benedikt , Patrice Godefroid , Thomas W. Reps, Model Checking of Unrestricted Hierarchical State Machines, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.652-666, July 08-12, 2001
• 3: G. Bhat , R. Cleaveland, Efficient model checking via the equational /spl mu/-calculus, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.304, July 27-30, 1996
• 4: Olaf Burkart , Bernhard Steffen, Model Checking for Context-Free Processes, Proceedings of the Third International Conference on Concurrency Theory, p.123-137, August 24-27, 1992
• 5: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 6: Rance Cleaveland , Marion Klein , Bernhard Steffen, Faster Model Checking for the Modal Mu-Calculus, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.410-422, June 29-July 01, 1992
• 7: Rance Cleaveland , Bernhard Steffen, Computing behavioural relations, logically, Proceedings of the 18th international colloquium on Automata, languages and programming, p.127-138, June 1991, Madrid, Spain
• 8: http://www.grammatech.com/products/codesurfer/.
• 9: Mads Dam, CTL and ECTL as fragments of the modal &mgr;-calculus, Theoretical Computer Science, v.126 n.1, p.77-96, April 11, 1994 [doi>10.1016/0304-3975(94)90269-0]
• 10: 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]
• 11: E. Allen Emerson , Charanjit S. Jutla, The Complexity of Tree Automata and Logics of Programs, SIAM Journal on Computing, v.29 n.1, p.132-158, Feb. 2000 [doi>10.1137/S0097539793304741]
• 12: E. Allen Emerson , Chin-Laung Lei, Modalities for model checking (extended abstract): branching time strikes back, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318620]
• 13: E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings, Symposium on Logic in Computer Science, pages 267--278, Cambridge, Massachusetts, June 1986. IEEE Computer Society.
• 14: J. Ezick, D. W. Richardson, and T. Teitelbaum. Practical model checking and example generation for context-free processes. Technical Report TR2002-1851, Cornell University, August 2001.
• 15: Carsten Fritz , Thomas Wilke, State Space Reductions for Alternating Büchi Automata, Proceedings of the 22nd Conference Kanpur on Foundations of Software Technology and Theoretical Computer Science, p.157-168, December 12-14, 2002
• 16: Paul Gastin , Denis Oddoux, Fast LTL to Büchi Automata Translation, Proceedings of the 13th International Conference on Computer Aided Verification, p.53-65, July 18-22, 2001
• 17: Rob Gerth , Doron Peled , Moshe Y. Vardi , Pierre Wolper, Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, p.3-18, June 01, 1995
• 18: K. Kennedy. A survey of data flow analysis techniques. In S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 1, pages 5--54. Prentice-Hall, 1981.
• 19: D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science (TCS), 27:333--354, 1983.
• 20: W. M. McKeeman, Peephole optimization, Communications of the ACM, v.8 n.7, p.443-444, July 1965 [doi>10.1145/364995.365000]
• 21: Marc Shapiro , Susan Horwitz, Fast and accurate flow-insensitive points-to analysis, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 15-17, 1997, Paris, France [doi>10.1145/263699.263703]
• 22: N. Shilov and K. Yi. A new proof of exponential decidability for propositional mu-calculus with program converse. In III International Conference on Theoretical Aspects of Computer Science, Novi Sad, Yugoslavia, September 2000.
• 23: Fabio Somenzi , Roderick Bloem, Efficient Büchi Automata from LTL Formulae, Proceedings of the 12th International Conference on Computer Aided Verification, p.248-263, July 15-19, 2000
• 24: Robert S. Streett, Propositional Dynamic Logic of looping and converse, Proceedings of the thirteenth annual ACM symposium on Theory of computing, p.375-383, May 11-13, 1981, Milwaukee, Wisconsin, United States [doi>10.1145/800076.802492]
• 25: Moshe Y. Vardi, Reasoning about The Past with Two-Way Automata, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.628-641, July 13-17, 1998
• 26: Mark N. Wegman , F. Kenneth Zadeck, Constant propagation with conditional branches, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.181-210, April 1991 [doi>10.1145/103135.103136]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Modal logic

General Terms:
Verification

Keywords:
model checking, optimizing compiler, temporal logic