Responsive Choice in Mobile Processes

We propose a general type notation, formal semantics and a sound, compositional, and decidable type system to characterise some liveness properties of distributed systems. In the context of mobile processes, we define two concepts, activeness (ability to send/receive on a channel) and responsiveness (ability to reliably conduct a conversation on a channel), that make the above properties precise. The type system respects the semantic definitions of the concepts, in the sense that the logical statements it outputs are, according to the semantics, correct descriptions of the analysed process. Our work is novel in two aspects. First, since mobile processes can make and communicate choices, a fundamental component of data representation (where a piece of data matches one of a set of patterns) or conversations (where the protocol may permit more than one message at each point), our types and type system use branching and selection to capture activeness and responsiveness in process constructs necessary for such usage patterns. Secondly, conditional properties offer compositionality features that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.