Probabilistic Temporal Logics for Finite and Bounded Models

We present two (closely-related) propositional probabilistic temporal logics based on temporal logics of branching time as introduced by Ben-Ari, Pnueli and Manna and by Clarke and Emerson. The first logic, PTL f , is interpreted over finite models, while the second logic, PTL b , which is an extension of the first one, is interpreted over infinite models with transition probabilities bounded away from 0. The logic PTL f allows us to reason about finite-state sequential probabilistic programs, and the logic PTL b 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 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 PTL b , and the connection between satisfiable formulae of PTL b and finite state concurrent probabilistic programs, are also discussed.

Authors

• Sergiu Hart
• Micha Sharir

Keywords

No keywords are indexed for this paper.