We introduce a new class of automata on infinite trees called alternating nonzero automata, which extends the class of non-deterministic nonzero automata. The emptiness problem for this class is still open, however we identify a subclass, namely limited choice, for which we reduce the emptiness problem for alternating nonzero automata to the same problem for non-deterministic ones, which implies decidability. We obtain, as corollaries, algorithms for the satisfiability of a probabilistic temporal logic extending both CTL* and the qualitative fragment of pCTL*.
@InProceedings{fournier_et_al:LIPIcs.CONCUR.2018.13, author = {Fournier, Paulin and Gimbert, Hugo}, title = {{Alternating Nonzero Automata}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {13:1--13:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.13}, URN = {urn:nbn:de:0030-drops-95517}, doi = {10.4230/LIPIcs.CONCUR.2018.13}, annote = {Keywords: zero-automata, probabilities, temporal logics} }
Feedback for Dagstuhl Publishing