Computing Measures of Weak-MSO Definable Sets of Trees

Authors Damian Niwiński, Marcin Przybyłko, Michał Skrzypczak

Thumbnail PDF


  • Filesize: 0.54 MB
  • 18 pages

Document Identifiers

Author Details

Damian Niwiński
  • Institute of Informatics, University of Warsaw, Poland
Marcin Przybyłko
  • Fachbereich Informatik, University of Bremen, Germany
Michał Skrzypczak
  • Institute of Informatics, University of Warsaw, Poland

Cite AsGet BibTex

Damian Niwiński, Marcin Przybyłko, and Michał Skrzypczak. Computing Measures of Weak-MSO Definable Sets of Trees. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 136:1-136:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Mathematics of computing → Markov processes
  • infinite trees
  • weak alternating automata
  • coin-flipping measure


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. André Arnold and Damian Niwiński. Fixed point characterisation of weak monadic logic definable sets of trees. In Tree Automata and Languages, pages 159-188, 1992. Google Scholar
  2. Saugata Basu, Richard Pollack, and Marie-Françoise Roy. Algorithms in Real Algebraic Geometry, volume 10 of Algorithms and Computation in Mathematics. Springer-Verlag Berlin Heidelberg, 2006. Google Scholar
  3. Michael Ben-Or, Dexter Kozen, and John Reif. The complexity of elementary algebra and geometry. Journal of Computer and System Sciences, 32(2):251-264, 1986. Google Scholar
  4. Jacek Bochnak, Michel Coste, and Marie-Françoise Roy. Real Algebraic Geometry, volume 36 of A Series of Modern Surveys in Mathematics. Springer-Verlag Berlin Heidelberg, 1998. Google Scholar
  5. Krishnendu Chatterjee, Marcin Jurdzinski, and Thomas A. Henzinger. Quantitative stochastic parity games. In SODA, pages 121-130, 2004. Google Scholar
  6. Taolue Chen, Klaus Dräger, and Stefan Kiefer. Model checking stochastic branching processes. In MFCS, pages 271-282, 2012. Google Scholar
  7. George E. Collins. Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Automata Theory and Formal Languages, pages 134-183, 1975. Google Scholar
  8. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. J. ACM, 42(4):857-907, 1995. Google Scholar
  9. Stéphane Demri, Valentin Goranko, and Martin Lange. Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. Google Scholar
  10. Alessandro Facchini, Filip Murlak, and Michał Skrzypczak. Rabin-Mostowski index problem: A step beyond deterministic automata. In LICS, pages 499-508, 2013. Google Scholar
  11. Gaëlle Fontaine. Continuous fragment of the mu-calculus. In CSL, pages 139-153, 2008. Google Scholar
  12. Tomasz Gogacz, Henryk Michalewski, Matteo Mio, and Michał Skrzypczak. Measure properties of regular sets of trees. Information and Computation, 256:108-130, 2017. Google Scholar
  13. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  14. Claire Jones and Gordon D. Plotkin. A probabilistic powerdomain of evaluations. In LICS, pages 186-195, 1989. Google Scholar
  15. Henryk Michalewski and Matteo Mio. On the problem of computing the probability of regular sets of trees. In FSTTCS, pages 489-502, 2015. Google Scholar
  16. Matteo Mio. On the equivalence of game and denotational semantics for the probabilistic mu-calculus. Logical Methods in Computer Science, 8(2), 2012. Google Scholar
  17. David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Alternating automata. the weak monadic theory of the tree, and its complexity. In ICALP, volume 226 of Lecture Notes in Computer Science, pages 275-283, 1986. Google Scholar
  18. Damian Niwiński and Igor Walukiewicz. A gap property of deterministic tree languages. Theoretical Computer Science, 1(303):215-231, 2003. Google Scholar
  19. Dominique Perrin and Jean-Éric Pin. Infinite Words: Automata, Semigroups, Logic and Games. Elsevier, 2004. Google Scholar
  20. Marcin Przybyłko. On computing the measures of first-order definable sets of trees. In GandALF, pages 206-219, 2018. Google Scholar
  21. Marcin Przybyłko and Michał Skrzypczak. The uniform measure of simple regular sets of infinite trees. CoRR, abs/2001.11576, 2020. URL:
  22. Nasser Saheb-Djahromi. Cpo’s of measures for nondeterminism. Theor. Comput. Sci., 12:19-37, 1980. Google Scholar
  23. Jerzy Skurczyński. The Borel hierarchy is infinite in the class of regular sets of trees. Theoretical Computer Science, 112(2):413-418, 1993. Google Scholar
  24. Ludwig Staiger. The Hausdorff measure of regular omega-languages is computable. Bulletin of the EATCS, 66:178-182, 1998. Google Scholar
  25. Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, 1951. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail