Visibly pushdown languages

ABSTRACT

We 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 determines when the pushdown automaton can push or pop, and thus the stack depth at every position. We show that the resulting class Vpl of languages is closed under union, intersection, complementation, renaming, concatenation, and Kleene-*, and problems such as inclusion that are undecidable for context-free languages are Exptime-complete for visibly pushdown automata. Our framework explains, unifies, and generalizes many of the decision procedures in the program analysis literature, and allows algorithmic verification of recursive programs with respect to many context-free properties including access control properties via stack inspection and correctness of procedures with respect to pre and post conditions. We demonstrate that the class Vpl is robust by giving two alternative characterizations: a logical characterization using the monadic second order (MSO) theory over words augmented with a binary matching predicate, and a correspondence to regular tree languages. We also consider visibly pushdown languages of infinite words and show that the closure properties, MSO-characterization and the characterization in terms of regular trees carry over. The main difference with respect to the case of finite words turns out to be determinizability: nondeterministic Büchi visibly pushdown automata are strictly more expressive than deterministic Muller visibly pushdown automata.

REFERENCES

• 1: Jean-Michel Autebert , Jean Berstel , Luc Boasson, Context-free languages and pushdown automata, Handbook of formal languages, vol. 1: word, language, grammar, Springer-Verlag New York, Inc., New York, NY, 1997
• 2: R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. To appear in Proc. of Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS'04, Spain, LNCS 2988. Springer, 2004.
• 3: Rajeev Alur , Kousha Etessami , Mihalis Yannakakis, Analysis of Recursive State Machines, Proceedings of the 13th International Conference on Computer Aided Verification, p.207-220, July 18-22, 2001
• 4: Jean Berstel , Luc Boasson, Balanced grammars and their languages, Formal and natural computing, Springer-Verlag New York, Inc., New York, NY, 2002
• 5: 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
• 6: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 7: 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
• 8: A. Bouquet, O. Serre and I. Walukiewicz. Pushdown games with unboundedness and regular conditions. To appear in Foundations of Software Technology and Theoretical Computer Science (FSTTCS), December 2003.
• 9: H. Comon, M. Dauchet, R. Gilleron, D. Lugiez, S. Tison and M. Tommasi. Tree automata techniques and applications. Draft, Available at http://www. grappa. univ-lille3. fr/tata/, 2002.
• 10: Thierry Cachat , Jacques Duparc , Wolfgang Thomas, Solving Pushdown Games with a Sigma3 Winning Condition, Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, p.322-336, September 22-25, 2002
• 11: R. S. Cohen and A. Y. Gold. Theory of omega-Languages. I. Characterizations of omega-Context-Free Languages. JCSS 15(2): 169--184, 1977.
• 12: K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T. A. Henzinger, and J. Palsberg. Stack size analysis for interrupt driven programs. In Proceedings of the 10th International Symposium on Static Analysis, volume LNCS 2694, pages 109--126, 2003.
• 13: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 14: Javier Esparza , Antonín Kucera , Stefan Schwoon, Model checking LTL with regular valuations for pushdown systems, Information and Computation, v.186 n.2, p.355-376, 01 November 2003 [doi>10.1016/S0890-5401(03)00139-1]
• 15: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 16: David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
• 17: T. Jensen, D. Le Metayer, and T. Thorn. Verification of control flow based security properties. In Proceedings of the IEEE Symposium on Security and Privacy, pages 89--103, 1999.
• 18: D. E. Knuth. A characterization of parenthesis languages. Information and Control, 11(3):269--289, 1967.
• 19: Clemens Lautemann , Thomas Schwentick , Denis Thérien, Logics For Context-Free Languages, Selected Papers from the 8th International Workshop on Computer Science Logic, p.205-216, September 25-30, 1994
• 20: Robert McNaughton, Parenthesis Grammars, Journal of the ACM (JACM), v.14 n.3, p.490-500, July 1967 [doi>10.1145/321406.321411]
• 21: 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]
• 22: S. Safra. On the complexity of $omega$-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 319--327, 1988.
• 23: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 24: M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First IEEE Symposium on Logic in Computer Science, pages 332--344, 1986.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Decision problems; Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
ω-languages, context-free languages, logic, pushdown automata, regular tree languages, verification