In this paper an action based logic for the ?-calculus is presented. A model checker is built for this logic following an automata based approach. This is made possible by a result which allows by finite state Labelled Transition Systems to be associated to a wide class of ?-calculus agents so that bisimilar Labelled Transition Systems are associated to bisimilar ?-calculus agents. The model checker has then been built rensing an effincent model checker, that was developed to check the satisfiability of formulae of the action based logic ACTL on finite state Labelled Transition Systems and implementing a sound translation from ?-logic into ACTL
A model checking algorithm for pi-calculus agents
Gnesi S;
1996
Abstract
In this paper an action based logic for the ?-calculus is presented. A model checker is built for this logic following an automata based approach. This is made possible by a result which allows by finite state Labelled Transition Systems to be associated to a wide class of ?-calculus agents so that bisimilar Labelled Transition Systems are associated to bisimilar ?-calculus agents. The model checker has then been built rensing an effincent model checker, that was developed to check the satisfiability of formulae of the action based logic ACTL on finite state Labelled Transition Systems and implementing a sound translation from ?-logic into ACTL| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_408868-doc_143611.pdf
accesso aperto
Descrizione: A model checking algorithm for pi-calculus agents
Dimensione
1.33 MB
Formato
Adobe PDF
|
1.33 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
