We propose a method for the specification and the automated verification of temporal properties of protocols which regulate the activities of multiagent systems. The set of states of those systems may be infinite so that, in general, the verification of a property of a multiagent system cannot be performed by an exhaustive inspection. We specify a given multiagent system by means of a constraint logic program P with locally stratified negation, and we specify a given temporal property to be verified by means of an atomic formula A. In order to verify that the given temporal property holds, we transform the program P into an equivalent program T such that the fact A ← belongs to T. Our transformation method consists of a set of rules and an automatic strategy that guides the application of the rules. Our method is sound for verifying properties of protocols that are expressible in the CTL logic [5]. Although our method is incomplete for proving properties of infinite state systems, it is able to verify important properties of several protocols which are used in practice.

Automatic Proofs of Protocols via Program Transformation.

FIORAVANTI, Fabio;MAURIZIO PROIETTI
2005-01-01

Abstract

We propose a method for the specification and the automated verification of temporal properties of protocols which regulate the activities of multiagent systems. The set of states of those systems may be infinite so that, in general, the verification of a property of a multiagent system cannot be performed by an exhaustive inspection. We specify a given multiagent system by means of a constraint logic program P with locally stratified negation, and we specify a given temporal property to be verified by means of an atomic formula A. In order to verify that the given temporal property holds, we transform the program P into an equivalent program T such that the fact A ← belongs to T. Our transformation method consists of a set of rules and an automatic strategy that guides the application of the rules. Our method is sound for verifying properties of protocols that are expressible in the CTL logic [5]. Although our method is incomplete for proving properties of infinite state systems, it is able to verify important properties of several protocols which are used in practice.
2005
9783540232452
File in questo prodotto:
File Dimensione Formato  
msras_book_2005_proceedings.pdf

Solo gestori archivio

Tipologia: Documento in Post-print
Dimensione 996.04 kB
Formato Adobe PDF
996.04 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11564/104533
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact