×

zbMATH — the first resource for mathematics

Proof systems for message-passing process algebras. (English) Zbl 0857.68040
Summary: We give sound and complete proof systems for a variety of bisimulation based equivalences over a message-passing process algebra. The process algebra is a generalisation of pure \(CCS\) where the actions consist of receiving and sending messages or data on communication channels; the standard prefixing operator a.p is replaced by the two operators \(c?x.p\) and \(c!e.p\) and in addition messages can be tested by a conditional construct. The various proof systems are parametrised on auxiliary proof systems for deciding on equalities or more general boolean identities over the expression language for data. The completeness of these proof systems are thus relative to the completeness of the auxiliary proof systems.

MSC:
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Burns, G. A language for value-passing ccs. Technical Report ECS-LFCS-91-175, University of Edinburgh, August 1991.
[2] Cleaveland, R., Parrow, J., Steffen, B. The concurrency workbench: A semantics based verification tool for finite state systems.ACM Transactions on Programming Systems, 15:36-72, 1989. · doi:10.1145/151646.151648
[3] Groote, J.F., Ponse, A. The syntax and semantics of?CRL. Technical Report CS-R9076, CWI, Amsterdam, 1990.
[4] Groote, J.F., Ponse, A. Proof theory for?CRL. Technical Report CS-R9138, CWI, Amsterdam, 1991. · Zbl 0813.68135
[5] Hennessy, M.An Algebraic Theory of Processes. MIT Press, 1988. · Zbl 0744.68047
[6] Hennessy, M. A proof system for communicating processes with value-passing.Formal Aspects of Computer Science, 3:346-366, 1991. · Zbl 0736.68057 · doi:10.1007/BF01642508
[7] Hennessy, M., Ingolfsdottir, A. A theory of communicating processes with value-passing.Information and Computation, 107(2):202-236, 1993. · Zbl 0794.68098 · doi:10.1006/inco.1993.1067
[8] Hennessy, M. Lin, H. Symbolic bisimulations. Theoretical Computer Science, 138:353-389, 1995. · Zbl 0874.68187 · doi:10.1016/0304-3975(94)00172-F
[9] Hennessy, M. Liu, X. A modal logic for message passing processes.Acta Informatica, 32:375-393, 1995. · Zbl 0827.68102
[10] Hoare, C.A.R., Roscoe, A.W. The laws of occam. Technical Report PRG Monograph 53, Oxford University Computing Laboratory, 1986. · Zbl 0719.68039
[11] Lin, H. PAM: A process algebra manipulator. In K. Larsen and A. Skou, editors,Computer Aided Verification, volume 575 ofLecture Notes in Computer Science, pages 136-146. Springer-Verlag, 1991. Also available as Sussex Computer Science Technical Report 9/91.
[12] Lin, H. A verification tool for value-passing processes. InProceedings of 13th International Symposium on Protocol Specification, Testing Verification, IFIP Transactions. North-Holland, 1993.
[13] Milner, R.Communication and Concurrency. Prentice-Hall, 1989.
[14] Milner, R., Parrow, J., Walker, D. A calculus of mobile proceses, part i.Information and Computation, 100(1):1-40, 1992. · Zbl 0752.68036 · doi:10.1016/0890-5401(92)90008-4
[15] Parrow, J., Sangiorgi, D. Algebraic theories for value-passing calculi. Technical report, University of Edinburgh, 1993. Also Technical Report from SICS, Sweden. To appear in Information and Computation. · Zbl 0836.03020
[16] Walker, D. Automated analysis of mutual exclusion algorithms using CCS.Formal Aspects of Computing, 1:273-292, 1989. · Zbl 0696.68039 · doi:10.1007/BF01887209
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.