Zenoness for Timed Pushdown Automata
Parosh Aziz Abdulla (Uppsala University), Mohamed Faouzi Atig (Uppsala, University), Jari Stenman (Uppsala University)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Parallel Computing and Optimization Techniques · Embedded Systems Design Techniques
