×

zbMATH — the first resource for mathematics

A proof system for communicating processes with value-passing. (English) Zbl 0736.68057
The language studied is essentially the original value-passing version of CCS except that \(\tau\) is replaced by versions of the internal and external choice operators from TCSP. The reasonings about data and about processes are dissociated. The main proof system is used for the reasoning about processes. For the reasoning about data a subsidiary proof system would be used or called by the main one. In the denotational model the input expression c?x.p is represented as a function mapping data-values to semantic objects. The main system is shown to be sound and complete for finite processes with respect to a denotational semantics based on Acceptance Trees.

MSC:
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Apt, K.: Proving Correctness of CSP Programs – A tutorial.Proceedings of IFIP Workshop on Protocol Specification, Testing and Verification V, M. Diaz (ed.), pp. 73–84, North-Holland, Amsterdam, 1986.
[2] Dijkstra, E. W.:A Discipline of Programming. Prentice Hall, Englewood Cliffs, 1976. · Zbl 0368.68005
[3] Hennessy, M.: Acceptance Trees.Journal of the ACM,32 (4), 896–928 (1985). · Zbl 0633.68074 · doi:10.1145/4221.4249
[4] Hennessy, M.:Algebraic Theory of Processes. MIT Press, Cambridge, 1988. · Zbl 0744.68047
[5] Hennessy, M and Ingolfsdottir, A.: A Theory of Communicating Processes with Value-passing. University of Sussex Technical Report No 3/89, 1989. Also presented at ICALP ’90. · Zbl 0729.68020
[6] Hoare, C. A. R.: Communicating Sequential Processes.Communications of ACM,21 (8), 666–677 (1978). · Zbl 0383.68028 · doi:10.1145/359576.359585
[7] Hoare, C. A. R.Communicating Sequential Processes. Prentice-Hall International, London, 1985. · Zbl 0637.68007
[8] Hoare, C. A. R. and Roscoe, A. W.: The Laws of Occam. PRG Monograph, Oxford University, 1986. (Also published inTheoretical Computer Science) · Zbl 0719.68039
[9] Milne, R.: Concurrency Models and Axioms. RAISE/STC/REM/6/V2, STC Technology Ltd., 1988.
[10] Milner, R.:A Calculus of Communicating Systems. Lecture Notes in Computer Science 92, Springer-Verlag, Berlin, 1980. · Zbl 0452.68027
[11] Milner, R.:Calculus for Communication and Concurrency. Prentice-Hall, London 1989. · Zbl 0683.68008
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.