Rajeev Alur
Thomas Reps
Abstract
Recursive state machines (RSMs) enhance the power of ordinary state machines by allowing vertices to correspond either to ordinary states or to potentially recursive invocations of other state machines. RSMs can model the control flow in sequential imperative programs containing recursive procedure calls. They can be viewed as a visual notation extending Statecharts-like hierarchical state machines, where concurrency is disallowed but recursion is allowed. They are also related to various models of pushdown systems studied in the verification and program analysis communities.After introducing RSMs and comparing their expressiveness with other models, we focus on whether verification can be efficiently performed for RSMs. Our first goal is to examine the verification of linear time properties of RSMs. We begin this study by dealing with two key components for algorithmic analysis and model checking, namely, reachability (Is a target state reachable from initial states?) and cycle detection (Is there a reachable cycle containing an accepting state?). We show that both these problems can be solved in time O(nθ2) and space O(nθ), where n is the size of the recursive machine and θ is the maximum, over all component state machines, of the minimum of the number of entries and the number of exits of each component. From this, we easily derive algorithms for linear time temporal logic model checking with the same complexity in the model. We then turn to properties in the branching time logic CTL*, and again demonstrate a bound linear in the size of the state machine, but only for the case of RSMs with a single exit node.
- Alur, R., Etessami, K., and Madhusudan, P. 2004. A temporal logic of nested calls and returns. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), volume 2988 of LNCS, pages 467--481. Springer.]]Google Scholar
- Alur, R., Etessami, K., and Yannakakis, M. 2001. Analysis of recursive state machines. In CAV 2001, pages 207--220.]] Google Scholar
- Alur, R., Torre, S. L., and Madhusudan, P. 2003a. Modular strategies for recursive game graphs. In Proceedings of TACAS, volume 2619 of LNCS, pages 363--378.]] Google Scholar
- Alur, R., Torre, S. L., and Madhusudan, P. 2003b. Modular strategies for infinite games on recursive graphs. In Proceedings of CAV'03, volume 2725 of LNCS, pages 67--79.]]Google Scholar
- Alur, R. and Yannakakis, M. 2001. Model checking of hierarchical state machines. ACM Trans. Prog. Lang. Syst. 23, 3, pages 273--303.]] Google Scholar
- Andersen, H. 1994. Model checking and boolean graphs. Theoret. Comput. Sci.126, 1, 3--30.]] Google Scholar
- Ball, T. and Rajamani, S. 2000. Bebop: A symbolic model checker for boolean programs. In SPIN '2000, volume 1885 of LNCS, pages 113--130.]] Google Scholar
- Benedikt, M., Godefroid, P., and Reps, T. 2001. Model checking of unrestricted hierarchical state machines. In ICALP'2001, pages 652--666.]] Google Scholar
- Booch, G., Jacobson, J., and Rumbaugh, J. 1997. The Unified Modeling Language User Guide. Addison Wesley.]] Google Scholar
- Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR'97, pages 135--150.]] Google Scholar
- Bouajjani, A., Esparza, J., and Touili, T. 2003. A generic approach to the static analysis of concurrent programs with procedures. In POPL '03, pages 62--73.]] Google Scholar
- Balakrishnan, G. and Reps, T. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Compiler Construction (CC'04), volume 2985 of LNCS, pages 5--23. Springer.]]Google Scholar
- Burkart, O. and Steffen, B. 1992. Model checking and context-free processes. In CONCUR '92, pages 122--137.]] Google Scholar
- Burkart, O. and Steffen, B. 1999. Model checking the full modal mu-calculus for infinite sequential processes. Theoret. Comput. Sci. 221, 251--270.]] Google Scholar
- Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., and Palsberg, J. 2003. Stack size analysis for interrupt-driven programs. In Proceedings of the 10th Static Analysis Symposium, pages 109--126.]] Google Scholar
- Chen, H. and Wagner, D. 2002. MOPS: An infrastructure for examining security properties of software. In Proceedings of the Conference on Computer and Communication Section.]] Google Scholar
- Cousot, P. and Cousot, R. 1977. Static determination of dynamic properties of recursive procedures. In IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., CA, E.J. Neuhold (Ed.), pages 237--277, St-Andrews, N.B., Canada.]]Google Scholar
- Caucal, B. and Monfort, R. 1990. On the transition graphs of automata and grammars. In Graph Theoretic Concepts in Computer Science, Springer LNCS 484, pages 311--337.]] Google Scholar
- Emerson, A. 1990. Modal and temporal logic. In Handbook of Theoretical Computer Science, Volume B, pages 995--1072, MIT Press.]]Google Scholar
- Emerson, A. and Lei, C. 1986. Efficient model-checking in fragments of the propositional mu-calculus. In LICS 98, pages 267--278.]]Google Scholar
- Esparza, J., Hansel, D., Rossmanith, P., and Schwoon, S. 2000. Efficient algorithms for model checking pushdown systems. In Computer Aided Verification, 12th International Conference, volume 1855 of LNCS, pages 232--247. Springer.]] Google Scholar
- Etessami, K. 2004. Analysis of recursive game graphs using data flow equations. In 5th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS, pages 282--296. Springer.]]Google Scholar
- Finkel, A., Willems, B., and Wolper, P. 1997. A direct symbolic approach to model checking pushdown systems. In Infinity'97 Workshop, volume 9 of Electronic Notes in Theoretical Computer Science.]]Google Scholar
- GrammaTech, Inc. 2000. CodeSurfer System. “http://www.grammatech.com/products/ codesurfer/”.]]Google Scholar
- Harel, D. 1987. Statecharts: A visual formalism for complex systems. Sci. Comput. Prog. 8, 231--274.]] Google Scholar
- Heintze, N. and McAllester, D. A. 1997. On the cubic bottleneck in subtyping and flow analysis. In Proceedings of Logic in Computer Science, pages 342--351.]] Google Scholar
- Horwitz, S., Reps, T., and Binkley, D. 1990. Interprocedural slicing using dependence graphs. In Trans. Prog. Lang. Syst. 12, 1, 26--60.]] Google Scholar
- Horwitz, S., Reps, T., Bricker, T., and Rosay, G. 1997. Wisconsin Program-Slicing Tool. “http://www.cs.wisc.edu/wpis/slicing_tool/”.]]Google Scholar
- Horwitz, S., Reps, T., Sagiv, M., and Rosay, G. 1994. Speeding up slicing. In Proceedings of the 2nd ACM Symposium on Foundation of Software Engineering, pages 11--20.]] Google Scholar
- Melski, D. and Reps, T. 1999. Interprocedural path profiling. In Proceedings of the 8th Internatinal Conference on Compiler Construction, pages 47--62.]] Google Scholar
- Melski, D. and Reps, T. 2000. Interconvertibility of a class of set constraints and context-free-language reachability. Theoret. Comput. Sci., 248(1--2), 29--98.]] Google Scholar
- Reps, T. 1998. Program analysis via graph reachability. Info. Soft. Tech. 40(11--12), 701--726.]]Google Scholar
- Reps, T., Horwitz, S., and Sagiv, S. 1995. Precise interprocedural dataflow analysis via graph reachability. In POPL, pages 49--61.]] Google Scholar
- Reps, T. and Rosay, G. 1995. Precise interprocedural chopping. In Proceedings of the 3rd ACM Symposium on Foundation of Software Engineering, pages 41--52.]] Google Scholar
- Reps, T., Schwoon, S., and Jha, S. 2003. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Proceedings of the 10th Static Analysis Symposium, pages 189--213.]] Google Scholar
- Sagiv, M., Reps, T., and Horwitz, S. 1996. Precise interprocedural dataflow analysis with applications to constant propagation. Theoret. Comput. Sci. 167(1--2), 131--170.]] Google Scholar
- Schwoon, S. 2002. Moped System. “http://www.fmi.uni-stuttgart.de/szs/tools/moped/”.]]Google Scholar
- Schwoon, S., Reps, T., and Jha, S. 2003. Weighted PDS Library. “http://www.fmi. uni-stuttgart.de/szs/tools/wpds/”.]]Google Scholar
- Schwoon, S., Jha, S., Reps, T., and Stubblebine, S. 2003. On generalized authorization problems. In Proceedings of the 16th Computer Section Foundations Workshop, pages 202--218.]]Google Scholar
- Ball, T. and Rajamani, S. 2000. SLAM Toolkit. “http://research.microsoft.com/slam/”.]]Google Scholar
- Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S.S. Muchnick and N.D. Jones (eds.), Prentice-Hall, Englewood Cliffs, NJ, pages 189--234.]]Google Scholar
- Ullman, J. D. 1988. Principles of Database and Knowledge-base systems. Computer Science Press.]] Google Scholar
- Valiant, L. G. 1975. General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10, 308--315.]]Google Scholar
- Vardi, M. and Wolper, P. 1986. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Softw. 32, 2, 183--221.]] Google Scholar
- Walukiewicz, I. 2001. Pushdown processes: Games and model-checking. Information and Computation 164, 2, 234--263.]] Google Scholar
- Yannakakis, M. 1990. Graph-theoretic methods in database theory. In Proceedings of the 9th ACM Symposium on Principles of Database Systems, pages 230--242.]] Google Scholar
- Woods, W. A. 1970. Transition network grammars for natural language analysis. Commun. ACM 13, 10, 591--606.]] Google Scholar
- WPDS++: 2004. A C++ Library for Weighted Pushdown Systems, University of Wisconsin.]]Google Scholar
Index Terms
- Analysis of recursive state machines
Recommendations
Visibly pushdown languages
STOC '04: Proceedings of the thirty-sixth annual ACM symposium on Theory of computingWe propose the class of visibly pushdown languages as embeddings of context-free languages that is rich enough to model program analysis questions and yet is tractable and robust like the class of regular languages. In our definition, the input symbol ...
Subcubic algorithms for recursive state machines
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe 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 ...
Analysis of Recursive State Machines
CAV '01: Proceedings of the 13th International Conference on Computer Aided VerificationRecursive state machines (RSMs) enhance the power of ordinary state machines by allowing vertices to correspond either to ordinary states or to potentially recursive invocations of other state machines. RSMs can model the control flow in sequential ...
Comments