×

zbMATH — the first resource for mathematics

Communicating processes with value-passing and assignments. (English) Zbl 0784.68055
Summary: A semantic theory of an imperative language which allows value-passing and assignments as a simple action prefixing is described. Three different semantic approaches are given: denotational based on the mathematical model Acceptance Trees, axiomatic based on inequations and behavioural in terms of testing. The equivalence of these different approaches is shown. The results are compared with similar results for other languages such as CSP and Occam.

MSC:
68Q55 Semantics in the theory of computing
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Brookes, S.D., Hoare, C.A.R. and Roscoe, A.W. ?A Theory of Communicating Sequential Processes?,JACM 31(7), 560-599 1984. · Zbl 0628.68025 · doi:10.1145/828.833
[2] Brinksma, E. ?A Tutorial on LOTOS.?Proceedings of IFIP Workshop on Protocol Specification, Testing and Verification V, M. Diaz, ed., pp. 73-84. North-Holland, Amsterdam, 1986.
[3] DeNicola, R. and M. Hennessy. ?Testing Equivalences for Processes.?Theoretical Computer Science, 24, 1984, pp. 83-113.
[4] Francez, N., Lehman, D. and Pnueli, A. ?A Linear History of Semantics for Languages with Distributed Processing,TCS, 32, 25-46, 1984. · Zbl 0543.68019 · doi:10.1016/0304-3975(84)90022-7
[5] Guessarian, I., ?Algebraic Semantics?,Springer-Verlag Lecture Notes in Computer Science, vol.99, 1981.
[6] Hennessy, M., Ingólfsdóttir, A. A Theory of Communicating Processes With Value-Passing, University of Sussex Technical Report No 3/89, 1989. To appear in Information and Computation · Zbl 0794.68098
[7] Hennessy, M. ?Acceptance Trees.?Journal of the ACM, v. 32, n. 4, October 1985, pp. 896-928. · Zbl 0633.68074 · doi:10.1145/4221.4249
[8] Hennessy, M.Algebraic Theory of Processes. MIT Press, Cambridge, 1988. · Zbl 0744.68047
[9] Hennessy, M., A Proof System for Communicating Processes With Value - Passing,Formal Aspects of Computing, vol.3, 1991, pp. 346-366. · Zbl 0736.68057 · doi:10.1007/BF01642508
[10] Hennessy, M. and Plotkin, G., ?A Term Model for CCS?,Springer-Verlag Lecture Notes in Computer Science, vol.88, 1980. · Zbl 0479.68011
[11] Hoare, C.A.R. ?Communicating Sequential Processes?,Comm. ACM, 21(8), 666-677 1978. · Zbl 0383.68028 · doi:10.1145/359576.359585
[12] Hoare, C.A.R.Communicating Sequential Processes. Prentice-Hall International, London, 1985. · Zbl 0637.68007
[13] Hoare, C.A.R. and Roscoe, A.W., ?The Laws of Occam?, TCS 60, pp 177-229, 1988. · Zbl 0719.68039 · doi:10.1016/0304-3975(88)90049-7
[14] Inmos Ltd.,The Occam Programming Manual, Prentice-Hall, London, 1984.
[15] Milner, R.A Calculus of Communicating Systems, Lecture Notes in Computer Science 92. Springer-Verlag, Berlin, 1980. · Zbl 0452.68027
[16] Milne, R., ?Concurrency Models and Axioms?, RAISE/STC/REM/6/V2, STC Technology Ltd., 1988.
[17] Milner, R.,Calculus for Communication and Concurrency, Prentice-Hall, London 1989. · Zbl 0683.68008
[18] Olderog, E.R., Process Theory: Semantics, Specifications and Verifications, in J.W. deBakker, W.P. deRover, G. Rozenberg (Eds), Current Trends in Concurrency, Lecture Notes in Computer Science 224, Springer-Verlag, 1986, pp 442-509.
[19] Plotkin, G., ?Lecture Notes in Domain Theory?, University of Edinburgh, 1981.
[20] Plotkin, G., ?An Operational Semantics for CSP?,Proc. of IFIP WG 2.2, Working Conference on Formal Description of Programming Concepts 11, 1989. · Zbl 0512.68012
[21] Roscoe, A.W., ?Denotational Semantics for Occam?, PRG Monograph, Oxford University, 1988. · Zbl 0565.68024
[22] Schmidt, D.,Denotational Semantics, Allen and Bacon, 1986.
[23] Smyth, M. and Plotkin, G., ?The Category-Theoretic Solution of Recursive Domain Equations?,SIAM Journal on Computing, vol.11, No.4, 1982. · Zbl 0493.68022
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.