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 |

1) Download Document PDF |

Open access Restricted Private