Advertisement

Linear time and branching time semantics for recursion with merge

  • J. W. de Bakker
  • J. A. Bergstra
  • J. W. Klop
  • J. -J. Ch. Meyer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)

Abstract

We consider two ways of assigning semantics to a class of statements built from a set of atomic actions (the ‘alphabet‘), by means of sequential composition, nondeterministic choice, recursion and merge (arbitrary interleaving). The first is linear time semantics (LT), stated in terms of trace theory; the semantic domain is the collection of all closed sets of finite and infinite words. The second is branching time semantics (BT), as introduced by de Bakker and Zucker; here the semantic domain is the metric completion of the collection of finite processes. For LT we prove the continuity of the operations (merge, sequential composition) in a direct, combinatorial way.

Next, a connection between LT and BT is established by means of the operation trace which assigns to a process its set of traces. If the alphabet is finite, the trace set of a process is closed and trace is a continuous operation. Using trace, we then can carry over BT into LT.

Keywords

Cauchy Sequence Sequential Composition Denotational Semantic Semantic Domain Trace Theory 
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]
    DE BAKKER, J.W., Mathematical Theory of Program Correctness, Prentice-Hall International, 1980.Google Scholar
  2. [2]
    DE BAKKER, J.W., J.A. BERGSTRA, J.W. KLOP & J.-J. CH. MEYER, Linear time and branching time semantics for recursion with merge. Report IW 211/82, Mathematical Centre, Amsterdam 1982.Google Scholar
  3. [3]
    DE BAKKER, J.W. & J.I. ZUCKER, Denotational semantics of concurrency, Proc. 14th ACM Symp. on Theory of Computing, pp.153–158, 1982.Google Scholar
  4. [4]
    DE BAKKER, J.W. & J.I. ZUCKER, Processes and the denotational semantics of concurrency, Report IW 209/82, Mathematisch centrum, Amsterdam 1982.Google Scholar
  5. [5]
    BERGSTRA, J.A. & J.W. KLOP, Fixed point semantics in process algebras, Report IW 206/82, Mathematisch Centrum, Amsterdam 1982.Google Scholar
  6. [6]
    ENGELKING, R., General Topology, Polish Scientific Publishers, 1977.Google Scholar
  7. [7]
    FRANCEZ, N., D.J. LEHMANN & A. PNUELI, Linear history semantics for distributed languages, Proc. 21st Symp. Foundations of Computer Science, IEEE 1980, pp.143–151.Google Scholar
  8. [8]
    MILNER, R., A Calculus for Communicating Systems, Springer LNCS 92, 1980.Google Scholar
  9. [9]
    MILNER, R., A complete inference system for a class of regular behaviours, Preprint, Edinburgh 1982.Google Scholar
  10. [10]
    NIVAT, M., Mots infinis engendrés par une grammaire algébrique, RAIRO Informatique Théorique Vol.11 (1977) pp.311–327.Google Scholar
  11. [11]
    NIVAT, M., Sur les ensembles des mots infinis engendrés par une grammaire algébrique, RAIRO Informatique Théorique Vol.12 (1978) pp.259–278.Google Scholar
  12. [12]
    NIVAT, M., Infinite words, infinite trees, infinite computations, Foundations of Computer Science III.2 (J.W. de Bakker & J. van Leeuwen,eds.) pp.3–52, Mathematical Centre Tracts 109, 1979.Google Scholar
  13. [13]
    NIVAT, M., Synchronization of concurrent processes, Formal Language Theory (R.V. Book, ed.), pp.429–454, Academic Press, 1980.Google Scholar
  14. [14]
    PLOTKIN, G.D., A power domain construction, SIAM J. on Comp., 5 (1976), pp.452–487.Google Scholar
  15. [15]
    SCOTT, D.S., Data types as lattices, SIAM J. on Comp., 5 (1976), pp.522–587.Google Scholar
  16. [16]
    SCOTT, D.S., Domains for denotational semantics. Proc. 9th ICALP (M. Nielsen & E.M. Schmidt, eds.), pp.577–613, Springer LNCS 140, 1982.Google Scholar
  17. [17]
    SMYTH, M.B., Power domains, J. Comp. Syst. sciences, 16 (1978), pp.23–36.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • J. W. de Bakker
    • 1
    • 2
  • J. A. Bergstra
    • 3
  • J. W. Klop
    • 3
  • J. -J. Ch. Meyer
    • 2
  1. 1.Mathematical CentreSJ Amsterdam
  2. 2.Free UniversityAmsterdam
  3. 3.Mathematical CentreAmsterdam

Personalised recommendations