Abstract
We present a variety of denotational linear time semantics for a language with recursion and “true” concurrency in a form of synchronous co-operation, which in the literature is known as step semantics. We show that this can be done by a generalization of known results for interleaving semantics. A general method is presented to define semantical operators and denotational semantics in the Smyth powerdomain of streams. With this method, first a naive and then more sophisticated semantics for synchronous co-operation are developed, which include such features as interleaving and synchronization. Then we refine the semantics to deal with a bounded number of processors, subatomic actions, maximal parallelism and a real-time operator. Finally, it is indicated how to apply these ideas to branching-time models, where it becomes possible to analyze deadlock behaviour as well as a form of “true” concurrency.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Aceto L, de Nicola R, Fantechi A (1987) Testing equivalences for event structures. In: Venturini Zilli M (ed) Proc Advanced School on Mathematical Models for the Semantics of Parallelism (Lect Notes Comput Sci 280 Springer, Berlin Heidelberg New York Tokyo, pp 1–20
Back RJ (1983) A continuous semantics for unbounded nondeterminism. TCS 23:187–210
de Bakker JW (1980) Mathematical theory of program correctness. Prentice Hall, London
Boudol G, Castellani I (1987) On the semantics of concurrency: partial orders and transition systems. In: Ehrig H et al. (eds) Proc TAPSOFT/CAAP '87 (Lect Notes Comput Sci 249) Springer, Berlin Heidelberg New York Tokyo, pp 123–137
Boudol G, Castellani I (1987) Concurrency and atomicity, rapports de recherche 748, INRIA Sophia Antipolis
Bergstra JA, Klop JW (1984) Process algebra for synchronous communication. Inf Control 60:109–137
de Bakker JW, Kok JN, Meyer J-JC, Olderog E-R, Zucker JI (1986) Contrasting themes in the semantics of imperative concurrency. In: de Bakker JW, de Roever WP, Rozenberg G (eds) (Lect Notes Comput Sci 224) Springer, Berlin Heidelberg New York Tokyo, pp 51–121
de Bakker JW, Meyer J-JC (1987) Metric semantics for concurrency, Tech Rep IR-139, Free University, Amsterdam
de Bakker JW, Meyer J-JC, Olderog E-R, Zucker JI (1989) Transition systems, metric spaces and ready sets in the semantics of uniform concurrency. JCSS 36:158–224
Broy M (1986) A theory for nondeterminism, parallelism, communication and concurrency. TCS 45:1–62
de Bakker JW, Zucker JI (1982) Processes and the denotational semantics of concurrency. Inf Control 54:70–120
de Nicola R, Hennessy M (1987) CCS without τ's, In: Ehrig H et al. (eds) Proc TAPSOFT/CAAP '87 (Lect Notes Comput Sci 249) Springer, Berlin Heidelberg New York Tokyo, pp 138–152
Degano P, de Nicola R, Montanari U (1987) CCS is an (augmented) contact free C/E system. In: Venturini Zilli M (ed) Proc Advanced School on Mathematical Models for the Semantics of Parallelism (Lect Notes Comput Sci 280) Springer, Berlin Heidelberg New York Tokyo, 144–165
Francez N, Hoare CAR, Lehmann DJ, de Roever WP (1979) Semantics of nondeterminism, concurrency and communication. JCSS 19:290–308
van Glabbeek RJ, Vaandrager FW (1987) Petri net models for algebraic theories of concurrency. In: de Bakker et al. (eds) Proc PARLE (Lect Notes Comput Sci 259) Springer, Berlin Heidelberg New York Tokyo, pp 224–242
Janicki R (1987) A formal semantics for concurrent systems with a priority relation. Acta Inf 24:33–55
Hoare CAR (1985) Communicating sequential processes. Prentice-Hall Englewood Cliffs, New Jersey
Kok JN, Rutten JJMM (1988) Contractions in comparing concurrency semantics. In: Lepistö T, Salomaa A (eds) Proc ICALP '88 (Lect Notes Comput Sci 317) Springer, Berlin Heidelberg New York Tokyo, pp 317–332
Koymans R, Shyamasundar RK, de Roever WP, Gerth R, Arun-Kumar S (1985) Compositional semantics for realtime distributed computing. In: Parikh R (ed) Proc Logics of Programs (Lect Notes Comput Sci 193) Springer, Berlin Heidelberg New York, pp 167–189
Mazurkiewicz A (1978) Concurrent program schemes and their interpretation, Rep DIAMI PB-78, Comput Sci Dept, Aarhus University, Aarhus, Denmark
Meyer, J-JC (1985) Programming calculi based on fixed point transformations: semantics and applications. Dissertation, Free University, Amsterdam
Milner R (1980) A calculus for communicating systems (Lect Notes Comput Sci 92) Springer, Berlin Heidelberg New York Tokyo
Meyer J-JC, de Vink EP (1987) Applications of compactness in the Smyth powerdomain of streams. In: Ehrig H et al. (eds) Proc TAPSOFT/CAAP '87. (Lect Notes Comput Sci 249) Springer, Berlin, Heidelberg New York Tokyo, 241–255
Olderog E-R, Hoare CAR (1986) Specification oriented semantics for communicating processes. Acta Inf 23:9–66
Plotkin GD (1976) A powerdomain construction. SIAM J Comput 5:452–487
Plotkin GD (1980) An operational semantics for CSP. In: Bjørner D (ed) Formal description of programming concepts II (Lect Notes Comput Sci 86) Springer, Berlin Heidelberg New York Tokyo, pp 527–553
Reisig W (1985) Petri nets. Springer, Berlin Heidelberg New York Tokyo
Rozenberg G, Verraedt R (1983) Subset languages of Petri nets I: the relationship to string languages and normal forms. TCS 26:301–326
Salwicki A, Müldner T (1981) On the algebraic properties of concurrent programs. In: Engeler E (ed) Proc Logic of Programs (Lect Notes Comput Sci 125) Springer, Berlin Heidelberg New York, pp 169–197
Smyth, MB (1978) Power domains. JCSS 16:23–36
Taubner DA, Vogler W (1987) The step failure semantics. In: Brandenburg FJ, Vidal Naquet G (eds) Proc STACS '87 (Lect Notes Comput Sci 247) Springer, Berlin Heidelberg New York Tokyo, pp 348–359
Winskel G (1980) Events in computation Ph.D. Thesis, Edinburgh University, Edinburgh
Author information
Authors and Affiliations
Additional information
John-Jules Meyer received his Master's degree in Mathematics in 1979 from the University of Leiden, and his Ph.D. degree in 1985 from the Free University Amsterdam. He is currently a Professor of Theoretical Computer Science, both at the Free University Amsterdam and at the University of Nijmegen. His current research interests include semantics of programming languages and logics for computer science, in particular artifical intelligence.
Erik de Vink received the M.S. degree in Mathematics from the University of Amsterdam. He is currently a Junior Researcher at the Department of Mathematics and Computer Science of the Free University Amsterdam. At the moment his main research concerns the semantics of concurrent and logic programming languages.
Rights and permissions
About this article
Cite this article
Meyer, J.J.C., de Vink, E.P. Step semantics for “true” concurrency with recursion. Distrib Comput 3, 130–145 (1989). https://doi.org/10.1007/BF01784023
Issue Date:
DOI: https://doi.org/10.1007/BF01784023