上海科技大学知识管理系统

Finite automata over infinite words (called omega-automata) play an important role in the automata-theoretic approach to system verification. Different types of omega-automata differ in their succinctness and complexity of their emptiness problems, as a result, theory of omega-automata has received considerable research attention. Pushdown automata over infinite words (called omega-PDAs), a generalization of omega-automata, are a natural model of recursive programs. Our goal in this paper is to conduct a relatively complete investigation on the complexity of the emptiness problems for variants of omega-PDAs. For this purpose, we consider omega-PDAs of five standard acceptance types: Buchi, Parity, Rabin, Streett and Muller acceptances. Based on the transformation for omega-automata and the efficient algorithm proposed by Esparza et al. in CAV' 00 for verifying the emptiness problem of omega-PDAs with Buchi acceptance, it is trivial to check the emptiness problem of other omega-PDAs. However, this naive approach is not optimal. In this paper, we propose novel algorithms for the emptiness problem of omega-PDAs based on the observations of the structure of accepting runs. Our algorithms outperform algorithms that go through Buchi PDAs. In particular, the space complexity of the algorithm for Streett acceptance that goes through Buchi acceptance is exponential, while ours is polynomial. The algorithm for Parity acceptance that goes through Buchi acceptance is in O(k(3)n(2)m) time and O(k(2)nm) space, while ours is in O(kn(2)m) time and O(nm) space, where n (resp. m and k) is the number of control states (resp. transitions and index). Finally, we show that our algorithms yield a better solution for the pushdown model checking problem against linear temporal logic with fairness.