Making the Unobservable, Unobservable

Behavioural equivalences of various calculi for modelling distributed systems differ significantly because the properties which can be observed through interaction depend heavily upon their mode of communication. A typical approach to describing the semantics of communicating processes is to provide a labelled transition system (lts) which captures the interaction potential of the individual processes within a larger system. In many cases, a natural rendering of this lts leads to too fine a semantics as unobservability of certain communications is not accounted for.We propose that a standard approach to augmenting ltss allows morally unobservable communications to actually be modelled as unobservables in the semantics. This approach derives from a rule initially given by Honda and Tokoro to account for unobservability of reception in the asynchronous π-calculus. We examine the implications of adding such rules to lts with respect to the proving behavioural equivalences for various synchronisation mechanisms