Mikołaj Bojańczyk

April 3, 2019

Consider a probabilistic extension of MSO over infinite binary trees, which allows formulas saying “almost surely a branch satisfies ”. This logic was introduced by Mio and Michalewski, and it generalises known (qualitative) probabilistic logics such as probabilistic CTL or probabilistic CTL*. In an upcoming LICS 2019 paper, we show that this logic is undecidable. On the other hand, the weak fragment of the logic (where the usual set quantifiers are restricted to range over finite sets) is decidable, which follows from the following two papers:

Mikołaj Bojańczyk

*Thin MSO with a Probabilistic Path Quantifier.*ICALP, 2016 PDFMikołaj Bojańczyk, Hugo Gimbert, Edon Kelmendi

*Emptiness of Zero Automata Is Decidable.*ICALP, 2017 PDF

The first paper shows that the weak fragment of the probabilistic logic (and a bit more) can be compiled into an automaton model, while the second paper shows that emptiness for the automaton model is decidable.

## Leave a Reply