Now it appears convenient to formally capture the conceptual model introduced above to be able to reason, later on, about the properties that we must demand from CPs. Therefore, formally we define a conversation protocol as an 8-tuple :

such that:

- is a finite set of state symbols that represent the states of the finite state control.
- is a finite alphabet formed by the identifiers of all performatives that can be uttered during the conversation.
- is a finite input list alphabet composed of the identifiers of all predicates recognized by the speakers.
- is the finite pushdown list alphabet.
- is a mapping from to the finite subsets of which indicates all possible transitions that can take place during a conversation.
- is the initial state of a conversation.
- is the start symbol of the pushdown list.
- is the set of final states representing possible final states of a conversation.

CPs only contemplate a finite number of moves from each state that must belong to one of the following types:

Wed Mar 10 11:44:57 MET 1999