skip to main content
10.1145/1007352.1007390acmconferencesArticle/Chapter ViewAbstractPublication PagesstocConference Proceedingsconference-collections
Article

Visibly pushdown languages

Published: 13 June 2004 Publication History

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]
J. Autebert, J. Berstel, L. Boasson. Context-free languages and pushdown automata. In Handbook of Formal Languages, Vol. 1, pages 111--174, Springer, 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]
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.]]
[4]
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.]]
[5]
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.]]
[6]
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.]]
[7]
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.]]
[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]
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.]]
[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]
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.]]
[14]
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.]]
[15]
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.]]
[16]
D. Harel, D. Kozen and J. Tiuryn. Dynamic Logic. MIT Press, 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]
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.]]
[20]
R. McNaughton. Parenthesis grammars. Journal of the ACM, 14(3):490--500, 1967.]]
[21]
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.]]
[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]
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.]]
[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.]]

Cited By

View all
  • (2024)Streaming enumeration on nested documentsACM Transactions on Database Systems10.1145/3701557Online publication date: 25-Oct-2024
  • (2024)Weighted Context-Free-Language Ordered Binary Decision DiagramsProceedings of the ACM on Programming Languages10.1145/36897608:OOPSLA2(1390-1419)Online publication date: 8-Oct-2024
  • (2024)V-Star: Learning Visibly Pushdown Grammars from Program InputsProceedings of the ACM on Programming Languages10.1145/36564588:PLDI(2003-2026)Online publication date: 20-Jun-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
STOC '04: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing
June 2004
660 pages
ISBN:1581138520
DOI:10.1145/1007352
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 June 2004

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. ω-languages
  2. context-free languages
  3. logic
  4. pushdown automata
  5. regular tree languages
  6. verification

Qualifiers

  • Article

Conference

STOC04
Sponsor:
STOC04: Symposium of Theory of Computing 2004
June 13 - 16, 2004
IL, Chicago, USA

Acceptance Rates

Overall Acceptance Rate 1,469 of 4,586 submissions, 32%

Upcoming Conference

STOC '25
57th Annual ACM Symposium on Theory of Computing (STOC 2025)
June 23 - 27, 2025
Prague , Czech Republic

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)47
  • Downloads (Last 6 weeks)4
Reflects downloads up to 18 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Streaming enumeration on nested documentsACM Transactions on Database Systems10.1145/3701557Online publication date: 25-Oct-2024
  • (2024)Weighted Context-Free-Language Ordered Binary Decision DiagramsProceedings of the ACM on Programming Languages10.1145/36897608:OOPSLA2(1390-1419)Online publication date: 8-Oct-2024
  • (2024)V-Star: Learning Visibly Pushdown Grammars from Program InputsProceedings of the ACM on Programming Languages10.1145/36564588:PLDI(2003-2026)Online publication date: 20-Jun-2024
  • (2024)Deciding Asynchronous Hyperproperties for Recursive ProgramsProceedings of the ACM on Programming Languages10.1145/36328448:POPL(33-60)Online publication date: 5-Jan-2024
  • (2024)Pearl: A Multi-Derivation Approach to Efficient CFL-Reachability SolvingIEEE Transactions on Software Engineering10.1109/TSE.2024.343768450:9(2379-2397)Online publication date: Sep-2024
  • (2024)From words to pictures: row-column combinations and Chomsky-Schützenberger theoremTheoretical Computer Science10.1016/j.tcs.2024.114598(114598)Online publication date: Apr-2024
  • (2024)On the power of pushing or stationary moves for input-driven pushdown automataTheoretical Computer Science10.1016/j.tcs.2024.114503(114503)Online publication date: Mar-2024
  • (2024)On the Decidability of Infix Inclusion ProblemTheory of Computing Systems10.1007/s00224-023-10160-w68:3(301-321)Online publication date: 13-Jan-2024
  • (2024)Exact Descriptional Complexity of Determinization of Input-Driven Pushdown AutomataImplementation and Application of Automata10.1007/978-3-031-71112-1_18(249-260)Online publication date: 3-Sep-2024
  • (2024)SMT-Based Symbolic Model-Checking for Operator Precedence LanguagesComputer Aided Verification10.1007/978-3-031-65627-9_19(387-408)Online publication date: 24-Jul-2024
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media