【摘要】：Finite automata over infinite words(called ω-automata) play an important role in the automatatheoretic approach to system verification. Different types of ω-automata differ in their succinctness and complexity of their emptiness problems, as a result, theory of ω-automata has received considerable research attention.Pushdown automata over infinite words(called ω-PDAs), a generalization of ω-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 ω-PDAs. For this purpose, we consider ω-PDAs of five standard acceptance types: B¨uchi, Parity, Rabin, Streett and Muller acceptances. Based on the transformation for ω-automata and the efficient algorithm proposed by Esparza et al. in CAV'00 for verifying the emptiness problem of ω-PDAs with B¨uchi acceptance, it is trivial to check the emptiness problem of other ω-PDAs. However, this naive approach is not optimal. In this paper, we propose novel algorithms for the emptiness problem of ω-PDAs based on the observations of the structure of accepting runs. Our algorithms outperform algorithms that go through B¨uchi PDAs. In particular, the space complexity of the algorithm for Streett acceptance that goes through B¨uchi acceptance is exponential, while ours is polynomial. The algorithm for Parity acceptance that goes through B¨uchi 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.
[Abstract]:Finite automata over infinite words (called-automata) play an important role in the automatatheoretic approach to system verification. Different types of_-automata differ in their succinctness and complexity of their emptiness problems, as a result, theory of_-automata has received considerab Pushdown automata over infinite words (called_-PDAs), a generalization of_-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 empty problems for variants of_-PDAs. This purpose, we consider_-PDAs of five standard acceptance types: B_uchi, Parity, Rabin, Streett and Muller acceptances.Based on the transformation for_-automata and the efficient algorithm proposed by Esparza et al.in CAV'00 for verifying the empty problem of_-PDAs with B_uchi acceptances Tance, it is trivial to check the emptiness problem of other_-PDAs. However, this naive approach is not optimal. In this paper, we propose novel algorithms for the emptiness problem of_-PDAs based on the observations of the structure of accepting runs. Our algorithms outperform algorithms that Go through B_uchi PDAs.In particular, the space complexity of the algorithm for Streett acceptance that goes through B_uchi acceptance is exponential, while ours is polynomial.The algorithm for Parity acceptance that goes through B_uchi acceptance is in O (k3n2m) time and O (k2nm) space, while o Urs is in O (kn2m) time and O (n m) 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.
【作者單位】： Shanghai
【基金】：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).
【分類號(hào)】：TP301.1

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 ;Matrix expression and reachability analysis of finite automata[J];Journal of Control Theory and Applications;2012年02期

2 ;Notes on automata theory based on quantum logic[J];Science in China(Series F:Information Sciences);2007年02期

3 ;On behavior of two-dimensional cellular automata with an exceptional rule under periodic boundary condition[J];The Journal of China Universities of Posts and Telecommunications;2010年01期

4 石曉明;施倫;張解放;;Opinion evolution based on cellular automata rules in small world networks[J];Chinese Physics B;2010年03期

5 賈寧;馬壽峰;鐘石泉;;Analytical investigation of the boundary-triggered phase transition dynamics in a cellular automata model with a slow-to-start rule[J];Chinese Physics B;2012年10期

6 ;Loop reduction techniques for reachability analysis of linear hybrid automata[J];Science China(Information Sciences);2012年12期

7 殷澇，

本文編號(hào)：2242903