This work addresses the problem of computing measures of recognisable sets of infinite trees. An algorithm is provided to compute the probability measure of a tree language recognisable by a weak alternating automaton, or equivalently definable in weak monadic second-order logic. The measure is the uniform coin-flipping measure or more generally it is generated by a branching stochastic process. The class of tree languages in consideration, although smaller than all regular tree languages, comprises in particular the languages definable in the alternation-free μ-calculus or in temporal logic CTL. Thus, the new algorithm may enhance the toolbox of probabilistic model checking.
@InProceedings{niwinski_et_al:LIPIcs.ICALP.2020.136, author = {Niwi\'{n}ski, Damian and Przyby{\l}ko, Marcin and Skrzypczak, Micha{\l}}, title = {{Computing Measures of Weak-MSO Definable Sets of Trees}}, booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)}, pages = {136:1--136:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-138-2}, ISSN = {1868-8969}, year = {2020}, volume = {168}, editor = {Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.136}, URN = {urn:nbn:de:0030-drops-125430}, doi = {10.4230/LIPIcs.ICALP.2020.136}, annote = {Keywords: infinite trees, weak alternating automata, coin-flipping measure} }
Feedback for Dagstuhl Publishing