This paper presents ?-logic, an action-based logic for ?-calculus. A model checker is built for this logic, following an automata-based approach. This is made possible by a result which allows finite state Labelled Transition Systems to be associated with a wide class of 7r-calculus agents by preserving a notion of bisimulation equivalence. The model checker was thus built reusing an efficient model checker for the action based logic ACTL, after a sound translation from 7r-logic into ACTL has been defined.
A model checking algorithm for pi-calculus agents
Gnesi S;
2000
Abstract
This paper presents ?-logic, an action-based logic for ?-calculus. A model checker is built for this logic, following an automata-based approach. This is made possible by a result which allows finite state Labelled Transition Systems to be associated with a wide class of 7r-calculus agents by preserving a notion of bisimulation equivalence. The model checker was thus built reusing an efficient model checker for the action based logic ACTL, after a sound translation from 7r-logic into ACTL has been defined.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_406489-doc_142184.pdf
solo utenti autorizzati
Descrizione: A model checking algorithm for pi-calculus agents
Tipologia:
Versione Editoriale (PDF)
Dimensione
1.31 MB
Formato
Adobe PDF
|
1.31 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
