Subcubic algorithms for recursive state machines

ABSTRACT

We show that the reachability problem for recursive state machines (or equivalently, pushdown systems), believed for long to have cubic worst-case complexity, can be solved in slightly subcubic time. All that is necessary for the new bound is a simple adaptation of a known technique. We also show that a better algorithm exists if the input machine does not have infinite recursive loops.

REFERENCES

• 1: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 2: Rajeev Alur , Mihalis Yannakakis, Model checking of hierarchical state machines, Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering, p.175-188, November 01-05, 1998, Lake Buena Vista, Florida, United States
• 3: Rajeev Alur , Michael Benedikt , Kousha Etessami , Patrice Godefroid , Thomas Reps , Mihalis Yannakakis, Analysis of recursive state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.4, p.786-818, July 2005 [doi>10.1145/1075382.1075387]
• 4: V. L. Arlazarov, E. A. Dinic, M. A. Kronrod, and I. A. Faradzev. On economical construction of the transitive closure of an oriented graph. Soviet Mathematics Doklady, 11:1209--1210, 1970. ISSN 0197-6788.
• 5: Thomas Ball , Sriram K. Rajamani, The SLAM Toolkit, Proceedings of the 13th International Conference on Computer Aided Verification, p.260-264, July 18-22, 2001
• 6: Ahmed Bouajjani , Javier Esparza , Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, Proceedings of the 8th International Conference on Concurrency Theory, p.135-150, July 01-04, 1997
• 7: T. M. Chan. All--pairs shortest paths with real weights in o(n³ log n)) time. In 9th Workshop on Algorithms and Data Structures, pages 318--324, 2005.
• 8: Timothy M. Chan, More algorithms for all-pairs shortest paths in weighted graphs, Proceedings of the thirty-ninth annual ACM symposium on Theory of computing, June 11-13, 2007, San Diego, California, USA [doi>10.1145/1250790.1250877]
• 9: J. Eve and R. Kurki-Suonio. On computing the transitive closure of a relation. Acta Informatica, 8:303--314, 1977.
• 10: John E. Hopcroft , Rajeev Motwani , Jeffrey D. Ullman, Introduction to Automata Theory, Languages, and Computation (3rd Edition), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2006
• 11: S. Horwitz , T. Reps , D. Binkley, Interprocedural slicing using dependence graphs, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.35-46, June 20-24, 1988, Atlanta, Georgia, United States
• 12: Susan Horwitz , Thomas Reps , Mooly Sagiv, Demand interprocedural dataflow analysis, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.104-115, October 12-15, 1995, Washington, D.C., United States
• 13: David Melski , Thomas Reps, Interconvertibility of a class of set constraints and context-free-language reachability, Theoretical Computer Science, v.248 n.1-2, p.29-98, October 2000 [doi>10.1016/S0304-3975(00)00049-9]
• 14: P. W. Purdom. A transitive closure algorithm. BIT, 10:76--94, 1970.
• 15: Jakob Rehof , Manuel Fähndrich, Type-base flow analysis: from polymorphic subtyping to CFL-reachability, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 2001, London, United Kingdom
• 16: Thomas Reps, Shape analysis as a generalized path problem, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.1-11, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215466]
• 17: T. Reps. Program analysis via graph reachability. Information and Software Technology, 40(11-12): 701--726, 1998.
• 18: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 19: T. W. Reps, S. Schwoon, and S. Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. In 10th Static Analysis Symposium, pages 189--213, 2003.
• 20: W. Rytter. Time complexity of loop-free two-way pushdown automata. Information Processing Letters, 16(3): 127--129, 1983.
• 21: Wojciech Rytter, Fast recognition of pushdown automaton and context-free languages, Information and Control, v.67 n.1-3, p.12-22, Oct./Nov./Dec. 1986 [doi>10.1016/S0019-9958(85)80024-3]
• 22: L. Schmitz. An improved transitive closure algorithm. Computing, 30:359--371, 1983.
• 23: M. Sharir and A. Pnueli. Two approaches to interprocedural dataflow analysis. Program Flow Analysis: Theory and Applications, pages 189--234, 1981.
• 24: Manu Sridharan , Denis Gopan , Lexin Shan , Rastislav Bodík, Demand-driven points-to analysis for Java, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 25: L. G. Valiant. General context-free recognition in less than cubic time. Journal of Computer and System Sciences, 10(2):308--315, 1975.
• 26: Mihalis Yannakakis, Graph-theoretic methods in database theory, Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.230-242, April 02-04, 1990, Nashville, Tennessee, United States [doi>10.1145/298514.298576]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms, Theory, Verification

Keywords:
CFL-reachability, context-free languages, cubic bottleneck, interprocedural analysis, pushdown systems, recursive state machines, transitive closure