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.
Supported in part by ARO contract DAAL03-91-C-0027 and by DARPA-US ARMY AMCCOM (Picatinny Arsenal, N.J.) contract DAAA21-92-C-0013 to ORA Corporation.
Supported by DARPA-US ARMY AMCCOM (Picatinny Arsenal, N.J.) contract DAAA21-92-C-0013 to ORA Corporation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Alpern, B. and F.B. Schneider [1987], Proving Boolean Combinations of Deterministic Properties. Symposium on Logic in Computer Science, 131–137.
Andrews, G.R. and F.B. Schneider [1983], Concepts and Notations for Concurrent Programming. ACM Computing Surveys 15, no. 1, 3–43.
Abadi, M., L. Lamport and P. Wolper [1989], Realizable and Unrealizable Specifications of Reactive Systems. Proc. 1989 ICALP Conference.
Apt, K.R. and E-R. Olderog [1991], Verification of Sequential and Concurrent Programs. Springer-Verlag.
Ben-Ari, M. [1990], Principles of Concurrent Programming. Prentice-Hall.
de Bakker, J.W. and J.I. Zucker [1982], Processes and the Denotational Semantics of Concurrency. Information and Control, 54, 70–120.
Inmos Limited [1988], OCCAM 2 Reference Manual, Prentice-Hall Int., Hemel Hempstead.
Hwang, Kai and F.A. Briggs [1984], Computer Architecture and Parallel Processing. McGraw-Hill.
Gurevich, Y. and L. Moss [1990], Algebraic Operational Semantics and OCCAM. Mathematical Foundations of Computer Science, LNCS.
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.
Hoare, C.A.R. [1985], Communicating Sequential Processes. Prentice-Hall Int., Hemel Hempstead.
Hoare, C.A.R. [1978], Communicating Sequential Processes. Commun. ACM, 21(8), 666–677.
Levin, G.M. and D. Gries [1981], A Proof Technique for Communicating Sequential Processes. Acta Inf. 15, 281–302.
Loeckx, J., K. Sieber and R. Stansifer [1984], The Foundations of Program Verification. John Wiley & Sons.
Manna, Z. and A. Pnueli [1987], Specification and Verification of Concurrent Programs by Automata. 14th Annual Symposium on Principles of Programming Languages, 1–12.
Manna, Z. and A. Pnueli [1992], The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag.
Nerode, A., A. Yakhnis and V. Yakhnis [1992], Concurrent Programs as Strategies in Games. In: Logic from Computer Science, Y. Moschovakis (ed.), Springer-Verlag.
Owicki, S. and D. Gries [1976], An Axiomatic Proof Technique for Parallel Programs. Acta Inf. 6, 319–340.
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.
Pnueli, A. and P. Rosner [1989], On the Synthesis of a Reactive Module. Proc. of 16th Annual ACCM Symp. on Principles of Programming Languages.
Pountain, D. and D. May [1987], A Tutorial Introduction to OCCAM Programming. McGraw-Hill, New York.
Yakhnis, A. [1989], Concurrent Specifications and their Gurevich-Harrington Games and Representation of Programs as Strategies. 7th Army Conf. on Applied Math and Computing.
Yakhnis, A. [1990], Game-Theoretic Semantics for Concurrent Programs and their Specifications. Ph.D. Diss., Cornell University.
Yakhnis, V. [1989], Extraction of Concurrent Programs from Gurevich-Harrington Games. 7th Army Conf. on Applied Math and Computing.
Yakhnis, V. [1990], Concurrent Programs. Calculus of State Strategies, and Gurevich Harrington Games. Ph.D. Diss., Cornell University.
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.
Yakhnis, A. and V. Yakhnis [1993], Gurevich-Harrington’s Games Defined by Finite Automata. To appear in Annals of Pure and Appl. Logic.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer Science+Business Media New York
About this chapter
Cite this chapter
Nerode, A., Yakhnis, A., Yakhnis, V. (1993). Distributed Concurrent Programs as Strategies in Games. In: Crossley, J.N., Remmel, J.B., Shore, R.A., Sweedler, M.E. (eds) Logical Methods. Progress in Computer Science and Applied Logic, vol 12. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4612-0325-4_21
Download citation
DOI: https://doi.org/10.1007/978-1-4612-0325-4_21
Publisher Name: Birkhäuser, Boston, MA
Print ISBN: 978-1-4612-6708-9
Online ISBN: 978-1-4612-0325-4
eBook Packages: Springer Book Archive