Theorem proving for protocol languages

Robbert L. Brak, Jacques D. Fleuriot, Jarred Mcginnis

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We make a case for more rigour in the development of agent protocol languages, by examining the implementation of the logic-based protocol language ANML in the theorem prover Isabelle. However, the problems encountered in the formalization process were found to be insurmountable. As an alternative, we develop ANML2 as a rigourously formalized protocol language based on the same principles as ANML. We show how to formulate termination and consistency properties for specific protocols within the ANML2 framework and prove them in Isabelle.
Original languageEnglish
Title of host publicationProceedings of the Second European Workshop on Multi-Agent Systems (EUMAS 2004)
Publication statusPublished - 2004


Dive into the research topics of 'Theorem proving for protocol languages'. Together they form a unique fingerprint.

Cite this