Probabilistic propositional temporal logics

We present two (closely-related) propositional probabilistic temporal logics based on temporal logics of branching time as introduced by Ben-Ari, Pnueli, and Manna (Acta Inform. 20 (1983), 207–226), Emerson and Halpern (“Proceedings, 14th ACM Sympos. Theory of Comput.,” 1982, pp. 169–179, and Emerson and Clarke (Sci. Comput. Program. 2 (1982), 241–266). The first logic, PTLf, is interpreted over finite models, while the second logic, PTLb, which is an extension of the first one, is interpreted over infinite models with transition probabilities bounded away from 0. The logic PTLf allows us to reason about finite-state sequential probabilistic programs, and the logic PTLb allows us to reason about (finite-state) concurrent probabilistic programs, without any explicit reference to the actual values of their state-transition probabilities. A generalization of the tableau method yields deterministic single-exponential time decision procedures for our logics, and complete axiomatizations of them are given. Several meta-results, including the absence of a finite-model property for PTLb, and the connection between satisfiable formulae of PTLb and finite state concurrent probabilistic programs, are also discussed