# Reasoning with time and chance

- 2 Citations
- 107 Downloads

## Abstract

The temporal propositional logic of linear time is generalized to an uncertain world, in which random events may occur. The formulas do not mention probabilities explicitly, i.e. the only probability appearing explicitly in formulas is probability one. This logic is claimed to be useful for stating and proving properties of probabilistic programs. It is convenient for proving those properties that do not depend on the specific distribution of probabilities used in the program's random draws. The formulas describe properties of execution sequences. The models are stochastic systems, with state transition probabilities. Three different axiomatic systems are proposed and shown complete for general models, finite models and models with bounded transition probabilities respectively. All three systems are decidable, by the results of Rabin [Ra1].

## Keywords

Temporal Logic Linear Temporal Logic Propositional Variable Execution Sequence Probabilistic Algorithm## Preview

Unable to display preview. Download preview PDF.

## References

- [BMP]Ben-Ari, M., Manna, Z. and Pnueli, A. The temporal logic of branching time, Conf. Record 8
^{th}Annual ACM Symposium on Principles of Programming Languages, Williamsburg, Va. (Jan. 1981), pp. 164–176.Google Scholar - [CE]Clarke, E.M. and Emerson, E.A. Design and synthesis of synchronization skeletons using branching time temporal logic, Proc. Workshop on Logics of Programs, Kozen ed., Springer-Verlag (1982) (to appear).Google Scholar
- [Ch]Chellas, B. F. Modal logic, an introduction, Cambridge University Press, Cambridge (1980).Google Scholar
- [CLP]Cohen, S., Lehmann D. and Pnueli, A. Symmetric and economical solutions to the mutual exclusion problem in a distributed system (in preparation).Google Scholar
- [EH]Emerson, E. A. and Halpern, J. Y. Decision procedures and expressiveness in the temporal logic of branching time, Conf. Record 14
^{th}Annual ACM Symposium on Theory of Computing, San Francisco, CA (May 1982), pp. 169–179.Google Scholar - [FH]Feldman, Y. A. and Harel, D. A probabilistic dynamic logic, Conf. Record 14
^{th}Annual ACM Symposium on Theory of Computing, San Francisco, CA (May 1982), pp. 181–195. (also Tech. Report CS82-07, Dept. of Applied Mathematics, the Weizmann Institute of Science).Google Scholar - [GPSS]Gabbay, D., Pnueli, A., Shelah, S, and Stavi, J. On the temporal analysis of fairness, Conf. Record of 7
^{th}Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada (Jan. 1980), pp. 163–173.Google Scholar - [HC]Hughes, G. E. and Cresswell, M. J., An introduction to modal logic, Methuen, London (1972).Google Scholar
- [HR]Halpern, J. Y. and Rabin, M. O., A logic to reason about likelihood, Proc. 15
^{th}Annual ACM Symposium on Theory of Computing (April 1983).Google Scholar - [HSP]Hart, S., Sharir, M. and Pnueli, A. Termination of probabilistic concurrent programs, Conf. Record 9
^{th}Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico (1982), pp. 1–6.Google Scholar - [Ko]Kozen, D. Semantics of probabilistic programs, J. of Computer and System Sciences Vol. 22 (1981), pp. 328–350.Google Scholar
- [KSK]Kemeny, J.G., Snell, J.L. and Knapp, A.W., Denumerable Markov chains, Van Nostrand, Princeton, NJ (1966).Google Scholar
- [La]Lamport, L. “Sometimes” is sometimes “not never”, Conf. Record of 7
^{th}Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada (Jan. 1980), pp. 174–183.Google Scholar - [Le]Lehmann, D. On primality tests, SIAM Journal on Computing Vol. 11 (1982), pp. 374–375.Google Scholar
- [LPS]Lehmann, D., Pnueli, A. and Stavi, J. Impartiality, Justice and Fairness: the ethics of concurrent termination, Proceedings of 8
^{th}International Colloquium on Automata, Languages and Programming, July 1981, Acco, Israel, pp. 264–277.Google Scholar - [LR]Lehmann, D. and Rabin, M. O. On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem (extended abstract), Conf. Record of 8
^{th}Annual ACM Symposium on Principles of Programming Languages, Williamsburg, Va. (Jan. 198), pp. 133–138.Google Scholar - [MT]Makowski, J.A. and Tiomkin, M. A probabilistic propositional dynamic logic (Extended Abstract), manuscript 1982.Google Scholar
- [Pn]Pnueli, A. The temporal semantics of concurrent programs, Theoretical Computer Science Vol. 13 (1981), pp. 45–60.Google Scholar
- [Ra1]Rabin, M. O. Decidability of second order theories and automata on infinite trees, Trans. AMS Vol. 141 (1969), pp. 1–35.Google Scholar
- [Ra2]Rabin, M.O. Probabilistic algorithms, in Algorithms and Complexity, New Directions and Recent Results, J.F. Traub, ed., Academic Press, New York, 1976.Google Scholar
- [Ra3]Rabin, M.O. N-process mutual exclusion with bounded waiting by 4.log N-valued shared variable, Journal of Computer and System Sciences Vol. 25 (1982) pp. 66–75.Google Scholar
- [Ra4]Rabin, M.O. The choice coordination problem, Acta Informatica Vol. 17 (1982), pp. 121–134.Google Scholar
- [Re]Reif, J. H. Logics for probabilistic programming, Proc. 12
^{th}ACM Symposium on Theory of Computing, Los Angeles, CA (April 1980), pp. 8–13.Google Scholar - [SC]Sisla, A. P. and Clarke, E. M. The complexity of propositional linear temporal logics, Proc. 14
^{th}Annual ACM Symposium on Theory of Computing, San Francisco, CA (May 1982), pp. 159–168.Google Scholar - [SS]Solovay, R. and Strassen V., A fast Monte-Carlo test for primality, SIAM Journal on Computing Vol. 6 (1977), pp. 84–85; erratum Vol. 7 (1978), pp. 118.Google Scholar