Value-passing CCS with noisy channels

Value-passing CCS, a full version of Milner’s CCS, is a process algebra in which actions consist of sending and receiving values through noiseless communication channels. The full calculus is a succinct yet expressive language for the specification and verification of reactive systems. Taking into account the reality of channel noise in reactive systems, in this paper we introduce an extension of value-passing CCS, called value-passing CCS with noisy channels (VCCSN), in which noise is described by a probability distribution over the values. After presenting the reduction operational semantics and labelled operational semantics of VCCSN, we develop the theory of behavioural equivalence by introducing barbed equivalence, barbed congruence, bisimilarity, and full bisimilarity. In particular, we show that barbed equivalence and barbed congruence coincide with bisimilarity and full bisimilarity, respectively. Based upon the labelled operational semantics of VCCSN, we establish a probabilistic modal logic for expressing system properties and show its connection with the notion of bisimilarity. Finally, we use VCCSN to model a communication protocol for ensuring the reliable transmission of data across an error-prone channel.