一句话：证明定时寄存器下推自动机的非空性可判定，并给出两个相关系统的指数时间判定结果。
论文研究定时寄存器下推自动机的非空性问题。该模型允许转移同时涉及状态时钟和栈顶时钟，且时钟差可以无界，因此严格包含 Bouajjani 等人的下推时间自动机、Abdulla 等人的稠密时间下推自动机以及 Clemente 和 Lasota 的轨道有限定时寄存器下推自动机。文章证明该非空性问题可在双指数时间内判定。作为证明过程中的独立结果，论文还证明了两类问题的可判定性：整数集合上带加法、并集及与 N 和 -N 的交的方程组最小解非空性，以及带状态和减法的单维分支向量加法系统的可达性；二者均可在指数时间内判定。
We prove that non-emptiness of timed register pushdown automata is decidable in doubly exponential time. This is a very expressive class of automata, whose transitions may involve state and top-of-stack clocks with unbounded differences. It strictly subsumes pushdown timed automata of Bouajjani et al., dense-timed pushdown automata of Abdulla et al., and orbit-finite timed register pushdown automata of Clemente and Lasota. Along the way, we prove two further decidability results of independent interest: for non-emptiness of least solutions to systems of equations over sets of integers with addition, union and intersections with ℕ and -ℕ, and for reachability in one-dimensional branching vector addition systems with states and subtraction, both in exponential time.