Average Stack Cost of Buechi Pushdown Automata
Jakub Michaliszyn, Jan Otop

TL;DR
This paper introduces the average stack cost problem for Buechi pushdown automata, providing a polynomial-time solution to determine if an accepting run exists with average stack costs below a threshold, enabling quantitative analysis of pushdown systems.
Contribution
It defines the average stack cost problem for Buechi PDA, generalizes mean-payoff objectives, and offers a polynomial-time algorithm for solving this problem.
Findings
The ASC problem can be solved in polynomial time.
The approach generalizes mean-payoff objectives.
Enables quantitative analysis like average response time.
Abstract
We study the average stack cost of Buechi pushdown automata (Buechi PDA). We associate a non-negative price with each stack symbol and define the cost of a stack as the sum of costs of all its elements. We introduce and study the average stack cost problem (ASC), which asks whether there exists an accepting run of a given Buechi PDA such that the long-run average of stack costs is below some given threshold. The ASC problem generalizes mean-payoff objective and can be used to express quantitative properties of pushdown systems. In particular, we can compute the average response time using the ASC problem. We show that the ASC problem can be solved in polynomial time.
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
Topicssemigroups and automata theory · Formal Methods in Verification · Logic, programming, and type systems
