Zenoness for Timed Pushdown Automata

TL;DR

This paper investigates the zenoness problem in dense-timed pushdown automata, establishing its EXPTIME-completeness, thereby advancing understanding of the computational complexity of these automata models.

Contribution

It proves that the zenoness problem for dense-timed pushdown automata is EXPTIME-complete, extending previous decidability results.

Findings

Zenoness problem is EXPTIME-complete for dense-timed pushdown automata.

Decidability of reachability was previously established for this model.

The complexity classification clarifies the computational difficulty of analyzing zenoness.

Abstract

Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clocks and the age of the topmost symbol. Therefore, dense-timed pushdown automata subsume both pushdown automata and timed automata. We have previously shown that the reachability problem for this model is decidable. In this paper, we study the zenoness problem and show that it is EXPTIME-complete.