On the extremely fair treatment of probabilistic algorithms

ABSTRACT

A proof system based on linear temporal logic for the qualitative verification of concurrent probabilistic programs is proposed. The concept of extreme fairness is introduced as an approximation to the notion of probabilistic executions. The proof system proposed is shown to be relatively complete with respect to validity over all extremely fair computations. The proof methodology is demonstrated by proving correctness of a new probabilistic algorithm for solving the mutual exclusion problem ([CLP]).

REFERENCES

• 1: Apt, K.R. and E.R. Olderog. "Proof Rule Dealing with Fairness," TR 8104, Applied Mathematics, University of Kiel, 1981.
• 2: Burns, J.E., M.J. Fischer, P. Jackson, N.A. Lynch, and G.L. Peterson, "Shared Data Requirements for Implementation of Mutual Exclusion Using a Test-and-Set Primitive," Proc. 1978 International Conf. on Parallel Processing, 79-87.
• 3: Cohen, S., D. Lehmann, and A. Pnueli, "Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System," The Hebrew University, Jerusalem (Aug. 1982).
• 4: 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]
• 5: Francez, N. and M. Rodeh, "A Distributed Data Type Implemented by a Probabilistic Communication Scheme," Proc. 21st Symp. on the Foundations of Computer Science, 1980, 373-379.
• 6: Grumberg, O., N. Francez, J.A. Makowsky, and W.P. de Roever, "A Proof Rule for Fair Termination of Guarded Commands," Proc. of the Int. Symp. on Algorithmic Languages, North-Holland, 1981.
• 7: Sergiu Hart , Micha Sharir , Amir Pnueli, Termination of probabilistic concurrent programs: (extended abstract), Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-6, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582154]
• 8: Itai, A. and M. Rodeh, "The Lord of the Ring, or Probabilistic Methods for Breaking Symmetry in Distributve Networks," Tech. Rep. RJ 3110, IBM, San José, 1981.
• 9: Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
• 10: Daniel Lehmann , Michael O. Rabin, On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.133-138, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567547]
• 11: Lehmann, D. and S. Shelah, "Reasoning with Time and Chance," Institute of Mathematics, The Hebrew University, Jerusalem, Israel, Oct. 1982.
• 12: Zohar Manna , Amir Pnueli, Verification of Concurrent Programs: Temporal Proof Principles, Logic of Programs, Workshop, p.200-252, May 01, 1981
• 13: Manna, Z. and A. Pnueli, "Verification of Concurrent Programs: A Temporal Proof System," Proc. 4th School on Advanced Programming, Amsterdam, Holland, June 1982.
• 14: Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567082]
• 15: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 16: Park, D., "A Predicate Transformer for Weak Fair Iteration," Proc. 6 IBM Symp. on Math. Foundation of Computer Science, Hakone, Japan, 1981.
• 17: Rabin, M.O., "Probabilistic Algorithms," in Algorithms and Complexity, New Directions and Recent Results, (J.F. Traub, ed.), Academic Press, New York, 1976.
• 18: Rabin, M.O., "N Process Synchronization by 4 logN-valued Shared Variable," Tech. Report Forschungsinstitut für Mathematik, ETH, Zürich, March 1980. (See also Proc. of the 21st Annual Symp. on Foundations of Computer Science, Syracuse, NY, Oct. 1980, 407-410.
• 19: Rabin, M.O., "The Choice Coordination Problem," Acta Informatica, Vol. 17, 1982, 121-134.
• 20: John H. Reif, Logics for probabilistic programming (Extended Abstract), Proceedings of the twelfth annual ACM symposium on Theory of computing, p.8-13, April 28-30, 1980, Los Angeles, California, United States [doi>10.1145/800141.804647]

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.3 PROBABILITY AND STATISTICS
      Subjects: Probabilistic algorithms (including Monte Carlo)

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory; Temporal logic

General Terms:
Algorithms, Theory