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.
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