logo

SCIENCE CHINA Information Sciences, Volume 60, Issue 11: 112102(2017) https://doi.org/10.1007/s11432-016-9026-x

On the complexity of $\omega$-pushdown automata

More info
  • ReceivedNov 3, 2016
  • AcceptedJan 29, 2017
  • PublishedJul 12, 2017

Abstract

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 hasreceived considerable research attention. Pushdown automata over infinite words (called $\omega$-PDAs), a generalization of $\omega$-automata, are a naturalmodel of recursive programs. Our goal in this paper is to conduct a relatively complete investigation on the complexity of the emptiness problems for variantsof $\omega$-PDAs. For this purpose, we consider $\omega$-PDAs of five standard acceptance types: Büchi, 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$-PDAswith Büchi 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 algorithmsthat go through Büchi PDAs. In particular, the space complexity of the algorithm for Streett acceptance that goes through Büchi acceptance is exponential,while ours is polynomial. The algorithm for Parity acceptance that goes through Büchi acceptance is in ${\boldsymbol O}(k^3n^2m)$ time and ${\boldsymbol O}(k^2nm)$ space,while ours is in ${\boldsymbol O}(kn^2m)$ time and ${\boldsymbol 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.


Acknowledgment

This work was partially supported by National Natural Science Foundation of China (Grant Nos. 61402179, 61532019, 61103012), ChenGuang Project of the Shanghai Municipal Education Commission (SHMEC) and Shanghai Education Development Foundation (SHEDF) (Grant No. 13CG21), and Open Project of Shanghai Key Laboratory of Trustworthy Computing (Grant No. 07dz22304201404).


References

[1] Büchi J R. On a decision method in restricted second order arithmetic. In: The Collected Works of J. Richard Büchi. New York: Springer-Verlag, 1990. 425--435. Google Scholar

[2] Muller D E. Infinite sequences and finite machines. In: Proceedings of the 4th Annual Symposium on Switching Circuit Theory and Logical Design. New York: IEEE, 1963. 3--16. Google Scholar

[3] McNaughton R. Testing and generating infinite sequences by a finite automaton. Inf Control, 1966, 9: 521-530 CrossRef Google Scholar

[4] Rabin M O. Decidability of second-order theories and automata on infinite trees. Trans Amer Math Soc, 1969, 141: 1--35. Google Scholar

[5] Streett R S. Propositional dynamic logic of looping and converse is elementarily decidable. Inf Control, 1982, 54: 121-141 CrossRef Google Scholar

[6] Mostowski A W. Regular expressions for infinite trees and a standard form of automata. In: Proceedings of the 5th Symposium on Computation Theory. Berlin: Springer-Verlag, 1984. 157--168. Google Scholar

[7] Emerson E A, Lei C. Modalities for model checking: branching time strikes back. In: Proceedings of the 12th ACM Symposium on Principles of Programming Languages. New York: ACM 1985. 84--96. Google Scholar

[8] Thomas W. Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B. Cambridge: MIT Press, 1990. 133--192. Google Scholar

[9] Vardi M Y. Verification of concurrent programs: the automata-theoretic framework*. Ann Pure Appl Logic, 1991, 51: 79-98 CrossRef Google Scholar

[10] Vardi M Y, Wolper P. Automata-theoretic techniques for modal logics of programs. J Comp Syst Sci, 1986, 32: 183-221 CrossRef Google Scholar

[11] Pnueli A. The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science. New York: IEEE, 1977. 46--57. Google Scholar

[12] Löding C. Methods for the transformation of $\omega$-automata: complexity and connection to second order logic. Dissertation for Ph.D. Degree. Kiel: Christian-Albrechts-University of Kiel, 1998. Google Scholar

[13] Löding C. Optimal bounds for transformations of omega-automata. In: Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science. Berlin: Springer-Verlag, 1999. 97--109. Google Scholar

[14] Piterman N. From nondeterministic Büchi and Streett automata to deterministic parity automata. Log Meth Comput Sci, 2007, 3: 1--21. Google Scholar

[15] Bloem R, Gabow H N, Somenzi F. An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps. Form Method Syst Des, 2006, 28: 37-56 CrossRef Google Scholar

[16] Henzinger M R, Telle J A. Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. In: Proceedings of the 5th Scandinavian Workshop on Algorithm Theory. Berlin: Springer-Verlag, 1996. łinebreak 16--27. Google Scholar

[17] King V, Kupferman O, Vardi M Y. On the complexity of parity word automata. In: Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures. Berlin: Springer-Verlag, 2001. 276--286. Google Scholar

[18] Cohen R S, Gold A Y. Theory of ω-languagesI: Characterizations of ω-context-free languages. J Comp Syst Sci, 1977, 15: 169-184 CrossRef Google Scholar

[19] Cohen R S, Gold A Y. Theory of ω-languages. II: A study of various models of ω-type generation and recognition. J Comp Syst Sci, 1977, 15: 185-208 CrossRef Google Scholar

[20] Cohen R S, Gold A Y. ω-Computations on deterministic pushdown machines. J Comp Syst Sci, 1978, 16: 275-300 CrossRef Google Scholar

[21] Linna M. On ω-sets associated with context-free languages. Inf Control, 1976, 31: 272-293 CrossRef Google Scholar

[22] Linna M. A decidability result for deterministic ω context-free languages. Theor Comp Sci, 1977, 4: 83-98 CrossRef Google Scholar

[23] Bouajjani A, Esparza J, Maler O. Reachability analysis of pushdown automata: application to model checking. In: Proceedings of the 8th International Conference on Concurrency Theory. Berlin: Springer-Verlag, 1997. 135--150. Google Scholar

[24] Esparza J, Hansel D, Rossmanith P, et al. Efficient algorithm for model checking pushdown systems. In: Proceedings of the 12th International Conference Computer Aided Verification. Berlin: Springer-Verlag, 2000. 232--247. Google Scholar

[25] Esparza J, Schwoon S. A BDD-based model checker for recursive programs. In: Proceedings of the 13th International Conference Computer Aided Verification. Berlin: Springer-Verlag, 2001. 324--336. Google Scholar

[26] Finkel A, Willems B, Wolper P. A Direct Symbolic Approach to Model Checking Pushdown Systems (extended abstract). Electron Notes Theor Comp Sci, 1997, 9: 27-37 CrossRef Google Scholar

[27] Walukiewicz I. Pushdown processes: games and model checking. Inf Comput, 1996, 164: 62--74. Google Scholar

[28] Hague M, Ong C L. Winning regions of pushdown parity games: a saturation method. In: Proceedings of the 20th International Conference on Concurrency Theory. Berlin: Springer-Verlag, 2009. 384--398. Google Scholar

[29] Hague M, Ong C H L. A saturation method for the modal μ-calculus over pushdown systems. Inf Computation, 2011, 209: 799-821 CrossRef Google Scholar

[30] Kupferman O, Piterman N, Vardi M Y. Pushdown specifications. In: Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Berlin: Springer-Verlag, 2002. 262--277. Google Scholar

[31] Song F, Touili T. Efficient CTL model-checking for pushdown systems. In: Proceedings of the 8th International Conference on Concurrency Theory. Berlin: Springer-Verlag, 2011. 434--449. Google Scholar

[32] Song F, Touili T. Efficient CTL model-checking for pushdown systems. Theor Comp Sci, 2014, 549: 127-145 CrossRef Google Scholar

[33] Song F, Touili T. PoMuC: a CTL model-checker for sequential programs. In: Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering. New York: ACM 2012. 346--349. Google Scholar

[34] Reps T. Program analysis via graph reachability. Inf Software Tech, 1998, 40: 701-726 CrossRef Google Scholar

[35] Baier C, Katoen J. Principles of Model Checking. London: MIT Press, 2008. Google Scholar

[36] Esparza J, Ku?era A, Schwoon S. Model checking LTL with regular valuations for pushdown systems. Inf Computation, 2003, 186: 355-376 CrossRef Google Scholar

[37] Bozzelli L. Complexity results on branching-time pushdown model checking. Theor Comp Sci, 2007, 379: 286-297 CrossRef Google Scholar

[38] Cachat T. Symbolic strategy synthesis for games on pushdown graphs. In: Proceedings of the 29th International Colloquium on Automata, Languages and Programming. Berlin: Springer-Verlag, 2002. 704--715. Google Scholar

[39] Serre O. Note on winning positions on pushdown games with ω-regular conditions. Inf Processing Lett, 2003, 85: 285-291 CrossRef Google Scholar

Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1