Decidability of finite probabilistic propositional dynamic logics

This paper deals with various versions of finite propositional probabilistic dynamic logic. We present probabilistic propositional dynamic logic with simple probabilistic estimations and “almost regular” program language. Besides the logics previously introduced in the literature we present some natural variations and extensions of these logics. We investigate the (un)decidability of these logics and give a complete picture of decidability and undecidability. Some of these logics have the finite model property, and therefore, if they are undecidable, they are exactly Π 1 0. We show that allowing nesting and probabilistic choice often leads to undecidability.

Authors

• M. Tiomkin
• J.A. Makowsky

Keywords

No keywords are indexed for this paper.