Verifiable agent dialogues

In the first half of the paper we specify the syntax of MAP, together with an operational semantics that defines an abstract implementation of the language. Our specification is derived from process calculus and thus forms a sound basis for the verification of our protocols. We also sketch a connection between MAP and temporal logic. In the latter half of the paper we define a translation from MAP into PROMELA which is the specification language of the SPIN model checker. This translation allows us to prove properties of our protocols, such as termination, liveness, and correctness. The verification process is defined by P⊨φ, where P is our translated agent protocol, and φ is a linear temporal logic formula. By performing model checking on our protocols we can obtain a high degree of confidence in the resulting agent dialogues.