Reachability in pushdown register automata

作者：

Highlights：

• We look at the complexity of reachability for automata over infinite alphabets equipped with registers and a stack.

• We show that local reachability is EXPTIME-complete.

• We give an EXPTIME saturation algorithm for global reachability.

• We show that reachability is undecidable for higher-order register pushdown automata even at order 2.

摘要

•We look at the complexity of reachability for automata over infinite alphabets equipped with registers and a stack.•We show that local reachability is EXPTIME-complete.•We give an EXPTIME saturation algorithm for global reachability.•We show that reachability is undecidable for higher-order register pushdown automata even at order 2.

论文关键词：Register automata,Pushdown automata,Reachability,Infinite alphabets,Complexity

论文评审过程：Received 19 November 2014, Revised 9 January 2017, Accepted 13 February 2017, Available online 8 March 2017, Version of Record 11 April 2017.

论文官网地址：https://doi.org/10.1016/j.jcss.2017.02.008