eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-06-29
136:1
136:18
10.4230/LIPIcs.ICALP.2020.136
article
Computing Measures of Weak-MSO Definable Sets of Trees
Niwiński, Damian
1
Przybyłko, Marcin
2
Skrzypczak, Michał
1
https://orcid.org/0000-0002-9647-4993
Institute of Informatics, University of Warsaw, Poland
Fachbereich Informatik, University of Bremen, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol168-icalp2020/LIPIcs.ICALP.2020.136/LIPIcs.ICALP.2020.136.pdf
infinite trees
weak alternating automata
coin-flipping measure