A modal interface theory for component-based design.

*(English)*Zbl 1242.68147Summary: This paper presents the modal interface theory, a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model which allows the designer to express assumptions on the environment and which uses an optimistic view of composition: two components can be composed if there is an environment where they can work together. Modal specifications are a language-theoretic account of a fragment of the modal mu-calculus with a rich composition algebra, which meets certain methodological requirements but which does not allow the environment and the component to be distinguished. The present paper contributes a more thorough unification of the two theories by correcting a first attempt in this direction by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing the comparison between interface automata, modal automata and modal interfaces even further.

##### MSC:

68Q45 | Formal languages and automata |

03B45 | Modal logic (including the logic of norms) |

68Q60 | Specification and verification (program logics, model checking, etc.) |