Responsive Choice in Mobile Processes

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

4 Citations (Scopus)


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) andresponsiveness(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 usebranchingandselectionto capture activeness and responsiveness in process constructs necessary for such usage patterns. Secondly,conditional propertiesoffercompositionalityfeatures that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.
Original languageUnknown
Title of host publicationLecture Notes in Computer Science
EditorsMartin Wirsing Martin Hofmann, A Rauschmayer
ISBN (Print)978-3-642-15640-3
Publication statusPublished - 1 Jan 2010
EventTrustworthly Global Computing (TGC) -
Duration: 1 Jan 2010 → …


ConferenceTrustworthly Global Computing (TGC)
Period1/01/10 → …

Cite this