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

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-processes
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/1825
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact