Unboundedness and downward closures of higher-order pushdown automata

Matthew Hague; Jonathan Kochems; C.-H. Luke Ong

doi:10.1145/2837614.2837627

Unboundedness and downward closures of higher-order pushdown automata

Matthew Hague, Jonathan Kochems, C.-H. Luke Ong

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

112 Downloads (Pure)

Abstract

We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.

Original language	English
Title of host publication	Principles of Programming Languages
Subtitle of host publication	POPL '16
Place of Publication	New York, NY
Publisher	ACM
Pages	151-163
Number of pages	13
ISBN (Print)	978-1-4503-3549-2
DOIs	https://doi.org/10.1145/2837614.2837627
Publication status	Published - 11 Jan 2016

Keywords

Higher-Order Programs
Functional Programs
Model-Checking
Verification
Formal Languages
Downward Closures
Parikh Images
Concurrency
Automata
Pushdown Automata

Access to Document

10.1145/2837614.2837627

Accepted ManuscriptAccepted author manuscript, 208 KB

Verification of Concurrent and Higher-Order Recursive Programs
Hague, M. (PI)
Eng & Phys Sci Res Council EPSRC
1/05/13 → 30/04/18
Project: Research

Cite this

@inproceedings{0f3c0b5d84cf4a15b7d54651138d34bd,

title = "Unboundedness and downward closures of higher-order pushdown automata",

abstract = "We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.",

keywords = "Higher-Order Programs, Functional Programs, Model-Checking, Verification, Formal Languages, Downward Closures, Parikh Images, Concurrency, Automata, Pushdown Automata",

author = "Matthew Hague and Jonathan Kochems and Ong, {C.-H. Luke}",

year = "2016",

month = jan,

day = "11",

doi = "10.1145/2837614.2837627",

language = "English",

isbn = "978-1-4503-3549-2",

pages = "151--163",

booktitle = "Principles of Programming Languages",

publisher = "ACM",

}

TY - GEN

T1 - Unboundedness and downward closures of higher-order pushdown automata

AU - Hague, Matthew

AU - Kochems, Jonathan

AU - Ong, C.-H. Luke

PY - 2016/1/11

Y1 - 2016/1/11

N2 - We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.

AB - We show the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes.

KW - Higher-Order Programs

KW - Functional Programs

KW - Model-Checking

KW - Verification

KW - Formal Languages

KW - Downward Closures

KW - Parikh Images

KW - Concurrency

KW - Automata

KW - Pushdown Automata

U2 - 10.1145/2837614.2837627

DO - 10.1145/2837614.2837627

M3 - Conference contribution

SN - 978-1-4503-3549-2

SP - 151

EP - 163

BT - Principles of Programming Languages

PB - ACM

CY - New York, NY

ER -

Unboundedness and downward closures of higher-order pushdown automata

Abstract

Keywords

Access to Document

Projects

Verification of Concurrent and Higher-Order Recursive Programs

Cite this