Verification of multiprocess probabilistic protocols
Tóm tắt
In this paper we demonstrate the utility of temporal logic to the formal verification of probabilistic distributed programs. The approach taken is to represent the quantitative notion of probabilistic computations by the qualitative abstraction ofextreme fairness. The method is illustrated first on the dining philosophers problem [3] and then on a new probabilistic symmetric solution to then-processes mutual exclusion problem. Two related solutions are presented corresponding to different assumptions about the granularity of a compound test.
Tài liệu tham khảo
Burns JE, Fischer MJ, Jackson P, Lynch NA, Peterson GL (1978) Shared data requirements for imolementation of mutual exclusion using a test-and-set primitive. Proc Intr Conf Parallel Processing, pp 79–87
Cohen, S, Lehmann D, Pnueli A (1984) Symmetric and economical solution to the mutual exclusion problem in distributed systems. Theor Comp Sci 34:215–226
Dijkstra EW (1972) Hierarchical ordering of sequential process. Operating system techniques. Academic Press
Feller W (1967) An introduction to probability theory and its appliction 3rd ed, vol 1, ch. XIII, section 7. Wiley, pp 322–324
Hart S, Sharir M, Pnueli A (1983) Termintion of probabilistic concurrent programs. TOPLAS 5:356–380
Itai A, Rodeh M (1981) The lord of the ring, or probabilistic methods for breaking symmetry in distributive networks. RJ 3110, IBM, San Jose
Lehmann D, Rabin MO (1981) On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem (extended abstract) Conf Record of the 8th Annual ACM Symp on Principles of Programming Languages, Williamsburg, VA, Jan 1981, pp 133–138
Lehmann D, Shelah S (1982) Reasoning with time and chance. Inf Control 53: 165–198
Lichtenstein O, Pnueli A, Zuck L (1985) The glory of the past. Proceedings of the Workshop on Logics of Programs, Spriger-Verlag, New York
Manna Z, Pnueli A (1981) Verification of concurrent programs: temporal proof principles. Proc of the Workshop on Logic of Programs. Springer-Verlag, New York, pp 200–252
Manna Z, Pnueli A (1982) Verification of concurrent programs: a temporal proof system. Proc 4th School on Advanced Programming, Amsterdam
Manna Z, Pnueli A (1983) How to cook a temporal system for your pet language. Proc of the 10th Annual ACM Symp on Principles of Programming Languages
Owicki S, Lamport L (1982) Proving liveness properties of concurrent programs. TOPLAS 4:455–495
Pnueli A (1983) On the extremely fair treatment of probabilistic algorithms. Proc of the 15th Annual Symp on Theory of Computing
Rabin MO (1976) Probabilistic algorithms. Algorithms and complexity new directions and recent results. Academic Press, New York
Rabin MO (1980) N-process synchronization by 4 logN-valued shared variables. Tech Report Forschungsinstitute für Mathematik, ETH, Zürich
Rabin MO (1982) The choice coordimation problem, Acta Inf 17:121–134
Sharir M, Hart S (1983) Probabilistic temporal logics for finite and bounded models. Tel-Aviv University, Tel-Aviv