Linear time and branching time semantics for recursion with merge
- 103 Downloads
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.
KeywordsCauchy Sequence Sequential Composition Denotational Semantic Semantic Domain Trace Theory
Unable to display preview. Download preview PDF.
- DE BAKKER, J.W., Mathematical Theory of Program Correctness, Prentice-Hall International, 1980.Google Scholar
- 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
- 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
- DE BAKKER, J.W. & J.I. ZUCKER, Processes and the denotational semantics of concurrency, Report IW 209/82, Mathematisch centrum, Amsterdam 1982.Google Scholar
- BERGSTRA, J.A. & J.W. KLOP, Fixed point semantics in process algebras, Report IW 206/82, Mathematisch Centrum, Amsterdam 1982.Google Scholar
- ENGELKING, R., General Topology, Polish Scientific Publishers, 1977.Google Scholar
- 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
- MILNER, R., A Calculus for Communicating Systems, Springer LNCS 92, 1980.Google Scholar
- MILNER, R., A complete inference system for a class of regular behaviours, Preprint, Edinburgh 1982.Google Scholar
- NIVAT, M., Mots infinis engendrés par une grammaire algébrique, RAIRO Informatique Théorique Vol.11 (1977) pp.311–327.Google Scholar
- 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
- 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
- NIVAT, M., Synchronization of concurrent processes, Formal Language Theory (R.V. Book, ed.), pp.429–454, Academic Press, 1980.Google Scholar
- PLOTKIN, G.D., A power domain construction, SIAM J. on Comp., 5 (1976), pp.452–487.Google Scholar
- SCOTT, D.S., Data types as lattices, SIAM J. on Comp., 5 (1976), pp.522–587.Google Scholar
- 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
- SMYTH, M.B., Power domains, J. Comp. Syst. sciences, 16 (1978), pp.23–36.Google Scholar