Compactness in semantics for merge and fair merge

  • J. W. de Bakker
  • J. I. Zucker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 164)


An analysis of the role of compactness in defining the semantics of the merge and fair merge operations is provided. In a suitable context of hyperspaces (sets of subsets) a set is compact iff it is the limit of a sequence of finite sets; hence, compactness generalises bounded nondeterminacy. The merge operation is investigated in the setting of a simple language with elementary actions, sequential composition, nondeterministic choice and recursion. Metric topology is used as a framework to assign both a linear time and a branching time semantics to this language. It is then shown that the resulting meanings are compact trace sets and compact processes, respectively. This result complements previous work by De Bakker, Bergstra, Klop & Meyer. For the fair merge, an approach using scheduling through random choices is adopted — since a direct definition precludes the use of closed, let alone of compact sets. In the indirect approach, a compactness condition is used to show that the fair merge of two fair processes yields a fair process.


Compact Subset Cauchy Sequence Compact Process Basic Node Denotational Semantic 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    APT, K.R. & E.R. OLDEROG, Proof rules dealing with fairness, Proc. Logic of Programs 1981 (D. Kozen, ed.), 1–9, LNCS 131, Springer, 1982.Google Scholar
  2. [2]
    APT, K.R. & G.D. PLOTKIN, A Cook's tour of countable nondeterminism, Proc. 8th ICALP (S. Even & O. Kariv, eds), 479–494, LNCS 115, Springer, 1981.Google Scholar
  3. [3]
    ARNOLD, A., Topological characterizations of infinite behaviours of transition systems, Proc. 10th ICALP (J. Diaz, ed.), 28–38, LNCS 154, Springer, 1983.Google Scholar
  4. [4]
    ARNOLD, A. & M. NIVAT, Metric interpretations of infinite trees and semantics of nondeterministic recursive programs, Theoretical Computer Science 11, 181–206, 1980.Google Scholar
  5. [5]
    ARNOLD, A. M. NIVAT, The metric space of infinite trees, algebraic and topological properties, Fund. Inform. III, 4, 445–476, 1980.Google Scholar
  6. [6]
    DE BAKKER, J.W., Mathematical Theory of Program Correctness, Prentice-Hall International, 1980.Google Scholar
  7. [7]
    DE BAKKER, J.W., J.A. BERGSTRA, J.W. KLOP & J.-J.Ch. MEYER, Linear time and branching time semantics for recursion with merge, Proc. 10th ICALP (J. Diaz, ed.), 39–51, LNCS 154, Springer, 1983.Google Scholar
  8. [8]
    DE BAKKER, J.W. & J.I. ZUCKER, Denotational semantics of concurrency, Proc. 14th ACM Symp. on Theory of Computing, 153–158, 1982.Google Scholar
  9. [9]
    DE BAKKER, J.W. & J.I. ZCKER, Processes and the denotational semantics of concurrency, Information and Control, 54, 70–120, 1982.Google Scholar
  10. [10]
    DE BAKKER, J.W. & J.I. ZUCKER, Processes and a fair semantics for the ADA rendezvous, Proc. 10th ICALP (J. Diaz, ed.), 52–66, LNCS 154, Springer, 1983.Google Scholar
  11. [11]
    BERGSTRA, J.A. & J.W. KLOP, Process algebra for communication and mutual exclusion, Department of Computer Science Technical Report IW 218/83, Mathematisch Centrum, 1983.Google Scholar
  12. [12]
    BERGSTRA, J.A. & J.W. KLOP, The algebra of recursively defined processes and the algebra of regular processes, Department of Computer Science Report IW 235/83, Mathematisch Centrum, 1983.Google Scholar
  13. [13]
    DUGUNDJI, J., Topology, Allen and Bacon, 1966.Google Scholar
  14. [14]
    ENGELKING, R., General Topology, Polish Scientific Publishers, 1977.Google Scholar
  15. [15]
    GIERZ, G. et al., A Compendium of Continuous Lattices, Springer, 1980.Google Scholar
  16. [16]
    GOLSON, W. & W.C. ROUNDS, Connections between two theories of concurrency — metric spaces and synchronization trees, University of Michigan Computing Research Laboratory Technical Report CRL TR 3-83, 1983.Google Scholar
  17. [17]
    HAHN, H., Reelle Funktionen, Chelsea, 1948.Google Scholar
  18. [18]
    HOPCROFT, J.E. & J.D. ULLMAN, Introduction to Automata Theory, Languages and Computation, Addison-Wesley, 1979.Google Scholar
  19. [19]
    MICHAEL, E., Topologies on spaces of subsets, Trans. AMS 71, 152–182, 1951.Google Scholar
  20. [20]
    MILNER, R., A Calculus of Communicating Systems, LNCS 92, Springer, 1980.Google Scholar
  21. [21]
    NIVAT, M., Infinite words, infinite trees, infinite computations, Foundations of Computer Science III.2 (J.W. de Bakker & J. van Leeuwen, eds), 3–52, Mathematical Centre Tracts 109, 1979.Google Scholar
  22. [22]
    NIVAT, M., Synchronization of concurrent processes, Formal Language Theory (R.V. Book, ed.), 429–454, Academic Press, 1980.Google Scholar
  23. [23]
    PLOTKIN, G.D., A power domain for countable nondeterminism, Proc. 9th ICALP (M. Nielsen & E.M. Schmidt, eds), 418–428, LNCS 140, Springer, 1982.Google Scholar
  24. [24]
    ROUNDS, W.C., On the relationships between Scott domains, synchronization trees, and metric spaces, preprint, Department of Computer and Communication Sciences, University of Michigan, 1983.Google Scholar
  25. [25]
    SCOTT, D.S., Domain equations, Proc. 6th IBM Symp. on Mathematical Foundations of Computer Science: Logical Aspects of Programs, 105–256, IBM Japan, 1981.Google Scholar
  26. [26]
    SMYTH, M.B., Power domains and predicate transformers, a topological view, Proc. 10th ICALP (J. Diaz, ed.), 662–675, LNCS 154, Springer, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • J. W. de Bakker
    • 1
    • 2
  • J. I. Zucker
    • 3
  1. 1.Mathematical CentreAmsterdam
  2. 2.Free UniversityAmsterdam
  3. 3.Computer Science DepartmentSUNY at Buffalo

Personalised recommendations