Mikołaj Bojańczyk

MSO with probability

April 3, 2019
  1. Mikołaj Bojańczyk
    Thin MSO with a Probabilistic Path Quantifier. ICALP, 2016   PDF

  2. Mikołaj Bojańczyk, Hugo Gimbert, Edon Kelmendi
    Emptiness of Zero Automata Is Decidable. ICALP, 2017   PDF

  3. Mikołaj Bojańczyk, Edon Kelmendi, Michal Skrzypczak
    MSO+∇ is undecidable. LICS, 2019   PDF

Consider a probabilistic extension of MSO over infinite binary trees, which allows formulas saying “almost surely a branch \pi \in \set{0,1}^\omega satisfies \varphi(\pi)”. This logic was introduced by Mio and Michalewski, and it generalises known (qualitative) probabilistic logics such as probabilistic CTL or probabilistic CTL*. Paper [3] shows 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 papers [1] and [2]. Paper [1] shows that the weak fragment of the probabilistic logic (and a bit more) can be compiled into an automaton model, while paper [2] shows that emptiness for the automaton model is decidable.


Leave a Reply

Your email address will not be published.