Article

Visibly pushdown games

Authors:

Christof Löding,

Olivier SerreAuthors Info & Claims

FSTTCS'04: Proceedings of the 24th international conference on Foundations of Software Technology and Theoretical Computer Science

Pages 408 - 420

https://doi.org/10.1007/978-3-540-30538-5_34

Published: 16 December 2004 Publication History

Abstract

The class of visibly pushdown languages has been recently defined as a subclass of context-free languages with desirable closure properties and tractable decision problems. We study visibly pushdown games, which are games played on visibly pushdown systems where the winning condition is given by a visibly pushdown language. We establish that, unlike pushdown games with pushdown winning conditions, visibly pushdown games are decidable and are 2Exptime-complete. We also show that pushdown games against Ltl specifications and Caret specifications are 3Exptime-complete. Finally, we establish the topological complexity of visibly pushdown languages by showing that they are a subclass of Boolean combinations of Σ₃ sets. This leads to an alternative proof that visibly pushdown automata are not determinizable and also shows that visibly pushdown games are determined.

References

[1]

R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. In TACAS'04, volume 2988 of LNCS, pages 467-481. Springer, 2004.

[2]

R. Alur and P. Madhusudan. Visibly pushdown languages. In Proceedings of the 36th Annual ACM Symposium on Theory of Computing, STOC '04, 2004.

Digital Library

[3]

T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 2000, volume 1885 of LNCS, pages 113-130. Springer, 2000.

Digital Library

[4]

A. Bouquet, O. Serre, and I. Walukiewicz. Pushdown games with the unboundedness and regular conditions. In Proceedings of FSTTCS'03, volume 2914 of LNCS, pages 88-99. Springer, 2003.

[5]

T. Cachat, J. Duparc, and W. Thomas. Solving pushdown games with a Σ3 winning condition. In CSL'02, volume 2471 of LNCS, pages 322-336. Springer, 2002.

Digital Library

[6]

E.A. Emerson, C.S. Jutla, and A.P. Sistla. On model-checking for fragments of µ-calculus. In CAV '93, volume 697 of LNCS, pages 385-396. Springer, 1993.

Digital Library

[7]

A.S. Kechris. Classical Descriptive Set Theory, volume 156 of Graduate texts in mathematics. Springer Verlag, 1994.

[8]

D. A. Martin. Borel Determinacy. Annals of Mathematics, 102:363-371, 1975.

[9]

A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symposium on Principles of Programming Languages, Austin, January 1989.

Digital Library

[10]

T. Reps, S. Horwitz, and S. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proc. of ACM Symp. POPL, pages 49-61, 1995.

Digital Library

[11]

O. Serre. Games with winning conditions of high borel complexity. In Proceedings of ICALP'04, volume 3142 of LNCS, pages 1150-1162. Springer, 2004.

[12]

L. Staiger. Handbook of Formal Language Theory, volume III, chapter ?- Languages, pages 339-387. Springer, 1997.

Digital Library

[13]

W. Thomas. Handbook of Formal Language Theory, volume III, chapter Languages, Automata, and Logic, pages 389-455. Springer, 1997.

Digital Library

[14]

W. Thomas. A short introduction to infinite automata. In Proceedings of DLT '01, volume 2295 of LNCS, pages 130-144. Springer, 2002.

Digital Library

[15]

I. Walukiewicz. Pushdown processes: Games and model checking. Information and Computation, 164(2), January 2001.

Digital Library

[16]

I. Walukiewicz. A landscape with games in the background. In Proceedings of LICS'04, Invited talk, 2004. To appear.

Digital Library

[17]

W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. TCS, 200(1-2):135-183, 1998.

Digital Library

Cited By

Selivanov V(2023)Extending Wagner’s Hierarchy to Deterministic Visibly Pushdown AutomataUnity of Logic and Computation10.1007/978-3-031-36978-0_16(190-201)Online publication date: 24-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-36978-0_16
Ogawa MOkhotin A(2022)On the Determinization of Event-Clock Input-Driven Pushdown AutomataComputer Science – Theory and Applications10.1007/978-3-031-09574-0_16(256-268)Online publication date: 29-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-09574-0_16
Okhotin ASelivanov V(2021)Input-Driven Pushdown Automata on Well-Nested Infinite StringsComputer Science – Theory and Applications10.1007/978-3-030-79416-3_21(349-360)Online publication date: 28-Jun-2021
https://dl.acm.org/doi/10.1007/978-3-030-79416-3_21
Show More Cited By

