The pi-calculus is a development of CCS that has the ability of communicating channel names. The asynchronous pi-calculus is a variant of the pi-calculus where message emission is non-blocking. Finite state verification is problematic in this context, since even very simple asynchronous pi-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 pi-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 pi-processes
Finite State Verification for the Asynchronous pi-Calculus
Pistore, Marco
1999-01-01
Abstract
The pi-calculus is a development of CCS that has the ability of communicating channel names. The asynchronous pi-calculus is a variant of the pi-calculus where message emission is non-blocking. Finite state verification is problematic in this context, since even very simple asynchronous pi-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 pi-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 pi-processesI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
