This paper considers the problems associated with the composition of modal interface automata. A modal interface automaton (MIA) has both must transitions, which specify that a transition lands in one of a finite number of states, and may transitions, where the transition moves to a single well-defined state. A set of MIAs can be used to specify the behavior of a system with the overall behavior being the conjunction of the specifying MIAs.

Lüttgen et al. give an enlightening example of a waiter in a restaurant whose behavior is a conjunction of the interaction with customers and the interaction with the kitchen. A major issue in describing the conjunction of two MIAs occurs when one interface can produce an output that is not accepted by the other one: for example, the waiter interface responds to a customer request with something that the kitchen interface cannot process. Two approaches have been used to handle this situation. In one case, the optimistic one, the assumption is made that the input producing the offending output will not occur. In the pessimistic case, the two interfaces are considered to be incompatible. This paper shows how to modify previous work on the optimistic case to handle internal computations that lead to must transitions. In the pessimistic non-deterministic case, the authors show how to define conjunction and disjunction for interfaces.

The paper provides complete details of the authors’ approach and should be of interest to those engaged in the specification of system interactions.