Document Open Access Logo

Alternating Weak Automata from Universal Trees

Authors Laure Daviaud, Marcin Jurdziński, Karoliina Lehtinen



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.18.pdf
  • Filesize: 444 kB
  • 14 pages

Document Identifiers

Author Details

Laure Daviaud
  • City, University of London, UK
Marcin Jurdziński
  • University of Warwick, UK
Karoliina Lehtinen
  • University of Liverpool, UK

Acknowledgements

We thank Moshe Vardi for encouraging us to bring the state-space blow-up of alternating parity to alternating weak automata translation in line with the state-of-the-art complexity of solving parity games.

Cite AsGet BibTex

Laure Daviaud, Marcin Jurdziński, and Karoliina Lehtinen. Alternating Weak Automata from Universal Trees. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.18

Abstract

An improved translation from alternating parity automata on infinite words to alternating weak automata is given. The blow-up of the number of states is related to the size of the smallest universal ordered trees and hence it is quasi-polynomial, and it is polynomial if the asymptotic number of priorities is at most logarithmic in the number of states. This is an exponential improvement on the translation of Kupferman and Vardi (2001) and a quasi-polynomial improvement on the translation of Boker and Lehtinen (2018). Any slightly better such translation would (if - like all presently known such translations - it is efficiently constructive) lead to algorithms for solving parity games that are asymptotically faster in the worst case than the current state of the art (Calude, Jain, Khoussainov, Li, and Stephan, 2017; Jurdziński and Lazić, 2017; and Fearnley, Jain, Schewe, Stephan, and Wojtczak, 2017), and hence it would yield a significant breakthrough.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Algorithmic game theory
Keywords
  • alternating automata
  • weak automata
  • Büchi automata
  • parity automata
  • parity games
  • universal trees

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. U. Boker and K. Lehtinen. On the way to alternating weak automata. In FSTTCS 2018, volume 122 of LIPIcs, pages 21:1-21:22. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2018. Google Scholar
  2. C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In STOC 2017, pages 252-263. ACM, 2017. Google Scholar
  3. T. Colcombet and N. Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In FoSSaCS 2019, volume 11425 of LNCS, pages 1-26. Springer, 2019. Google Scholar
  4. T. Colcombet, D. Kuperberg, C. Löding, and M. Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In CSL 2013, volume 23 of LIPIcs, pages 215-230. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2013. Google Scholar
  5. W. Czerwiński, L. Daviaud, N. Fijalkow, M. Jurdziński, R. Lazić, and P. Parys. Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In SODA 2019, pages 2333-2349. ACM/SIAM, 2019. Google Scholar
  6. L. Daviaud, M. Jurdziński, and R. Lazić. A pseudo-quasi polynomial algorithm for solving mean-payoff parity games. In LICS 2018, pages 325-334. IEEE, 2018. Google Scholar
  7. D. Drusinsky and D. Harel. On the power of bounded concurrency I: Finite automata. Journal of the ACM, 41(3):517-539, 1994. Google Scholar
  8. E. A. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In FOCS 1991, pages 368-377. IEEE, 1991. Google Scholar
  9. J. Fearnley, S. Jain, S. Schewe, F. Stephan, and D. Wojtczak. An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In SPIN 2017, pages 112-121, 2017. Google Scholar
  10. M. Jurdziński. Small progress measures for solving parity games. In STACS 2000, volume 1770 of LNCS, pages 290-301. Springer, 2000. Google Scholar
  11. M. Jurdziński and R. Lazić. Succinct progress measures for solving parity games. In LICS 2017, page 9pp. IEEE, 2017. Google Scholar
  12. N. Klarlund. Progress measures for complementation of ω-automata with applications to temporal logic. In FOCS 1991, pages 358-367. IEEE, 1991. Google Scholar
  13. N. Klarlund and D. Kozen. Rabin measures. Chicago J. Theor. Comput. Sci., pages 1-24, 1995. Article 3. Google Scholar
  14. O. Kupferman and M. Y. Vardi. Weak alternating automata and tree automata emptiness. In STOC 1998, pages 224-233. ACM, 1998. Google Scholar
  15. O. Kupferman and M. Y. Vardi. Weak alternating automata are not that weak. ACM Trans. Comput. Log., 2(3):408-429, 2001. Google Scholar
  16. O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312-360, 2000. Google Scholar
  17. K. Lehtinen. A modal μ perspective on solving parity games in quasi-polynomial time. In LICS 2018, pages 639-648. IEEE, 2018. Google Scholar
  18. K. Lehtinen and S. Quickert. Σ^μ₂ is decidable for Π^μ₂. In CiE 2017: Unveiling Dynamics and Complexity, pages 292-303, 2017. Google Scholar
  19. P. Lindsay. On alternating ω-automata. Theoretical Computer Science, 43:107-116, 1988. Google Scholar
  20. M. Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 15, 1988. Google Scholar
  21. D. E. Muller, A. Saoudi, and P. E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In ICALP 1986, volume 226 of LNCS, pages 275-283. Springer, 1986. Google Scholar
  22. M. Skrzypczak and I. Walukiewicz. Deciding the topological complexity of Büchi languages. In ICALP 2016, volume 55 of LIPIcs, pages 99:1-99:13. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2016. Google Scholar
  23. Q. Yan. Lower bounds for complementation of ω-automata via the full automata technique. Logical Methods in Computer Science, 4:1-20, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail