Probabilistic Logic over Paths

We introduce a probabilistic modal logic PPL extending the work of [Ronald Fagin, Joseph Y. Halpern, and Nimrod Megiddo. A logic for reasoning about probabilities. Information and Computation, 87(1,2):78–128, 1990; Ronald Fagin and Joseph Y. Halpern. Reasoning about knowledge and probability. Journal of the ACM, 41(2):340–367, 1994] by allowing arbitrary nesting of a path probabilistic operator and we prove its completeness. We prove that our logic is strictly more expressive than other logics such as the logics cited above. By considering a probabilistic extension of CTL we show that this additional expressive power is really needed in some applications.