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.© Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Fioravanti, F., Pettorossi, A., & Proietti, M. (2005). Automatic proofs of protocols via program transformation. In Advances in Soft Computing (Vol. 28, pp. 99–116). Springer Verlag. https://doi.org/10.1007/3-540-32370-8_7
Mendeley helps you to discover research relevant for your work.