Rajeev Alur
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.
- J. Autebert, J. Berstel, L. Boasson. Context-free languages and pushdown automata. In Handbook of Formal Languages, Vol. 1, pages 111--174, Springer, 1997.]] Google Scholar
Digital Library
- 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.]]Google Scholar
- R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines. In Proc. of the 13th International Conference on Computer Aided Verification, LNCS 2102, pages 207--220. Springer, 2001.]] Google ScholarDigital Library
- J. Berstel and L. Boasson. Balanced grammars and their languages. In Formal and Natural Computing: Essays Dedicated to Grzegorz Rozenberg, LNCS 2300, pages 3--25. Springer, 2002.]] Google ScholarDigital Library
- A. Boujjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR'97: Concurrency Theory, Eighth International Conference, LNCS 1243, pages 135--150. Springer, 1997.]] Google ScholarDigital Library
- T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, pages 113--130. Springer, 2000.]] Google ScholarDigital Library
- O. Burkart and B. Steffen. Model checking for context-free processes. In CONCUR'92: Concurrency Theory, Third International Conference, LNCS 630, pages 123--137. Springer, 1992.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]]Google Scholar
- T. Cachat, J. Duparc and W. Thomas. Solving pushdown games with a Σ3 winning condition. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002, volume 2471 of Lecture Notes in Computer Science, pages 322--336. Springer, 2002.]] Google ScholarDigital Library
- R. S. Cohen and A. Y. Gold. Theory of omega-Languages. I. Characterizations of omega-Context-Free Languages. JCSS 15(2): 169--184, 1977.]]Google ScholarCross Ref
- 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.]] Google ScholarDigital Library
- H. Chen and D. Wagner. Mops: an infrastructure for examining security properties of software. In Proceedings of ACM Conference on Computer and Communications Security, pages 235--244, 2002.]] Google ScholarDigital Library
- J. Esparza, A. Kucera, and S. S. Schwoon. Model-checking LTL with regular valuations for pushdown systems. Information and Computation, 186(2):355--376, 2003.]] Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, G. C. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In CAV 02: Proc. of 14th Conf. on Computer Aided Verification, LNCS 2404, pages 526--538. Springer, 2002.]] Google ScholarDigital Library
- D. Harel, D. Kozen and J. Tiuryn. Dynamic Logic. MIT Press, 2000.]] Google ScholarDigital Library
- 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.]]Google ScholarCross Ref
- D. E. Knuth. A characterization of parenthesis languages. Information and Control, 11(3):269--289, 1967.]]Google ScholarCross Ref
- C. Lautemann, T. Schwentick and D. Therien. Logics For context-free languages. In Proceedings of Computer Science Logic, 8th International Workshop, CSL '94, Poland, LNCS 933, pages 205--216. Springer, 1994.]] Google ScholarDigital Library
- R. McNaughton. Parenthesis grammars. Journal of the ACM, 14(3):490--500, 1967.]] Google ScholarDigital Library
- T. Reps, S. Horwitz, and S. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 49--61, 1995.]] Google ScholarDigital Library
- S. Safra. On the complexity of $omega$-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 319--327, 1988.]]Google ScholarDigital Library
- W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133--191. Elsevier Science Publishers, 1990.]] Google ScholarDigital Library
- 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.]]Google Scholar
Index Terms
- Visibly pushdown languages
Recommendations
Two-Way Visibly Pushdown Automata and Transducers
LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer ScienceAutomata-logic connections are pillars of the theory of regular languages. Such connections are harder to obtain for transducers, but important results have been obtained recently for word-to-word transformations, showing that the three following models ...
Efficient determinization of visibly and height-deterministic pushdown automata
New algorithms for the determinization of nondeterministic visibly and nondeterministic real-time height-deterministic pushdown automata are presented. The algorithms improve the results of existing algorithms. They construct only accessible states and ...
Regulated nondeterminism in pushdown automata
A generalization of pushdown automata towards regulated nondeterminism is studied. The nondeterminism is governed in such a way that the decision, whether or not a nondeterministic rule is applied, depends on the whole content of the stack. More ...
Comments