On the complexity of ω-pushdown automata  

作　　者：Yusi LEI Fu SONG Wanwei LIU Min ZHANG 

机构地区：[1]Shanghai Key Laboratory of Trustworthy Computing, East China Normal University [2]School of Information Science and Technology, Shanghai Tech University [3]School of Computer Science, National University of Defense Technology

出　　处：《Science China(Information Sciences)》2017年第11期152-166,共15页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 61402179, 61532019, 61103012);Chen Guang Project of the Shanghai Municipal Education Commission (SHMEC) and Shanghai Education Development Foundation (SHEDF) (Grant No. 13CG21);Open Project of Shanghai Key Laboratory of Trustworthy Computing (Grant No. 07dz22304201404).

摘　　要：Finite automata over infinite words （called w-automata） play an important role in the automata- theoretic approach to system verification. Different types of w-automata differ in their succinctness and complexity of their emptiness problems, as a result, theory of w-automata has received considerable research attention. Pushdown automata over infinite words （called w-PDAs）, a generalization of w-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 w-PDAs. For this purpose, we consider w-PDAs of five standard acceptance types： Buchi, Parity, Rabin, Streett and Muller acceptances. Based on the transformation for w-automata and the efficient algorithm proposed by Esparza et al. in CAV＇00 for verifying the emptiness problem of w-PDAs with Biiehi acceptance, it is trivial to check the emptiness problem of other w-PDAs. However, this naive approach is not optimal. In this paper, we propose novel algorithms for the emptiness problem of w-PDAs based on the observations of the structure of accepting runs. Our algorithms outperform algorithms that go through uchi PDAs. In particular, the space complexity of the algorithm for Streett acceptance that goes through Bfichi acceptance is exponential, while ours is polynomial. The algorithm for Parity acceptance that goes through Buchi acceptance is in O（k3n2m） time and O（k2nm） space, while ours is in O（kn2m） 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.Finite automata over infinite words （called w-automata） play an important role in the automata- theoretic approach to system verification. Different types of w-automata differ in their succinctness and complexity of their emptiness problems, as a result, theory of w-automata has received considerable research attention. Pushdown automata over infinite words （called w-PDAs）, a generalization of w-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 w-PDAs. For this purpose, we consider w-PDAs of five standard acceptance types： Buchi, Parity, Rabin, Streett and Muller acceptances. Based on the transformation for w-automata and the efficient algorithm proposed by Esparza et al. in CAV＇00 for verifying the emptiness problem of w-PDAs with Biiehi acceptance, it is trivial to check the emptiness problem of other w-PDAs. However, this naive approach is not optimal. In this paper, we propose novel algorithms for the emptiness problem of w-PDAs based on the observations of the structure of accepting runs. Our algorithms outperform algorithms that go through uchi PDAs. In particular, the space complexity of the algorithm for Streett acceptance that goes through Bfichi acceptance is exponential, while ours is polynomial. The algorithm for Parity acceptance that goes through Buchi acceptance is in O（k3n2m） time and O（k2nm） space, while ours is in O（kn2m） 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.

关 键 词：pushdown automata EMPTINESS w-words model checking linear temporal logic 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]