Document Open Access Logo

On the Way to Alternating Weak Automata

Authors Udi Boker, Karoliina Lehtinen

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.21.pdf
  • Filesize: 0.52 MB
  • 22 pages

Document Identifiers

Author Details

Udi Boker
  • IDC Herzliya, Israel
Karoliina Lehtinen
  • Kiel University, Kiel, Germany

Funding

  • Boker, Udi: Research supported by the Israel Science Foundation grant 1373/16.
  • Lehtinen, Karoliina: Research supported by BMBF project no. 01IS160253 "ARAMiS II".

Cite As Get BibTex

Udi Boker and Karoliina Lehtinen. On the Way to Alternating Weak Automata. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2018.21

Abstract

Different types of automata over words and trees offer different trade-offs between expressivity, conciseness, and the complexity of decision procedures. Alternating weak automata enjoy simple algorithms for emptiness and membership checks, which makes transformations into automata of this type particularly interesting. For instance, an algorithm for solving two-player infinite games can be viewed as a special case of such a transformation. However, our understanding of the worst-case size blow-up that these transformations can incur is rather poor. This paper establishes two new results, one on word automata and one on tree automata. We show that: 
- Alternating parity word automata can be turned into alternating weak automata of quasi-polynomial (rather than exponential) size. 
- Universal co-Büchi tree automata, a special case of alternating parity tree automata, can be exponentially more concise than alternating weak automata. 
 Along the way, we present a family of game languages, strict for the levels of the weak hierarchy of tree automata, which corresponds to a weak version of the canonical game languages known to be strict for the Mostowski - Rabin index hierarchy.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Alternating automata
  • Parity games
  • Parity automata
  • Weak automata

Metrics

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

References

  1. U. Boker and O. Kupferman. Translating to Co-Büchi Made Tight, Unified, and Useful. ACM Trans. Comput. Log., 13(4):29:1-29:26, 2012. Google Scholar
  2. U. Boker and Y. Shaulian. Automaton-Based Criteria for Membership in CTL. In Proceedings of LICS, pages 155-164, 2018. Google Scholar
  3. J. Bradfield. Simplifying the modal mu-calculus alternation hierarchy. In Annual Symposium on Theoretical Aspects of Computer Science, pages 39-49. Springer, 1998. Google Scholar
  4. J.C. Bradfield. The modal mu-calculus alternation hierarchy is strict. Theoretical Computer Science, 195(2):133-153, 1998. Google Scholar
  5. C. S. Calude, S. Jain, B. Khoussainov, L. Bakhadyr, W. Li, and F. Stephan. Deciding Parity Games in Quasipolynomial Time. In Proceedings of STOC, pages 252-263. ACM, 2017. Google Scholar
  6. T. Colcombet, D. Kuperberg, C. Löding, and M. Vanden Boom. Deciding the weak definability of Büchi definable tree languages. In LIPIcs-Leibniz International Proceedings in Informatics, volume 23. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2013. Google Scholar
  7. E.A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy. In Proceeding of FoCS, pages 368-377. IEEE, 1991. Google Scholar
  8. M. Jurdzinski and R. Lazic. Succinct progress measures for solving parity games. In Proceedings of (LICS), pages 1-9, 2017. Google Scholar
  9. R. Kaivola. Axiomatising linear time mu-calculus. In International Conference on Concurrency Theory, pages 423-437. Springer, 1995. Google Scholar
  10. D. Kirsten. Alternating Tree Automata and Parity Games, pages 153-167. Springer Berlin Heidelberg, 2002. Google Scholar
  11. O. Kupferman and M. Y. Vardi. Π₂ ⋂ Σ₂ ≡ AFMC. In Proceedings of ICALP, pages 697-713. Springer, 2003. Google Scholar
  12. O. Kupferman and M.Y. Vardi. Weak alternating automata and tree automata emptiness. In Proceedings of STOC, pages 224-233, 1998. Google Scholar
  13. O. Kupferman and M.Y. Vardi. Weak alternating automata are not that weak. ACM Transactions on Computational Logic, 2(2):408-429, 2001. Google Scholar
  14. K. Lehtinen. A modal μ perspective on solving parity games in quasipolynomial time. In Proceedings of LICS, 2018. Google Scholar
  15. K. Lehtinen and S. Quickert. Σ^μ₂ is decidable for Π^μ₂. In Conference on Computability in Europe, pages 292-303. Springer, 2017. Google Scholar
  16. P. A. Lindsay. On Alternating omega-Automata. J. Comput. Syst. Sci., 36(1):16-24, 1988. Google Scholar
  17. R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and control, 9(5):521-530, 1966. Google Scholar
  18. M. Michel. Complementation is more difficult with automata on infinite words. CNET, Paris, 1988. Google Scholar
  19. A.W. Mostowski. Hierarchies of weak automata and weak monadic formulas. Theoretical Computer Science, 83(2):323-335, 1991. Google Scholar
  20. D.E. Muller and P.E. Schupp. Simulating Alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141:69-107, 1995. Google Scholar
  21. D. Niwiński and I. Walukiewicz. A gap property of deterministic tree languages. Theoretical Computer Science, 303(1):215-231, 2003. Google Scholar
  22. M. Skrzypczak and I. Walukiewicz. Deciding the topological complexity of Büchi languages. In LIPIcs-Leibniz International Proceedings in Informatics, volume 55. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  23. A. Di Stasio, A. Murano, G. Perelli, and M. Y. Vardi. Solving parity games using an automata-based algorithm. In International Conference on Implementation and Application of Automata, pages 64-76. Springer, 2016. Google Scholar
  24. T. Wilke. CTL^+ is exponentially more succinct than CTL. In Proc. of FoSSaCS, volume 1738 of LNCS, pages 110-121. Springer, 1999. 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact