Analyzing distributed pi-calculus systems by using the rewriting engine Maude

Abstract

Distributed systems with explicit locations and process mobility are described in terms of the distributed π -calculus. The systems described in distributed π -calculus are translated into a rewriting logic which is executable on the Maude software platform. We prove an operational correspondence allowing to verify properly the properties of the distributed systems. The approach is illustrated by examples of distributed systems analyzed by using the powerful Maude platform. We verify whether some systems are behaviourally equivalent by involving the metalevels of Maude.