Regular Languages of Trees and Probability

April 18, 2016

Matteo Mio (ENS-Lyon)

The decidability of the SAT(isfiability) problem for most branching-time temporal logics (such as CTL) follows from Rabin’s theorem about the decidability of the Monadic Second Order Theory of Two Successors (S2S). However, the decidability of the SAT problem for probabilistic logics (such as probabilistic CTL) is open. In an attempt to solve this problem it is natural to investigate probability-related variants and extensions of Rabin’s theorem. In this talk I will present some recent results on this line of research.