Matthew Hague
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.
- K. Aehlig, J. G. de Miranda, and C.-H. L. Ong. Safety is not a restriction at level 2 for string languages. In FOSSACS, 2005. Google Scholar
Digital Library
- A. V. Aho. Indexed grammars - an extension of context-free grammars. J. ACM, 15(4):647–671, 1968. Google ScholarDigital Library
- M. Bojanczyk. Beyond omega-regular languages. In STACS, 2010.Google Scholar
- A. Bouajjani, M. Müller-Olm, and T. Touili. Regular symbolic analysis of dynamic networks of pushdown systems. In CONCUR, 2005. Google ScholarDigital Library
- C. H. Broadbent and N. Kobayashi. Saturation-based model checking of higher-order recursion schemes. In CSL, 2013.Google Scholar
- C. H. Broadbent, A. Carayol, C.-H. L. Ong, and O. Serre. Recursion schemes and logical reflection. In LICS, 2010. Google ScholarDigital Library
- C. H. Broadbent, A. Carayol, M. Hague, and O. Serre. A saturation method for collapsible pushdown systems. In ICALP, 2012. Google ScholarDigital Library
- C. H. Broadbent, A. Carayol, M. Hague, and O. Serre. C-shore: a collapsible approach to higher-order verification. In ICFP, 2013. Google ScholarDigital Library
- B. Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 44:178–186, 1991.Google Scholar
- A. Cyriac, P. Gastin, and K. N. Kumar. MSO decidability of multipushdown systems via split-width. In CONCUR, 2012. Google ScholarDigital Library
- W. Czerwinski and W. Martens. A note on decidable separability by piecewise testable languages. CoRR, abs/1410.1042, 2014. URL http://arxiv.org/abs/1410.1042.Google Scholar
- J. Esparza and P. Ganty. Complexity of pattern-based verification for multithreaded programs. In POPL, 2011. Google ScholarDigital Library
- J. Esparza and A. Podelski. Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In POPL, 2000. Google ScholarDigital Library
- J. Esparza, A. Kucera, and S. Schwoon. Model checking LTL with regular valuations for pushdown systems. Inf. Comput., 186(2):355– 376, 2003. Google ScholarDigital Library
- M. Hague. Saturation of concurrent collapsible pushdown systems. In FSTTCS, 2013.Google Scholar
- M. Hague. Senescent ground tree rewrite systems. In CSL-LICS, 2014. Google ScholarDigital Library
- M. Hague and A. W. Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, 2012. Google ScholarDigital Library
- M. Hague, A. S. Murawski, C.-H. L. Ong, and O. Serre. Collapsible pushdown automata and recursion schemes. In LICS, 2008. Google ScholarDigital Library
- M. Hague, J. Kochems, and C. L. Ong. Unboundedness and downward closures of higher-order pushdown automata. CoRR, abs/1507.03304, 2015. URL http://arxiv.org/abs/1507.03304.Google Scholar
- L. Haines. On free monoids partially ordered by embedding. J. Combinatorial Theory, 6:9498, 1969.Google ScholarCross Ref
- V. Kahlon. Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise CFL-reachability for threads communicating via locks. In LICS, 2009. Google ScholarDigital Library
- T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In FOSSACS, 2002. Google ScholarDigital Library
- T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. In ICALP, 2005. Google ScholarDigital Library
- N. Kobayashi. Model-checking higher-order functions. In PPDP, 2009. Google ScholarDigital Library
- N. Kobayashi. GTR EC S2: A model checker for recursion schemes based on games and types. A tool available at http://www-kb.is. s.u-tokyo.ac.jp/~koba/gtrecs2/, 2012.Google Scholar
- N. Kobayashi and A. Igarashi. Model-checking higher-order programs with recursive types. In ESOP, 2013. Google ScholarDigital Library
- N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and cegar for higher-order model checking. In PLDI, 2011. Google ScholarDigital Library
- A. Lal and T. W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. FMSD, 35(1):73–97, 2009. Google ScholarDigital Library
- P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL, 2011. Google ScholarDigital Library
- A. N. Maslov. Multilevel stack automata. Problems of Information Transmission, 15:1170–1174, 1976.Google Scholar
- R. P. Neatherway, S. J. Ramsay, and C.-H. L. Ong. A traversal-based algorithm for higher-order model checking. In ICFP, 2012. Google ScholarDigital Library
- P. Parys. On the significance of the collapse operation. In LICS, 2012. Google ScholarDigital Library
- V. Penelle. Rewriting higher-order stack trees. In CSR, 2015.Google ScholarCross Ref
- G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst., 22(2):416–430, 2000. Google ScholarDigital Library
- S. J. Ramsay, R. P. Neatherway, and C.-H. L. Ong. A type-directed abstraction refinement approach to higher-order model checking. In POPL, 2014. Google ScholarDigital Library
- A. Seth. Games on higher order multi-stack pushdown systems. In RP, 2009. Google ScholarDigital Library
- S. L. Torre and M. Napoli. Reachability of multistack pushdown systems with scope-bounded matching relations. In CONCUR, 2011.Google ScholarCross Ref
- S. L. Torre, A. Muscholl, and I. Walukiewicz. Safety of parametrized asynchronous shared-memory systems is almost always decidable. In CONCUR, 2015. To appear.Google Scholar
- H. Unno, N. Tabuchi, and N. Kobayashi. Verification of treeprocessing programs via higher-order model checking. In APLAS, 2010. Google ScholarDigital Library
- J. van Leeuwen. Effective constructions in well-partially-ordered free monoids. Discrete Mathematics, 21(3):237252, 1978. Google ScholarDigital Library
- G. Zetzsche. An approach to computing downward closures. In ICALP, 2015.Google ScholarDigital Library
Index Terms
- Unboundedness and downward closures of higher-order pushdown automata
Recommendations
Unboundedness and downward closures of higher-order pushdown automata
POPL '16We 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 ...
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 ...
Left-most derivation and shadow-pushdown automata for context-sensitive languages
ICCOMP'06: Proceedings of the 10th WSEAS international conference on ComputersIn this paper left-most derivation for context-sensitive grammars is presented based on Penttonen one-sided normal-form. The derivations using grammars in normal form are represented by tree-like graphs. Left-most derivation is defined in the sense of ...
Comments