Probabilistic temporal logics for finite and bounded models

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 and by Clarke and Emerson. 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 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.

REFERENCES

• 1: M. Ben-Ari, A. Pnueli and Z. Manna, The Temporal Logic of Branching Time, Tech. Rept., Dept. of Applied Math., Weizmann Institute of Science, 1982.
• 2: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 3: Yishai A. Feldman , David Harel, A probabilistic dynamic logic, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.181-195, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802191]
• 4: Yishai A. Feidman, A decidable propositional probabilistic dynamic logic, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.298-309, December 1983 [doi>10.1145/800061.808759]
• 5: Sergiu Hart , Micha Sharir , Amir Pnueli, Termination of Probabilistic Concurrent Program, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.356-380, July 1983 [doi>10.1145/2166.357214]
• 6: S. Hart and M. Sharir, Concurrent Probabilistic Programs, or: How to Schedule if You Must, Tech. Rept., School of Math. Sciences, Tel Aviv University, May 1982.
• 7: Dexter Kozen, A probabilistic PDL, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.291-297, December 1983 [doi>10.1145/800061.808758]
• 8: S. Krauss and D. Lehmann, Decision Procedures for Time and Chance, Proc. 24th Symp. Foundations of Computer Science 1983, pp. 202-209.
• 9: D. Lehmann and S. Shelah, Reasoning with Time and Chance, Information and Control 53(1983) pp. 165-198.
• 10: Amir Pnueli, On the extremely fair treatment of probabilistic algorithms, Proceedings of the fifteenth annual ACM symposium on Theory of computing, p.278-290, December 1983 [doi>10.1145/800061.808757]
• 11: Micha Sharir , Amir Pnueli , Sergiu Harts, Verification of probabilistic programs, SIAM Journal on Computing, v.13 n.2, p.292-314, May 1984 [doi>10.1137/0213021]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Probabilistic computation

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded); Bounded-action devices (e.g., Turing machines, random access machines)

General Terms:
Algorithms, Theory