An operational semantics for a calculus for wireless systems

In wireless systems, the communication mechanism combines features of broadcast, synchrony, and asynchrony. We develop an operational semantics for a calculus of wireless systems. We present different Reduction Semantics and a Labelled Transition Semantics and prove correspondence results between them. Finally, we apply CWS to the modelling of the Alternating Bit Protocol, and prove a simple correctness result as an example of the kind of properties that can be formalized in this framework.A major goal of the semantics is to describe the forms of interference among the activities of processes that are peculiar of wireless systems. Such interference occurs when a location is simultaneously reached by two transmissions. The Reduction Semantics differ on how information about the active transmissions is managed.We use the calculus to describe and analyse a few properties of a version of the Alternating Bit Protocol.