Publication Type:

Journal Article


Science of Computer Programming, Volume 78, Number 9, p.1470-1489 (2013)



Abstract types, Bisimilarity, Calculations, Carrier mobility, Process algebras, Semantics, Specification languages, Stateful channel, Z language


We investigate a principled extension of the π-calculus for formal modeling of mobile communicating systems with stateful channels. In our proposed extension, called πZ, a channel is associated with a stateful abstract type in the Z specification language. We develop both reduction as well as labeled transition semantics for πZ. We show that the important properties of the π-calculus are preserved in πZ: (1) τ-transitions match reductions; and (2) bisimilarity induced by the labeled transitions is closed under parallel composition, name restriction, and a restricted recursion. The paper illustrates the use of stateful channels by modeling the 'hidden node problem' in a wireless network. © 2012 Elsevier B.V. All rights reserved.


cited By (since 1996)0

Cite this Research Publication

Ja Poroor and Jayaraman, Bb, “Modeling mobile stateful channels in πz”, Science of Computer Programming, vol. 78, pp. 1470-1489, 2013.