Recommendations

Visibly Pushdown Automata and Transducers with Counters
Non-Classical Models of Automata and Applications VI

We generalize the models of visibly pushdown automata (VPDAs) and visibly pushdown transducers (VPDTs) by equipping them with reversal-bounded counters. We show that some of the results for VPDAs and VPDTs (e.g., closure under intersection and ...
Properties of visibly pushdown transducers
MFCS'10: Proceedings of the 35th international conference on Mathematical foundations of computer science

Visibly pushdown transducers (VPTs) form a strict subclass of pushdown transducers (PTs) that extends finite state transducers with a stack. Like visibly pushdown automata, the input symbols determine the stack operations. It has been shown that visibly ...
Visibly pushdown languages
STOC '04: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FSTTCS'04: Proceedings of the 24th international conference on Foundations of Software Technology and Theoretical Computer Science

December 2004

530 pages

ISBN:3540240586

Editors:
Kamal Lodaya
The Institute of Mathematical Sciences, CIT Campus, Chennai, India
,
Meena Mahajan
The Institute of Mathematical Sciences, CIT Campus, Chennai, India

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 16 December 2004

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Selivanov V(2023)Extending Wagner’s Hierarchy to Deterministic Visibly Pushdown AutomataUnity of Logic and Computation10.1007/978-3-031-36978-0_16(190-201)Online publication date: 24-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-36978-0_16
Ogawa MOkhotin A(2022)On the Determinization of Event-Clock Input-Driven Pushdown AutomataComputer Science – Theory and Applications10.1007/978-3-031-09574-0_16(256-268)Online publication date: 29-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-09574-0_16
Okhotin ASelivanov V(2021)Input-Driven Pushdown Automata on Well-Nested Infinite StringsComputer Science – Theory and Applications10.1007/978-3-030-79416-3_21(349-360)Online publication date: 28-Jun-2021
https://dl.acm.org/doi/10.1007/978-3-030-79416-3_21
Lange M(2019)Specifying Program Properties Using Modal Fixpoint Logics: A Survey of ResultsLogic and Its Applications10.1007/978-3-662-58771-3_5(42-51)Online publication date: 1-Mar-2019
https://dl.acm.org/doi/10.1007/978-3-662-58771-3_5
Chen TSong FWu Z(2016)Verifying pushdown multi-agent systems against strategy logicsProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence10.5555/3060621.3060647(180-186)Online publication date: 9-Jul-2016
https://dl.acm.org/doi/10.5555/3060621.3060647
Chen TSong FWu Z(2016)Global model checking on pushdown multi-agent systemsProceedings of the Thirtieth AAAI Conference on Artificial Intelligence10.5555/3016100.3016243(2459-2465)Online publication date: 12-Feb-2016
https://dl.acm.org/doi/10.5555/3016100.3016243
De Crescenzo ILa Torre S(2016)A General Modular Synthesis Problem for Pushdown SystemsProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_24(495-513)Online publication date: 17-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-662-49122-5_24
Friedmann OKlaedtke FLange M(2015)Ramsey-Based Inclusion Checking for Visibly Pushdown AutomataACM Transactions on Computational Logic10.1145/277422116:4(1-24)Online publication date: 26-Aug-2015
https://dl.acm.org/doi/10.1145/2774221
Bozzelli LSánchez C(2014)Visibly rational expressionsActa Informatica10.5555/2697445.269768351:1(25-49)Online publication date: 1-Feb-2014
https://dl.acm.org/doi/10.5555/2697445.2697683
Droste MDück S(2014)Weighted Automata and Logics for Infinite Nested WordsProceedings of the 8th International Conference on Language and Automata Theory and Applications - Volume 837010.1007/978-3-319-04921-2_26(323-334)Online publication date: 10-Mar-2014
https://dl.acm.org/doi/10.1007/978-3-319-04921-2_26
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents