Probabilistic Logic and Regular Expressions on Infinite Words

Thomas Weidner ( Universität Leipzig )

We introduce a probabilistic extension to MSO logic on infinite words. This extended logic adds an expected-value operator to classical MSO. We also provide probabilistic omega-regular expressions, which are based on probabilistic regular expressions introduced by Bollig, Gastin, Monmege, Zeitoun. Both formalisms prove to be expressively equivalent to probabilistic Muller-automata. To obtain better decidability results we restrict probabilistic automata and probabilistic expressions such that probabilistic choices occur almost surely only finitely often. The image of such restricted automata, resp. expressions, can be approximated by a finite, computable set.