A modal interface theory for component-based design. (English) Zbl 1242.68147

Summary: 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.


68Q45 Formal languages and automata
03B45 Modal logic (including the logic of norms)
68Q60 Specification and verification (program logics, model checking, etc.)


Full Text: DOI