Emptiness of Zero Automata Is Decidable

Bojanczyk, Mikolaj; Gimbert, Hugo; Kelmendi, Edon

doi:10.4230/LIPIcs.ICALP.2017.106

File

LIPIcs.ICALP.2017.106.pdf

Filesize: 0.54 MB
13 pages

Document Identifiers

DOI: 10.4230/LIPIcs.ICALP.2017.106
URN: urn:nbn:de:0030-drops-74745

Author Details

Mikolaj Bojanczyk

Hugo Gimbert

Edon Kelmendi

Cite AsGet 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

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.

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

References

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.
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.
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.
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.
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.
L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, december 1997.
A. S. Kechris. Classical Descriptive Set Theory. Graduate Texts in Mathematics. Springer-Verlag, 1995.
Daniel Lehmann and Saharon Shelah. Reasoning with time and chance. Information and Control, 53(3):165-1983, 1982.
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.
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.
Larry J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, MIT, 1974.
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.