@article{Hart198697,
    Abstract = {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.},
    Author = {Hart, Sergiu and Sharir, Micha},
    File = {Probabilistic propositional temporal logics - Hart, Sharir (0) (0) - a - a - f.pdf},
    ISSN = {0019-9958},
    Journal = {Information and Control},
    Number = {2--3},
    Pages = {97 - 155},
    Title = {Probabilistic propositional temporal logics},
    URL = {http://www.sciencedirect.com/science/article/pii/S0019995886800018},
    Volume = {70},
    Year = {1986},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0019995886800018},
    bdsk-url-2 = {http://dx.doi.org/10.1016/S0019-9958(86)80001-8},
    date-added = {2014-07-30 06:27:01 +0000},
    date-modified = {2014-07-30 06:27:01 +0000},
    doi = {10.1016/S0019-9958(86)80001-8}
}

@article{Hart198697, Abstract = {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.}, Author = {Hart, Sergiu and Sharir, Micha}, File = {Probabilistic propositional temporal logics - Hart, Sharir (0) (0) - a - a - f.pdf}, ISSN = {0019-9958}, Journal = {Information and Control}, Number = {2--3}, Pages = {97 - 155}, Title = {Probabilistic propositional temporal logics}, URL = {http://www.sciencedirect.com/science/article/pii/S0019995886800018}, Volume = {70}, Year = {1986}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0019995886800018}, bdsk-url-2 = {http://dx.doi.org/10.1016/S0019-9958(86)80001-8}, date-added = {2014-07-30 06:27:01 +0000}, date-modified = {2014-07-30 06:27:01 +0000}, doi = {10.1016/S0019-9958(86)80001-8} }