Finite state verification for the asynchronous π-calculus

Abstract

The π-calculus is a development of CCS that has the ability of communicating channel names. The asynchronous π-calculus is a variant of the π-calculus where message emission is non-blocking. Finite state verification is problematic in this context, since even very simple asynchronous π-processes give rise to infinite-state behaviors. This is due to phenomena that are typical of calculi with name passing and to phenomena that are peculiar of asynchronous calculi. We present a finite-state characterization of a family of finitary asynchronous π-processes by exploiting History Dependent transition systems with Negative transitions (HDN), an extension of labelled transition systems particularly suited for dealing with concurrent calculi with name passing. We also propose an algorithm based on HDN to verify asynchronous bisimulation for finitary π-processes.