Article

Higher-Order Pushdown Trees Are Easy

Authors:

Damian Niwinski,

Pawel UrzyczynAuthors Info & Claims

FoSSaCS '02: Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures

Pages 205 - 222

Published: 08 April 2002 Publication History

Abstract

We show that the monadic second-order theory of an infinite tree recognized by a higher-order pushdown automaton of any level is decidable. We also show that trees recognized by pushdown automata of level n coincide with trees generated by safe higher-order grammars of level n . Our decidability result extends the result of Courcelle on algebraic(pushdo wn of level 1) trees and our own result on trees of level 2.

References

[1]

D. Caucal. On infinite transition graphs having a decidable monadic second-order theory. In F. Meyer auf der Heide and B. Monien, editors, 23th International Colloquium on Automata Languages and Programming , LNCS 1099, pages 194- 205, 1996. A long version will appear in tCS.

[2]

B. Courcelle. The monadic second-order theory of graphs IX: Machines and their behaviours. Theoretical Comput. Sci. , 151:125-162, 1995.

[3]

B. Courcelle and T. Knapik. The evaluation of first-order substitution is monadic second-order compatible. Theoretical Comput. Sci. , 2002. to appear.

[4]

W. Damm. the IO- and OI-hierarchies. Theoretical Comput. Sci. , 20(2):95-208, 1982.

[5]

W. Damm and A. Goerdt. An automata-theoreticc haracterization of the OI-hierarchy. Information and Control , 71:1-32, 1986.

[6]

J. Engelfriet. Iterated push-down automata and complexity classes. In Proc. 15th StOC , pages 365-373, 1983.

[7]

H. Hungar. Model checking and higher-order recursion. In L. Pacholski, M. Kuty8lowski and t. Wierzbicki, editors, Mathematical Foundations of Computer Science 1999 , LNCS 1672, pages 149-159, 1999.

[8]

B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. Bulletin of EATCS , 1997(62):222-259.

[9]

A.J. Kfoury, J. Tiuryn and P. Urzyczyn. On the expressive power of finitely typed and universally polymorphic recursive procedures. Theoretical Comput. Sci. , 93:1- 41, 1992.

[10]

A. Kfoury and P. Urzyczyn. Finitely typed functional programs, part II: comparisons to imperative languages. Report, Boston University, 1988.

[11]

T. Knapik, D. Niwi'ski, and P. Urzyczyn. Deciding monadic theories of hyperal-gebraictrees. In Typed Lambda Calculi and Applications, 5th International Conference , LNCS 2044, pages 253-267. Springer-Verlag, 2001.

[12]

W. Kowalczyk, D. Niwi'ski, and J. Tiuryn. A generalization of of Cook's auxiliary-pushdown- automata theorem. Fundamenta Informaticae , 12:497-506, 1989.

[13]

O. Kupferman and M. Vardi. An automata-theoretic approach to reasoning about infinite-state systems. In Computer Aided Verification, Proc. 12th Int. Conference , Lecture Notes in Computer Science. Springer-Verlag, 2000.

[14]

D. Muller and P. Schupp. The theory of ends, pushdown automata, and second-order logic. Theoretical Comput. Sci. , 37:51-75, 1985.

[15]

M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Soc , 141:1-35, 1969.

[16]

W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages , volume 3, pages 389-455. Springer-Verlag, 1997.

[17]

J. Tiuryn. Higher-order arrays and stacks in programming: An application of complexity theory to logics of programs. In Proc. 12th MFCS , LNCS 233, pages 177-198. Springer-Verlag, 1986.

[18]

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

Cited By

Kobayashi NLago UGrellois CBouyer P(2019)On the termination problem for probabilistic higher-order recursive programsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470177(1-14)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470177
Watanabe KTsukada TOshikawa HKobayashi NHermenegildo MIgarashi A(2019)Reduction from branching-time property verification of higher-order programs to HFL validity checkingProceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3294032.3294077(22-34)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3294032.3294077
Melliès PAceto LIngólfsdóttir A(2017)Higher-order parity automataProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330012(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330012
Show More Cited By

Higher-Order Pushdown Trees Are Easy
1. Software and its engineering
  1. Software notations and tools
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

First-Order Logic on Higher-Order Nested Pushdown Trees

We introduce a new hierarchy of higher-order nested pushdown trees generalising Alur et al.’s concept of nested pushdown trees. Nested pushdown trees are useful representations of control flows in the verification of programs with recursive calls of ...
Flip-pushdown automata: nondeterminism is better than determinism
DLT'03: Proceedings of the 7th international conference on Developments in language theory

Flip-pushdown automata are pushdown automata with the additional ability to flip or reverse its pushdown. We investigate deterministic and nondeterministic flip-pushdown automata accepting by final state or empty pushdown. In particular, for ...
Reversible pushdown automata

Reversible pushdown automata are deterministic pushdown automata that are also backward deterministic. Therefore, they have the property that any configuration occurring in any computation has exactly one predecessor. In this paper, the computational ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FoSSaCS '02: Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures

April 2002

435 pages

ISBN:354043366X

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 April 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

59
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kobayashi NLago UGrellois CBouyer P(2019)On the termination problem for probabilistic higher-order recursive programsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470177(1-14)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470177
Watanabe KTsukada TOshikawa HKobayashi NHermenegildo MIgarashi A(2019)Reduction from branching-time property verification of higher-order programs to HFL validity checkingProceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3294032.3294077(22-34)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3294032.3294077
Melliès PAceto LIngólfsdóttir A(2017)Higher-order parity automataProceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3329995.3330012(1-12)Online publication date: 20-Jun-2017
https://dl.acm.org/doi/10.5555/3329995.3330012
Kobayashi NLozes ÉBruse F(2017)On the relationship between higher-order recursion schemes and higher-order fixpoint logicACM SIGPLAN Notices10.1145/3093333.300985452:1(246-259)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009854
Kobayashi NLozes ÉBruse FCastagna GGordon A(2017)On the relationship between higher-order recursion schemes and higher-order fixpoint logicProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009854(246-259)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009854
Penelle V(2017)Rewriting Higher-Order Stack TreesTheory of Computing Systems10.1007/s00224-017-9769-661:2(536-580)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s00224-017-9769-6
Sin'Ya RAsada KKobayashi NTsukada T(2017)Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction SequenceProceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 1020310.1007/978-3-662-54458-7_4(53-68)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54458-7_4
Ong C(2017)Automata, Logic and Games for the $$\lambda $$-CalculusProceedings of the 7th Indian Conference on Logic and Its Applications - Volume 1011910.1007/978-3-662-54069-5_3(23-26)Online publication date: 5-Jan-2017
https://dl.acm.org/doi/10.1007/978-3-662-54069-5_3
Walukiewicz I(2016)Automata theory and higher-order model-checkingACM SIGLOG News10.1145/3026744.30267453:4(13-31)Online publication date: 15-Dec-2016
https://dl.acm.org/doi/10.1145/3026744.3026745
Hague MKochems JOng C(2016)Unboundedness and downward closures of higher-order pushdown automataACM SIGPLAN Notices10.1145/2914770.283762751:1(151-163)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837627
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents