Advertisement

Distributed Concurrent Programs as Strategies in Games

  • Anil Nerode
  • Alexander Yakhnis
  • Vladimir Yakhnis
Chapter
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 12)

Abstract

This paper models synchronized distributed computing by extending the games in [Nerode-Yakhnis-Yakhnis, [17]]. The intention is to provide a precise tool for reasoning about the correctness of distributed synchronized programs. [17] introduced the paradigm that concurrent programs denote state strategies in corresponding two-person computational games. Program specifications were winning sets of plays in such games. This was carried out relative to a shared memory model. It is our belief that state strategies on appropriate game trees capture all there is to any program. So here we extend this paradigm to synchronous message-passing models, which may have shared memory as well, by introducing additional rules of the game, and additional operations for constructing new strategies from old, which capture completely the syntax and semantics of OCCAM’S PAR program construct and message-passing. Almost all the results about operations on strategies and programs from [17] extend to the distributed context.

Keywords

Computational State Shared Memory Communication Instruction State Strategy Concurrent Program 
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. [1]
    Alpern, B. and F.B. Schneider [1987], Proving Boolean Combinations of Deterministic Properties. Symposium on Logic in Computer Science, 131–137.Google Scholar
  2. [2]
    Andrews, G.R. and F.B. Schneider [1983], Concepts and Notations for Concurrent Programming. ACM Computing Surveys 15, no. 1, 3–43.zbMATHCrossRefGoogle Scholar
  3. [3]
    Abadi, M., L. Lamport and P. Wolper [1989], Realizable and Unrealizable Specifications of Reactive Systems. Proc. 1989 ICALP Conference.Google Scholar
  4. [4]
    Apt, K.R. and E-R. Olderog [1991], Verification of Sequential and Concurrent Programs. Springer-Verlag.Google Scholar
  5. [5]
    Ben-Ari, M. [1990], Principles of Concurrent Programming. Prentice-Hall.Google Scholar
  6. [6]
    de Bakker, J.W. and J.I. Zucker [1982], Processes and the Denotational Semantics of Concurrency. Information and Control, 54, 70–120.MathSciNetzbMATHCrossRefGoogle Scholar
  7. [7]
    Inmos Limited [1988], OCCAM 2 Reference Manual, Prentice-Hall Int., Hemel Hempstead.Google Scholar
  8. [8]
    Hwang, Kai and F.A. Briggs [1984], Computer Architecture and Parallel Processing. McGraw-Hill.Google Scholar
  9. [9]
    Gurevich, Y. and L. Moss [1990], Algebraic Operational Semantics and OCCAM. Mathematical Foundations of Computer Science, LNCS.Google Scholar
  10. [10]
    Hanna, F.K. and N. Daeche [1985], Specification and Verification Using Higher-Order Logic. Proc. of 7th Int. Conf. on Computer Hardware Design Languages, Tokyo.Google Scholar
  11. [11]
    Hoare, C.A.R. [1985], Communicating Sequential Processes. Prentice-Hall Int., Hemel Hempstead.zbMATHGoogle Scholar
  12. [12]
    Hoare, C.A.R. [1978], Communicating Sequential Processes. Commun. ACM, 21(8), 666–677.MathSciNetzbMATHCrossRefGoogle Scholar
  13. [13]
    Levin, G.M. and D. Gries [1981], A Proof Technique for Communicating Sequential Processes. Acta Inf. 15, 281–302.MathSciNetzbMATHCrossRefGoogle Scholar
  14. [14]
    Loeckx, J., K. Sieber and R. Stansifer [1984], The Foundations of Program Verification. John Wiley & Sons.Google Scholar
  15. [15]
    Manna, Z. and A. Pnueli [1987], Specification and Verification of Concurrent Programs by Automata. 14th Annual Symposium on Principles of Programming Languages, 1–12.Google Scholar
  16. [16]
    Manna, Z. and A. Pnueli [1992], The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag.Google Scholar
  17. [17]
    Nerode, A., A. Yakhnis and V. Yakhnis [1992], Concurrent Programs as Strategies in Games. In: Logic from Computer Science, Y. Moschovakis (ed.), Springer-Verlag.Google Scholar
  18. [18]
    Owicki, S. and D. Gries [1976], An Axiomatic Proof Technique for Parallel Programs. Acta Inf. 6, 319–340.MathSciNetzbMATHCrossRefGoogle Scholar
  19. [19]
    Pnueli, A. [1986], Application of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. In Current Trends in Concurrency, LICS.Google Scholar
  20. [20]
    Pnueli, A. and P. Rosner [1989], On the Synthesis of a Reactive Module. Proc. of 16th Annual ACCM Symp. on Principles of Programming Languages.Google Scholar
  21. [21]
    Pountain, D. and D. May [1987], A Tutorial Introduction to OCCAM Programming. McGraw-Hill, New York.Google Scholar
  22. [22]
    Yakhnis, A. [1989], Concurrent Specifications and their Gurevich-Harrington Games and Representation of Programs as Strategies. 7th Army Conf. on Applied Math and Computing.Google Scholar
  23. [23]
    Yakhnis, A. [1990], Game-Theoretic Semantics for Concurrent Programs and their Specifications. Ph.D. Diss., Cornell University.Google Scholar
  24. [24]
    Yakhnis, V. [1989], Extraction of Concurrent Programs from Gurevich-Harrington Games. 7th Army Conf. on Applied Math and Computing.Google Scholar
  25. [25]
    Yakhnis, V. [1990], Concurrent Programs. Calculus of State Strategies, and Gurevich Harrington Games. Ph.D. Diss., Cornell University.Google Scholar
  26. [26]
    Yakhnis, A. and V. Yakhnis [1990], Extension of Gurevich-Harrington’s Restricted Memory Determinacy Theorem: a Criterion of the Winning Player and an Explicit Class of Winning Strategies. Annals of Pure and Appl. Logic 48, 277–297.MathSciNetzbMATHCrossRefGoogle Scholar
  27. [27]
    Yakhnis, A. and V. Yakhnis [1993], Gurevich-Harrington’s Games Defined by Finite Automata. To appear in Annals of Pure and Appl. Logic.Google Scholar

Copyright information

© Springer Science+Business Media New York 1993

Authors and Affiliations

  • Anil Nerode
    • 1
  • Alexander Yakhnis
    • 1
  • Vladimir Yakhnis
    • 2
  1. 1.Mathematical Sciences InstituteCornell UniversityIthacaUSA
  2. 2.IBM Corporation EndicottNYUSA

Personalised recommendations