Document Open Access Logo

Emptiness of Zero Automata Is Decidable

Authors Mikolaj Bojanczyk, Hugo Gimbert, Edon Kelmendi

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2017.106.pdf
  • Filesize: 0.54 MB
  • 13 pages

Document Identifiers

Subject Classification

Keywords
  • tree automata
  • probabilistic automata
  • monadic second-order logic

Metrics

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

Abstract

Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of MSO, called TMSO+zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero automata called nonzero automata. We prove that for every zero automaton there is an equivalent nonzero automaton of quadratic size
and the emptiness problem of nonzero automata is decidable, with complexity co-NP. These results imply that TMSO+zero has decidable satisfiability.

Cite As Get BibTex

Mikolaj Bojanczyk, Hugo Gimbert, and Edon Kelmendi. Emptiness of Zero Automata Is Decidable. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 106:1-106:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ICALP.2017.106

Author Details

Mikolaj Bojanczyk
Hugo Gimbert
Edon Kelmendi

References

  1. Mikolaj Bojanczyk. Thin MSO with a Probabilistic Path Quantifier. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 96:1-96:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.96.
  2. Mikołaj Bojańczyk, Hugo Gimbert, and Edon Kelmendi. Emptiness of zero automata is decidable. Technical report, CNRS, 2017. URL: http://arxiv.org/abs/1702.06858.
  3. Tomás Brázdil, Vojtech Forejt, and Antonín Kucera. Controller synthesis and verification for mdps with qualitative branching time objectives. In ICALP 2008., pages 148-159, 2008. Google Scholar
  4. C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. Technical report, CDMTCS, October 2016. URL: https://www.cs.auckland.ac.nz/research/groups/CDMTCS/researchreports/index.php?download&paper_file=631.
  5. Arnaud Carayol, Axel Haddad, and Olivier Serre. Randomization in automata on infinite trees. ACM Trans. Comput. Log., 15(3):24:1-24:33, 2014. URL: http://dx.doi.org/10.1145/2629336.
  6. L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, december 1997. Google Scholar
  7. A. S. Kechris. Classical Descriptive Set Theory. Graduate Texts in Mathematics. Springer-Verlag, 1995. Google Scholar
  8. Daniel Lehmann and Saharon Shelah. Reasoning with time and chance. Information and Control, 53(3):165-1983, 1982. Google Scholar
  9. Henryk Michalewski and Matteo Mio. Measure quantifier in monadic second order logic. In LFCS 2016, Deerfield Beach, FL, USA, January 4-7, 2016. Proceedings, pages 267-282, 2016. URL: http://dx.doi.org/10.1007/978-3-319-27683-0_19.
  10. Henryk Michalewski, Matteo Mio, and Mikołaj Bojańczyk. On the regular emptiness problem of subzero automata. CoRR, abs/1608.03319, 2016. URL: http://arxiv.org/abs/1608.03319.
  11. Larry J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, MIT, 1974. Google Scholar
  12. Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(98)00009-7.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact