Acceptance trees

ABSTRACT

A simple model, AT, for nondeterministic machines is presented which is based on certain types of trees. A set of operations, &Sgr;, is defined over AT and it is shown to be completely characterized by a set of inequations over &Sgr;. AT is used to define the denotational semantics of a language for defining nondeterministic machines. The significance of the model is demonstrated by showing that this semantics reflects an intuitive operational semantics of machines based on the idea that machines should only be differentiated if there is some experiment that differentiates between them.

REFERENCES

• 1: BERGSTRA, J.A., AND KLOP, J.W.fixed point semantics in process algebras. Tech. Rep. iW 206/82, Mathematisch Centrum, Amsterdam, The Netherlands, 1982.
• 2: BERGSTRA, J.A., AND KLOP, J.W.Process algebra for communication and mutual exclusion. Tech. Rep. IW 218/83, Mathematisch Centrum, Amsterdam, The Netherlands, 1983.
• 3: BROOKES, S.D. A model for communicating sequential processes. Ph.D. dissertation. Oxford Univ., Oxford, England, 1983.
• 4: Stephen D. Brookes , William C. Rounds, Behavioural Equivalence Relations Induced by Programming Logics, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.97-108, July 18-22, 1983
• 5: S. D. Brookes , C. A. R. Hoare , A. W. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM (JACM), v.31 n.3, p.560-599, July 1984 [doi>10.1145/828.833]
• 6: DE BAKKER, J.W., AND ZUCKER, J. i.Processes and the denotational semantics of concurrency. Tech. Rep. IW 209/82, Mathematisch Centrum, Amsterdam, The Netherlands, 1982.
• 7: Rocco De Nicola, A Complete Set of Axioms for a Theory of Communicating Sequential Processes, Proceedings of the 1983 International FCT-Conference on Fundamentals of Computation Theory, p.115-126, August 21-27, 1983
• 8: DE NICOLA, R., AND HENNESSY, M.Testing equivalences for processes. Theor. Comput. Sci. 34, 1, 2 (1984), 83-135.
• 9: Seymour Ginsburg , H. Gordon Rice, Two Families of Languages Related to ALGOL, Journal of the ACM (JACM), v.9 n.3, p.350-371, July 1962 [doi>10.1145/321127.321132]
• 10: J. A. Goguen , J. W. Thatcher , E. G. Wagner , J. B. Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM (JACM), v.24 n.1, p.68-95, Jan. 1977 [doi>10.1145/321992.321997]
• 11: William G. Golson , William C. Rounds, Connections between two theories of concurrency: metric spaces and synchronization trees, Information and Control, v.57 n.2-3, p.102-124, May/June 1983 [doi>10.1016/S0019-9958(83)80039-4]
• 12: Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 13: Irene Guessarian, Algebraic Semantics, Springer-Verlag New York, Inc., Secaucus, NJ, 1981
• 14: HENNESSY, M.A term model for synchronous process. Inf. Control 51, 1 (Oct. 1981), 58-75.
• 15: M Hennessy, Synchronous and asynchronous experiments on processes, Information and Control, v.59 n.1-3, p.36-83, Oct./Nov./Dec. 1983 [doi>10.1016/S0019-9958(83)80029-1]
• 16: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 17: Matthew Hennessy , Gordon D. Plotkin, A Term Model for CCS, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, p.261-274, September 01-05, 1980
• 18: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 19: HOARE, C.A.R A model for communicating sequential processes. Tech. Monograph Prg.-22. Comput. Lab., Univ. of Oxford, Oxford, England, 1981.
• 20: John E. Hopcroft , Jeffrey D. Ullman, Formal languages and their relation to automata, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1969
• 21: HOWlE, J.An Introduction to Semigroup Theory. Academic Press, Orlando, Fla., 1976.
• 22: KENNAWAY, J. K.Formal semantics of nondeterminism and parallelism, Ph.D. dissertation. Univ. of Oxford, Oxford, England, 1981.
• 23: Richard Kennaway , C. A. R. Hoare, A Theory of Nondeterminism, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.338-350, July 14-18, 1980
• 24: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 25: MILNER, R.On relating synchrony and asynchrony, Tech. Rep. CSR-75-80, Univ. of Edinburgh, Edinburgh, Scotland, 1980.
• 26: MILNER, R.Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25, (1983), 267-310.
• 27: Ernst-Rüdiger Olderog , C. A. R. Hoare, Specification-Oriented Semantics for Communicating Processes, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.561-572, July 18-22, 1983
• 28: PLOTKIN, G.A structural approach to operational semantics, Lecture Notes. Aarhus University, Aarhus, Denmark, 1981.
• 29: ROUNDS, W.C., AND BROOKES, S.D.possible futures, acceptances, refusals, and communicating processes. In Proceedings of the 22nd Foundations of Computer Science Annual Symposium (Nashville, Tenn., Oct.). IEEE, New York, 1981.
• 30: Arto Salomaa, Two Complete Axiom Systems for the Algebra of Regular Events, Journal of the ACM (JACM), v.13 n.1, p.158-169, Jan. 1966 [doi>10.1145/321312.321326]
• 31: SCOTT, D.Data types as lattices. SIAM J. Comput. 5 (1976), 522-587.
• 32: STIRLING, C.A proof theoretic characterisation of observational equivalence, Tech. Rep. CSR- 132-83. Univ. of Edinburgh, Edinburgh, Scotland, 1983; Theor. Comput. Sci., to be published.
• 33: STIRLING, C.Unpublished manuscript.
• 34: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 35: WINSKEL, G.On powerdomains and modality. Theor. Comput. Sci. 36 (1985), 127-137.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Languages, Theory, Verification