Modal Interface Automata

De Alfaro and Henzinger's Interface Automata (IA) and Nyman et al.'s recentcombination IOMTS of IA and Larsen's Modal Transition Systems (MTS) areestablished frameworks for specifying interfaces of system components. However,neither IA nor IOMTS consider conjunction that is needed in practice when acomponent shall satisfy multiple interfaces, while Larsen's MTS-conjunction isnot closed and Bene\v{s} et al.'s conjunction on disjunctive MTS does not treatinternal transitions. In addition, IOMTS-parallel composition exhibits acompositionality defect. This article defines conjunction (and alsodisjunction) on IA and disjunctive MTS and proves the operators to be'correct', i.e., the greatest lower bounds (least upper bounds) wrt. IA- andresp. MTS-refinement. As its main contribution, a novel interface theory calledModal Interface Automata (MIA) is introduced: MIA is a rich subset of IOMTSfeaturing explicit output-must-transitions while input-transitions are alwaysallowed implicitly, is equipped with compositional parallel, conjunction anddisjunction operators, and allows a simpler embedding of IA than Nyman's. Thus,it fixes the shortcomings of related work, without restricting designers todeterministic interfaces as Raclet et al.'s modal interface theory does.Comment: 28 page