Temporal Logics for Representing Agent Communication Protocols

  • Ulle Endriss
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3859)


This paper explores the use of temporal logics in the context of communication protocols for multiagent systems. We concentrate on frameworks where protocols are used to specify the conventions of social interaction, rather than making reference to the mental states of agents. Model checking can be used to check the conformance of a given dialogue between agents to a given protocol expressed in a suitable temporal logic. We begin by showing how simple protocols, such as those typically presented as finite automata, can be specified using a fragment of propositional linear temporal logic. The full logic can also express concepts such as future dialogue obligations (or commitments). Finally, we discuss how an extended temporal logic based on ordered trees can be used to specify nested protocols.


Model Check Temporal Logic Multiagent System Agent Communication Model Check Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Ulle Endriss
    • 1
  1. 1.Institute for Logic, Language and ComputationUniversity of AmsterdamAmsterdamThe Netherlands

Personalised recommendations