A proof system for communicating processes with value-passing

DOI10.1007/BF01642508MaRDI QIDQ1179808zbMATH OpenFDO

Authors Matthew Hennessy

Publication date 27 June 1992

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF01642508

zbMATH Keywords

algebraic lawsCCScompletenessproof systemvalue-passing

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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.

Recommendations

• scientific article; zbMATH DE number 4205976
• A theory of communicating processes with value passing
• scientific article; zbMATH DE number 177815
• Proof systems for message-passing process algebras

Cites work

• A calculus of communicating systems
• Acceptance trees
• Communicating sequential processes
• scientific article; zbMATH DE number 4205976 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• The laws of Occam programming

Cited in

(22)

• Bisimulations for a calculus of broadcasting systems
• A theory of communicating processes with value passing
• Process algebra with guards: Combining hoare logic with process algebra
• Linda-based applicative and imperative process algebras
• Proof systems for message-passing process algebras
• Planning proofs of equations in CCS
• On the expressiveness of choice quantification
• A modal logic for message passing processes
• A theory of bisimulation for the -calculus
• Formalising a value-passing calculus in H0L
• Probabilistic bisimulations for quantum processes
• A symbolic approach to value-passing processes
• The Value-Passing Calculus
• scientific article; zbMATH DE number 4205976 (Why is no real title available?)
• scientific article; zbMATH DE number 177815 (Why is no real title available?)
• Value-passing CCS with noisy channels
• Axiomatising real-timed processes
• Symbolic transition graph with assignment
• Branching bisimulation semantics for quantum processes
• Communicating processes with value-passing and assignments
• Revisiting sequential composition in process calculi
• Theory of interaction

This page was built for publication: A proof system for communicating processes with value-passing

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1179808)