Advertisement

Reasoning with time and chance

Extended abstract
  • Daniel Lehmann
  • Saharon Shelah
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BMP]
    Ben-Ari, M., Manna, Z. and Pnueli, A. The temporal logic of branching time, Conf. Record 8th Annual ACM Symposium on Principles of Programming Languages, Williamsburg, Va. (Jan. 1981), pp. 164–176.Google Scholar
  2. [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
  3. [Ch]
    Chellas, B. F. Modal logic, an introduction, Cambridge University Press, Cambridge (1980).Google Scholar
  4. [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
  5. [EH]
    Emerson, E. A. and Halpern, J. Y. Decision procedures and expressiveness in the temporal logic of branching time, Conf. Record 14th Annual ACM Symposium on Theory of Computing, San Francisco, CA (May 1982), pp. 169–179.Google Scholar
  6. [FH]
    Feldman, Y. A. and Harel, D. A probabilistic dynamic logic, Conf. Record 14th 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
  7. [GPSS]
    Gabbay, D., Pnueli, A., Shelah, S, and Stavi, J. On the temporal analysis of fairness, Conf. Record of 7th Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada (Jan. 1980), pp. 163–173.Google Scholar
  8. [HC]
    Hughes, G. E. and Cresswell, M. J., An introduction to modal logic, Methuen, London (1972).Google Scholar
  9. [HR]
    Halpern, J. Y. and Rabin, M. O., A logic to reason about likelihood, Proc. 15th Annual ACM Symposium on Theory of Computing (April 1983).Google Scholar
  10. [HSP]
    Hart, S., Sharir, M. and Pnueli, A. Termination of probabilistic concurrent programs, Conf. Record 9th Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico (1982), pp. 1–6.Google Scholar
  11. [Ko]
    Kozen, D. Semantics of probabilistic programs, J. of Computer and System Sciences Vol. 22 (1981), pp. 328–350.Google Scholar
  12. [KSK]
    Kemeny, J.G., Snell, J.L. and Knapp, A.W., Denumerable Markov chains, Van Nostrand, Princeton, NJ (1966).Google Scholar
  13. [La]
    Lamport, L. “Sometimes” is sometimes “not never”, Conf. Record of 7th Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada (Jan. 1980), pp. 174–183.Google Scholar
  14. [Le]
    Lehmann, D. On primality tests, SIAM Journal on Computing Vol. 11 (1982), pp. 374–375.Google Scholar
  15. [LPS]
    Lehmann, D., Pnueli, A. and Stavi, J. Impartiality, Justice and Fairness: the ethics of concurrent termination, Proceedings of 8th International Colloquium on Automata, Languages and Programming, July 1981, Acco, Israel, pp. 264–277.Google Scholar
  16. [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 8th Annual ACM Symposium on Principles of Programming Languages, Williamsburg, Va. (Jan. 198), pp. 133–138.Google Scholar
  17. [MT]
    Makowski, J.A. and Tiomkin, M. A probabilistic propositional dynamic logic (Extended Abstract), manuscript 1982.Google Scholar
  18. [Pn]
    Pnueli, A. The temporal semantics of concurrent programs, Theoretical Computer Science Vol. 13 (1981), pp. 45–60.Google Scholar
  19. [Ra1]
    Rabin, M. O. Decidability of second order theories and automata on infinite trees, Trans. AMS Vol. 141 (1969), pp. 1–35.Google Scholar
  20. [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
  21. [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
  22. [Ra4]
    Rabin, M.O. The choice coordination problem, Acta Informatica Vol. 17 (1982), pp. 121–134.Google Scholar
  23. [Re]
    Reif, J. H. Logics for probabilistic programming, Proc. 12th ACM Symposium on Theory of Computing, Los Angeles, CA (April 1980), pp. 8–13.Google Scholar
  24. [SC]
    Sisla, A. P. and Clarke, E. M. The complexity of propositional linear temporal logics, Proc. 14th Annual ACM Symposium on Theory of Computing, San Francisco, CA (May 1982), pp. 159–168.Google Scholar
  25. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Daniel Lehmann
    • 1
  • Saharon Shelah
    • 1
  1. 1.Institute of Mathematics and Computer ScienceHebrew UniversityJerusalemIsrael

Personalised recommendations