LIPIcs.ICALP.2017.106.pdf
- Filesize: 0.54 MB
- 13 pages
Document
Emptiness of Zero Automata Is Decidable
Authors
-
Part of:
Volume:
44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Colloquium on Automata, Languages, and Programming (ICALP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-07-07
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
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.
Subject Classification
Keywords
- tree automata
- probabilistic automata
- monadic second-order logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
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.