Paper Info
Title
Well-Structured pushdown systems
Abstract
Pushdown systems (PDSs) model single-thread recursive programs, and well-structured transition systems (WSTSs), such as vector addition systems, are useful to represent non-recursive multi-thread programs. Combining these two ideas, our goal is to investigate well-structured pushdown systems (WSPDSs), pushdown systems with well-quasi-ordered control states and stack alphabet. This paper focuses on subclasses of WSPDSs, in which the coverability becomes decidable. We apply WSTS-like techniques on classical P-automata. A Post*-automata (resp. Pre*-automata) construction is combined with Karp-Miller acceleration (resp. ideal representation) to characterize the set of successors (resp. predecessors) of given configurations. As examples, we show that the coverability is decidable for recursive vector addition system with states, multi-set pushdown systems, and a WSPDS with finite control states and well-quasi-ordered stack alphabet.
Year
DOI
Venue
2013
10.1007/978-3-642-40184-8_10
CONCUR
Keywords
Field
DocType
well-structured transition system,vector addition system,well-quasi-ordered control state,well-structured pushdown system,finite control state,multi-set pushdown system,recursive vector addition system,model single-thread recursive program,karp-miller acceleration,pushdown system
Embedded pushdown automaton,Discrete mathematics,Computer science,Deterministic pushdown automaton,Theoretical computer science,Decidability,Reachability problem,Pushdown automaton,Acceleration,Selection rule,Recursion
Conference
Citations 
PageRank 
References 
4
0.43
19
Authors
2
Name
Order
Citations
PageRank
Xiaojuan Cai1365.95
Mizuhito Ogawa213523.17