PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Gnesi S., Ristori G. A model checking algorithm for pi-calculus agents. Internal note IEI-B4-25, 1996.
 
 
Abstract
(English)
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
Subject Model checking algorithm


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional