Probabilistic Propositional Temporal Logics

Sergiu Hart and Micha Sharir


   
(Acrobat PDF files)


Abstract

We present two (closely-related) propositional probabilistic temporal logics based on temporal logics of branching time 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 actual 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.

Related papers on probabilistic programs by S. Hart, A. Pnueli and M. Sharir: