---
abstract: |
    De Alfaro and Henzinger’s Interface Automata (IA) and Nyman et al.’s recent combination IOMTS of IA and Larsen’s Modal Transition Systems (MTS) are established frameworks for specifying interfaces of system components. However, neither IA nor IOMTS consider conjunction that is needed in practice when a component shall satisfy multiple interfaces, while Larsen’s MTS-conjunction is not closed and Beneš et al.’s conjunction on disjunctive MTS does not treat internal transitions. In addition, IOMTS-parallel composition exhibits a compositionality defect.

    This article defines conjunction (and also disjunction) on IA and disjunctive MTS and proves the operators to be ‘correct’, i.e., the greatest lower bounds (least upper bounds) wrt. IA- and resp. MTS-refinement. As its main contribution, a novel interface theory called Modal Interface Automata (MIA) is introduced: MIA is a rich subset of IOMTS featuring explicit output-must-transitions while input-transitions are always allowed implicitly, is equipped with compositional parallel, conjunction and disjunction operators, and allows a simpler embedding of IA than Nyman’s. Thus, it fixes the shortcomings of related work, without restricting designers to deterministic interfaces as Raclet et al.’s modal interface theory does.
address:
- '[a]{}Software Technologies Research Group, University of Bamberg, 96045 Bamberg, Germany'
- '[b]{}Institute for Computer Science, University of Augsburg, 86135 Augsburg, Germany'
author:
- 'Gerald L[ü]{}ttgena'
- Walter Voglerb
bibliography:
- 'literature.bib'
title: Modal Interface Automata
---

Introduction {#sec:introduction}
============

Interfaces play an important role when designing complex software and hardware systems so as to be able to check interoperability of system components already at design stage. Early interface theories deal with types of data and operations only and have been successfully deployed in compilers. Over the past two decades, research has focused on more advanced interface theories for *sequential* and object-oriented software systems, where interfaces also comprise behavioural types. Such types are often referred to as *contracts* [@Mey92] and can express pre- and post-conditions and invariants of methods and classes. Much progress has been made on the design of contract languages and on automated verification techniques that can decide whether a system component meets its contract (cf. [@HatLeaLeinMuePar2012] for a survey).

More recently, *behavioural interfaces* have also been proposed and are being investigated for the use in *concurrent* systems, with prominent application examples being embedded systems (e.g., [@MayGru2005]) and web services (e.g., [@BeyChaHenSes2007; @MerBjo2003]). In this context, behavioural interfaces are intended to capture protocol aspects of component interaction. One prominent example of such an interface theory is de Alfaro and Henzinger’s *Interface Automata* (IA) [@DeAHen2001; @DeAHen2005], which is based on labelled transition systems (LTS) but distinguishes a component’s input and output actions. The theory comes with an asymmetric parallel composition operator, where a component may wait on inputs but never on outputs. Thus, a component’s output must be consumed immediately, or an error occurs. In case no potential system environment may restrict the system components’ behaviour so that all errors are avoided, the components are deemed to be incompatible.

Semantically, IA employs a refinement notion based on an alternating simulation, such that a component satisfies an interface if (a) it implements all input behaviour prescribed by the interface and (b) the interface permits all output behaviour executed by the implementing component. Accordingly and surprisingly, an output in a specification can always be ignored in an implementation. In particular, a component that consumes all inputs but never produces any output satisfies any interface. Since a specifier certainly wants to be able to prescribe at least some outputs, Larsen, Nyman and Wasowski have built their interface theory on Modal Transition Systems (MTS) [@Lar89] rather than LTS, which enables one to distinguish between may- and must-transitions and thus to express mandatory outputs. The resulting *IOMTS* interface theory [@LarNymWas2007], into which IA can be embedded, is equipped with an IA-style parallel composition and an MTS-style modal refinement. Unfortunately, IOMTS-modal refinement is not a precongruence (i.e., not compositional) for parallel composition; a related result in [@LarNymWas2007] has already been shown incorrect by Raclet et al. in [@RacBadBenCaiLegPas2011].

The present article starts from the observation that the above interface theories are missing one important operator, namely conjunction on interfaces. Conjunction is needed in practice since components are often designed to satisfy multiple interfaces simultaneously, each of which specifies a particular aspect of component interaction. Indeed, conjunction is a key operator when specifying and developing systems from different viewpoints as is common in modern software engineering. We thus start off by recalling the IA-setting and defining a conjunction operator ${\wedge}$ for IA; we prove that ${\wedge}$ is indeed conjunction, i.e., the greatest lower bound wrt. alternating simulation (cf. Sec. \[sec:ia\]). Essentially the same operator has recently and independently been defined in [@CheChiJonKwi2012], where it is shown that it gives the greatest lower bound wrt. a *trace-based* refinement relation. As an aside, we also develop and investigate the dual disjunction operator ${\vee}$ for IA. This is a natural operator for describing alternatives in loose specifications, thus leaving implementation decisions to implementors.

Similarly, we define conjunction and disjunction operators for a slight extension of MTS (a subset of *Disjunctive MTS* [@LarXin90], cf. Sec. \[sec:dmts\]), which paves us the way for our main contribution outlined below. Although Larsen has already studied conjunction and disjunction for MTS, his operators do, in contrast to ours, not preserve the MTS-property of syntactic consistency, i.e., a conjunction or disjunction almost always has some required transitions (must-transitions) that are not allowed (missing may-transitions). An additional difficulty when compared to the IA-setting is that two MTS-interfaces may not have a common implementation; indeed, inconsistencies may arise when composing MTSs conjunctively. We handle inconsistencies in a two-stage definition of conjunction, adapting ideas from our prior work on conjunction in a CSP-style process algebra [@LueVog2010] that uses, however, a very different parallel operator and refinement preorder. In [@BenCerKre2011], a conjunction for Disjunctive MTS (DMTS) is introduced in a two-stage style, too. Our construction and results for conjunction significantly extend the ones of [@BenCerKre2011] in that we also treat internal transitions that, e.g., result from communication.

Note also that our setting employs event-based communication via handshake and thus differs substantially from the one of shared-memory communication studied by Abadi and Lamport in their paper on conjoining specifications [@AbaLam95]. The same comment applies to Doyen et al. [@DoyHenJobPet2008], who have studied a conjunction operator for an interface theory involving shared-variable communication.

Our article’s main contribution is a novel interface theory, called *Modal Interface Automata* (MIA), which is essentially a rich subset of IOMTS that still allows one to express output-must-transitions. In contrast to IOMTS, must-transitions can also be disjunctive, and input-transitions are either required (i.e., must-transitions) or allowed implicitly. MIA is equipped with an MTS-style conjunction ${\wedge}$, disjunction ${\vee}$ and an IOMTS-style parallel composition operator, as well as with a slight adaptation of IOMTS-refinement. We show that (i) MIA-refinement is a precongruence for all three operators; (ii) ${\wedge}$ (${\vee}$) is indeed conjunction (disjunction) for this preorder; and (iii) IA can be embedded into MIA in a much cleaner, homomorphic fashion than into IOMTS [@LarNymWas2007] (cf. Sec. \[sec:mia\]). Thereby, we remedy the shortcomings of related work while, unlike the language-based modal interface theory of [@RacBadBenCaiLegPas2011], still permitting nondeterminism in specifications.

Conjunction and Disjunction for Interface Automata {#sec:ia}
==================================================

*Interface Automata* (IA) were introduced by de Alfaro and Henzinger [@DeAHen2001; @DeAHen2005] as a *reactive type* theory that abstractly describes the communication behaviour of software or hardware components in terms of their inputs and outputs. IAs are labelled transition systems where visible actions are partitioned into inputs and outputs. The idea is that interfaces interact with their environment according to the following rules. An interface cannot block an incoming input in any state but, if an input arrives unexpectedly, it is treated as a catastrophic system failure. This means that, if a state does not enable an input, this is a requirement on the environment not to produce this input. Vice versa, an interface guarantees not to produce any unspecified outputs, which are in turn inputs to the environment.

This intuition is reflected in the specific refinement relation of *alternating simulation* between IA and in the *parallel composition* on IA, which have been defined in [@DeAHen2005] and are recalled in this section. Most importantly, however, we introduce and study a *conjunction operator* on IA, which is needed in practice to reason about components that are expected to satisfy multiple interfaces.

An *Interface Automaton* (IA) is a tuple $Q = (Q, I, O,
  {\stackrel{}{\longrightarrow}})$, where

(1) $Q$ is a set of states,

(2) $I$ and $O$ are disjoint input and output alphabets, resp., not containing the special, silent action $\tau$,

(3) ${\stackrel{}{\longrightarrow}} \,\subseteq Q \times (I \cup O \cup \{\tau\})
        \times Q$ is the *transition relation*.

The transition relation is required to be *input-deterministic*, i.e., $a \in I$, $q {\stackrel{a}{\longrightarrow}} q'$ and $q {\stackrel{a}{\longrightarrow}} q''$ implies $q' = q''$. In the remainder, we write $q \!{\stackrel{a}{\longrightarrow}}$ if $q {\stackrel{a}{\longrightarrow}} q'$ for some $q'$, as well as $q
  \,\not\!{\stackrel{a}{\longrightarrow}}$ for its negation. \[def:ia\]

In contrast to [@DeAHen2005] we do not distinguish internal actions and denote them all by $\tau$, as is often done in process algebras. We let $A$ stand for $I \cup O$, let $a$ ($\alpha$) range over $A$ ($A
\cup \{\tau\}$), and introduce the following weak transition relations: $q {\stackrel{{\varepsilon}}{\Longrightarrow}} q'$ if $q ({\stackrel{\tau}{\longrightarrow}})^{\ast}
q'$, and $q {\stackrel{o}{\Longrightarrow}} q'$ for $o \in O$ if $\exists q''.\, q
{\stackrel{{\varepsilon}}{\Longrightarrow}} q'' {\stackrel{o}{\longrightarrow}} q'$; note that there are no $\tau$-transitions after the $o$-transition. Moreover, we define $\hat{\alpha} = {\varepsilon}$ if $\alpha = \tau$, and $\hat{\alpha} =
\alpha$ otherwise.

Let $P$ and $Q$ be IAs with common input and output alphabets. Relation ${\mathcal{R}} \subseteq P \times Q$ is an *alternating simulation relation* if for all ${({p},{q})} \in {\mathcal{R}}$:

1.  $q {\stackrel{a}{\longrightarrow}} q'$ and $a \in I$ implies $\exists p'.\, p
        {\stackrel{a}{\longrightarrow}} p'$ and ${({p'},{q'})} \in {\mathcal{R}}$,

2.  $p {\stackrel{\alpha}{\longrightarrow}} p'$ and $\alpha \in O \cup \{\tau\}$ implies $\exists q'.\, q {\stackrel{\hat{\alpha}}{\Longrightarrow}} q'$ and ${({p'},{q'})} \in {\mathcal{R}}$.

We write $p {\sqsubseteq_{\textrm{IA}}}q$ and say that $p$ *IA-refines* $q$ if there exists an alternating simulation relation ${\mathcal{R}}$ such that ${({p},{q})} \in {\mathcal{R}}$. \[def:iasim\]

According to the basic idea of IA, if specification $Q$ in state $q$ allows some input $a$ delivered by the environment, then the related implementation state $p$ of $P$ must allow this input immediately in order to avoid system failure. Conversely, if $P$ in state $p$ produces output $a$ to be consumed by the environment, this output must be expected by the environment even if $q {\stackrel{a}{\Longrightarrow}}$; this is because $Q$ could have moved unobservedly from state $q$ to some $q'$ that enables $a$. Since inputs are not treated in Def. \[def:iasim\] (ii), they are always allowed for $p$.

It is easy to see that IA-refinement ${\sqsubseteq_{\textrm{IA}}}$ is a preorder on IA and the largest alternating simulation relation. Given input and output alphabets $I$ and $O$, resp., the IA $$\textit{BlackHole}_{I,O} \,{=_{\text{df}}}\, (\{ \textit{blackhole} \}, I, O, \{
  (\textit{blackhole},a,\textit{blackhole}) \;|\; a \in I \})$$ IA-refines any other IA over $I$ and $O$.

Conjunction on IA {#subsec:iaconj}
-----------------

Two IAs with common alphabets are always logically consistent in the sense that they have a common implementation, e.g., the respective blackhole IA as noted above. This makes the definition of conjunction on IA relatively straightforward. Here and similarly later, we index a transition by the system’s name to make clear from where it originates, in case this is not obvious from the context.

Let $P = (P, I, O, {\stackrel{}{\longrightarrow}}_P)$ and $Q = (Q, I,$ $O,
  {\stackrel{}{\longrightarrow}}_Q)$ be IAs with common input and output alphabets and disjoint state sets $P$ and $Q$. The conjunction $P {\wedge}Q$ is defined by $(\{ p {\wedge}q \;|\; p \in P,\, q \in Q \} \cup P \cup
  Q, I, O, {\stackrel{}{\longrightarrow}})$, where ${\stackrel{}{\longrightarrow}}$ is the least set satisfying ${\stackrel{}{\longrightarrow}}_P \subseteq {\stackrel{}{\longrightarrow}}$, ${\stackrel{}{\longrightarrow}}_Q
  \subseteq {\stackrel{}{\longrightarrow}}$, and the following operational rules:

  ---------- --------------------------------------------------------------- ---- -------------------------------------------------------------------------------------------------------
  [(I1)]{}   $p {\wedge}q {\stackrel{a}{\longrightarrow}} p'$                if   $p {\stackrel{a}{\longrightarrow}}_P p'$, $q \,\not\!{\stackrel{a}{\longrightarrow}}_Q$ and $a \in I$
  [(I2)]{}   $p {\wedge}q {\stackrel{a}{\longrightarrow}} q'$                if   $p \,\not\!{\stackrel{a}{\longrightarrow}}_P$, $q {\stackrel{a}{\longrightarrow}}_Q q'$ and $a \in I$
  [(I3)]{}   $p {\wedge}q {\stackrel{a}{\longrightarrow}} p' {\wedge}q'$     if   $p {\stackrel{a}{\longrightarrow}}_P p'$, $q {\stackrel{a}{\longrightarrow}}_Q q'$ and $a \in I$
  [(O)]{}    $p {\wedge}q {\stackrel{a}{\longrightarrow}} p' {\wedge}q'$     if   $p {\stackrel{a}{\longrightarrow}}_P p'$, $q {\stackrel{a}{\longrightarrow}}_Q q'$ and $a \in O$
  [(T1)]{}   $p {\wedge}q {\stackrel{\tau}{\longrightarrow}} p' {\wedge}q$   if   $p {\stackrel{\tau}{\longrightarrow}}_P p'$
  [(T2)]{}   $p {\wedge}q {\stackrel{\tau}{\longrightarrow}} p {\wedge}q'$   if   $q {\stackrel{\tau}{\longrightarrow}}_Q q'$
  ---------- --------------------------------------------------------------- ---- -------------------------------------------------------------------------------------------------------

\[def:iaandop\]

![Example illustrating IA-conjunction.[]{data-label="fig:iaandopex"}](iaandopex.png)

Intuitively, conjunction is the synchronous product over actions (cf. Rules (I3), (O), (T1) and (T2)). Since inputs are always implicitly present, this also explains Rules (I1) and (I2); for example, in Rule (I1), $q$ does not impose any restrictions on the behaviour after input $a$ and is therefore dropped from the target state. Moreover, the conjunction operator is commutative and associative. As an aside, note that the rules with digit 2 in their names are the symmetric cases of the respective rules with digit 1; this convention will hold true throughout this article. Fig. \[fig:iaandopex\] applies the rules above to an illustrating example; here and in the following figures, we write $a?$ for an input $a$ and $a!$ for an output $a$.

Essentially the same conjunction operator is defined by Chen et al. in [@CheChiJonKwi2012], where a non-standard variant of IA is studied that employs *explicit* error states and uses a trace-based semantics and refinement preorder (going back to Dill [@Dil89]). The difference between their conjunction and Def. \[def:iaandop\] is that error states are explicitly used in the clauses that correspond to Rules (I1) and (I2) above, which renders our definition arguably more elegant. In [@CheChiJonKwi2012], an analogue theorem to Thm. \[thm:iaandisand\] below is shown, but its statement is different as it refers to a different refinement preorder. Also note that, deviating from the IA-literature, error states are called inconsistent in [@CheChiJonKwi2012], but this is not related to logic inconsistency as studied by us.

Our first result states that an implementation satisfies the conjunction of interfaces exactly if it satisfies each of them. This is a desired property in system design where each interface describes one aspect (or view) of the overall specification.

Let $P, Q, R$ be IAs with states $p$, $q$, $r$, resp. Then, $r {\sqsubseteq_{\textrm{IA}}}p$ and $r {\sqsubseteq_{\textrm{IA}}}q$ if and only if $r {\sqsubseteq_{\textrm{IA}}}p
  {\wedge}q$. \[thm:iaandisand\]

Technically, this result states that ${\wedge}$ gives the greatest lower-bound wrt. ${\sqsubseteq_{\textrm{IA}}}$ (up to equivalence), and its proof uses the input-determinism property of IA. The theorem also implies compositional reasoning; from universal algebra one easily gets:

For IAs $P, Q, R$ with states $p$, $q$ and $r$: $\,p {\sqsubseteq_{\textrm{IA}}}q$ $\;\Longrightarrow\;$ $p {\wedge}r{\sqsubseteq_{\textrm{IA}}}q {\wedge}r$. \[cor:iaandopcomp\]

Disjunction on IA {#subsec:iadisj}
-----------------

In analogy to conjunction we develop a disjunction operator on IA and discuss its properties; in particular, this operator should give the least upper bound.

Let $P = (P, I, O, {\stackrel{}{\longrightarrow}}_P)$ and $Q = (Q, I,$ $O,
  {\stackrel{}{\longrightarrow}}_Q)$ be IAs with common input and output alphabets and disjoint state sets $P$ and $Q$. The disjunction $P {\vee}Q$ is defined by $(\{ p {\vee}q \;|\; p \in P,\, q \in Q \} \cup P \cup Q,
  I, O, {\stackrel{}{\longrightarrow}})$, where ${\stackrel{}{\longrightarrow}}$ is the least set satisfying ${\stackrel{}{\longrightarrow}}_P \subseteq {\stackrel{}{\longrightarrow}}$, ${\stackrel{}{\longrightarrow}}_Q \subseteq
  {\stackrel{}{\longrightarrow}}$ and the following operational rules:

  ----------- --------------------------------------------------------- ---- --------------------------------------------------------------------------------------------------
  [(I)]{}     $p {\vee}q {\stackrel{a}{\longrightarrow}} p' {\vee}q'$   if   $p {\stackrel{a}{\longrightarrow}}_P p'$, $q {\stackrel{a}{\longrightarrow}}_Q q'$ and $a \in I$
  [(OT1)]{}   $p {\vee}q {\stackrel{\alpha}{\longrightarrow}} p'$       if   $p {\stackrel{\alpha}{\longrightarrow}}_P p'$ and $\alpha \in O \cup \{\tau\}$
  [(OT2)]{}   $p {\vee}q {\stackrel{\alpha}{\longrightarrow}} q'$       if   $q {\stackrel{\alpha}{\longrightarrow}}_Q q'$ and $\alpha \in O \cup \{\tau\}$
  ----------- --------------------------------------------------------- ---- --------------------------------------------------------------------------------------------------

\[def:iaorop\]

Note that this definition preserves the input-determinism required of IA. The definition is roughly dual to the one of IA-conjunction, i.e., we take the ‘intersection’ of initial input behaviour and the ‘union’ of initial output behaviour. Strictly speaking, this would require the following additional rule for outputs $o \in O$:

  ---------- --------------------------------------------------------- ---- ---------------------------------------------------------------------------------------
  [(O3)]{}   $p {\vee}q {\stackrel{o}{\longrightarrow}} p' {\vee}q'$   if   $p {\stackrel{o}{\longrightarrow}}_P p'$ and $q {\stackrel{o}{\longrightarrow}}_Q q'$
  ---------- --------------------------------------------------------- ---- ---------------------------------------------------------------------------------------

However, the addition of this rule would in general result in disjunctions $p {\vee}q$ that are larger than the least upper bound of $p$ and $q$ wrt. ${\sqsubseteq_{\textrm{IA}}}$. The following theorem shows that our ${\vee}$-operator properly characterizes the least upper bound:

Let $P, Q, R$ be IAs with states $p$, $q$ and $r$, resp. Then, $p
  {\vee}q {\sqsubseteq_{\textrm{IA}}}r$ if and only if $p {\sqsubseteq_{\textrm{IA}}}r$ and $q {\sqsubseteq_{\textrm{IA}}}r$. \[thm:iaorisor\]

Compositionality of disjunction can now be derived dually to the proof of Corollary \[cor:iaandopcomp\] but using Thm. \[thm:iaorisor\] instead of Thm. \[thm:iaandisand\]:

For IAs $P, Q, R$ with states $p$, $q$ and $r$: $\,p {\sqsubseteq_{\textrm{IA}}}q$ $\;\Longrightarrow\;$ $p {\vee}r{\sqsubseteq_{\textrm{IA}}}q {\vee}r$. \[cor:iaoropcomp\]

![Example illustrating IA-disjunction’s different treatment of inputs and outputs.[]{data-label="fig:iaoropex"}](iaoropex.png)

The two examples of Fig. \[fig:iaoropex\] round off our investigation of IA disjunction by illustrating the operator’s different treatment of inputs and outputs. Regarding $p {\vee}q$ on the figure’s left-hand side, the choice of which disjunct to implement is taken with the first action $o \in O$ if both disjuncts are implemented; this meets the intuition of an inclusive-or. In the analogous situation of $r {\vee}s$ on the figure’s right-hand side, a branching on $i \in I$ is not allowed due to input-determinism, and the resulting IA is thus intuitively unsatisfactory. The root cause for this is that the IA-setting does not include sufficiently many automata and, therefore, the least upper bound is ‘too large’. The shortcoming can be remedied by introducing disjunctive transitions, as we will do below in the dMTS- and MIA-settings. Then, we will have more automata and, indeed, will get a smaller least upper bound.\[fromtena\]

Parallel Composition on IA {#subsec:iaparop}
--------------------------

We recall the parallel composition operator ${|}$ on IA of [@DeAHen2005], which is defined in two stages: first a standard product ${\otimes}$ between two IAs is introduced, where common actions are synchronized and hidden. Then, error states are identified, and all states are pruned from which reaching an error state is unavoidable.

IAs $P_1$ and $P_2$ are called *composable* if $A_1 \cap A_2 =
  (I_1 \cap O_2) \cup (O_1 \cap I_2)$, i.e., each common action is input of one IA and output of the other IA. For such IAs we define the *product* $P_1 {\otimes}P_2 = (P_1 \times P_2, I, O,
  {\stackrel{}{\longrightarrow}})$, where $I = (I_1 \cup I_2) \setminus (O_1 \cup O_2)$ and $O = (O_1 \cup O_2) \setminus (I_1 \cup I_2)$ and where ${\stackrel{}{\longrightarrow}}$ is given by the following operational rules:

  ------------ ------------------------------------------------------------------------- ---- ---------------------------------------------------------------------------------------------------------
  [(Par1)]{}   ${({p_1},{p_2})} {\stackrel{\alpha}{\longrightarrow}} {({p'_1},{p_2})}$   if   $p_1 {\stackrel{\alpha}{\longrightarrow}} p'_1$ and $\alpha \notin A_2$
  [(Par2)]{}   ${({p_1},{p_2})} {\stackrel{\alpha}{\longrightarrow}} {({p_1},{p'_2})}$   if   $p_2 {\stackrel{\alpha}{\longrightarrow}} p'_2$ and $\alpha \notin A_1$
  [(Par3)]{}   ${({p_1},{p_2})} {\stackrel{\tau}{\longrightarrow}} {({p'_1},{p'_2})}$    if   $p_1 {\stackrel{a}{\longrightarrow}} p'_1$ and $p_2 {\stackrel{a}{\longrightarrow}} p'_2$ for some $a$.
  ------------ ------------------------------------------------------------------------- ---- ---------------------------------------------------------------------------------------------------------

\[def:iaparprod\]

Note that, in case of synchronization and according to Rule (Par3), one only gets internal $\tau$-transitions.

A state ${({p_1},{p_2})}$ of a parallel product $P_1 {\otimes}P_2$ is an *error state* if there is some $a \in A_1 \cap A_2$ such that (a) $a \in O_1$, $p_1 \!{\stackrel{a}{\longrightarrow}}$ and $p_2
  \,\not\!{\stackrel{a}{\longrightarrow}}$, or (b) $a \in O_2$, $p_2 \!{\stackrel{a}{\longrightarrow}}$ and $p_1 \,\not\!{\stackrel{a}{\longrightarrow}}$.

A state of $P_1 {\otimes}P_2$ is *incompatible* if it may reach an error state autonomously, i.e., only by output or internal actions that are, intuitively, locally controlled. Formally, the set $E \subseteq P_1 \times P_2$ of incompatible states is the least set such that ${({p_1},{p_2})} \in E$ if (i) ${({p_1},{p_2})}$ is an error state or (ii) ${({p_1},{p_2})} {\stackrel{\alpha}{\longrightarrow}}
  {({p'_1},{p'_2})}$ for some $\alpha \in O \cup \{\tau\}$ and ${({p'_1},{p'_2})} \in E$.

The *parallel composition* $P_1 {|}P_2$ of $P_1, P_2$ is obtained from $P_1 {\otimes}P_2$ by *pruning*, i.e., removing all states in $E$ and all transitions involving such states as source or target. If ${({p_1},{p_2})} \in P_1 {|}P_2$, we write $p_1
  {|}p_2$ and call $p_1$ and $p_2$ *compatible*. \[def:iaparop\]

Parallel composition is well-defined since input-determinism is preserved.

Let $P_1$, $P_2$ and $Q_1$ be IAs with $p_1 \in P_1$, $p_2 \in P_2$, $q_1 \in Q_1$ and $p_1 {\sqsubseteq_{\textrm{IA}}}q_1$. Assume that $Q_1$ and $P_2$ are composable; then, (a) $P_1$ and $P_2$ are composable and (b) if $q_1$ and $p_2$ are compatible, then so are $p_1$ and $p_2$ and $p_1 {|}p_2 {\sqsubseteq_{\textrm{IA}}}q_1 {|}p_2$. \[thm:iaparopcomp\]

This result relies on the fact that IAs are input-deterministic. While the theorem is already stated in [@DeAHen2005], its proof is only sketched therein. Here, it is a simple corollary of Thm. \[thm:miaparopcomp\] in Sec. \[subsec:miaparop\] and Thms. \[thm:iaembeddingmia\] and \[thm:miaembedding\](b) in Sec. \[subsec:embedding\] below.

![Example illustrating IA-parallel composition, where IA *TryOnce* has inputs $\{\textit{send, ack, nack}\}$ and outputs $\{\textit{trnsmt, ok, reset, retry}\}$, while IA *Client* has inputs $\{\textit{ok, retry}\}$ and outputs $\{\textit{send}\}$.[]{data-label="fig:iaparopex"}](iaparopex.png)

We conclude by presenting a small example of IA-parallel composition in Fig. \[fig:iaparopex\], which is adapted from [@DeAHen2005]. *Client* does not accept its input *retry*. Thus, if the environment of $\textit{Client} {\otimes}\textit{TryOnce}$ would produce *nack*, the system would autonomously produce *reset* and run into a catastrophic error. To avoid this, the environment of $\textit{Client} \,{|}\textit{TryOnce}$ is required not to produce *nack*. This view is called optimistic: there exists an environment in which *Client* and *TryOnce* can cooperate without errors, and $\textit{Client} \,{|}\textit{TryOnce}$ describes the necessary requirements for such an environment. In the pessimistic view as advocated in [@BauHenWir2011], *Client* and *TryOnce* are regarded as incompatible due to the potential error.

Conjunction and Disjunction for Modal Transition Systems {#sec:dmts}
========================================================

*Modal Transition Systems* (MTS) were investigated by Larsen [@Lar89] as a specification framework based on labelled transition systems but with two kinds of transitions: must-transitions specify required behaviour, may-transitions specify allowed behaviour, and absent transitions specify forbidden behaviour. Any refinement of an MTS-specification must preserve required and forbidden behaviour and may turn allowed behaviour into required or forbidden behaviour. Technically, this is achieved via an alternating-style simulation relation, called *modal refinement*, where any must-transition of the specification must be simulated by an implementation, while any may-transition of the implementation must be simulated by the specification.

Our aim in this section is to extend MTS with conjunction and also disjunction. Larsen [@Lar89] first defined conjunction and disjunction on MTS (without $\tau$), but the resulting systems often violate syntactic consistency (they are not really MTSs) and are hard to understand. This construction was subsequently generalized by Larsen and Xinxin to Disjunctive MTS (DMTS) [@LarXin90], again ignoring syntactic consistency. This shortcoming was recently fixed by Beneš et al. [@BenCerKre2011] by exploiting the fact that an $a$-must-transition in a DMTS may have several alternative target states. However, this work does still not consider a weak setting, i.e., systems with $\tau$. Below, we will define conjunction and disjunction on a syntactically consistent subclass of DMTS, called *dMTS*, but more generally in a weak setting as defined in [@DeAHen2005; @LarNymWas2007]; this subclass is sufficient for the purposes of the present article, and we leave the extension of our results to DMTS for future work. Since the treatment of $\tau$-transitions is non-trivial and non-standard, we will motivate and explain it in detail.

Note that this section will not consider parallel composition for (d)MTS. This is because we are working towards the MIA-setting that will be introduced in the next section, which like IA and unlike (d)MTS distinguishes between inputs and outputs. (d)MTS parallel composition can simply be defined in the style similar to Def. \[def:iaparprod\]; in particular, it does not have error states and thus fundamentally differs from conjunction as defined below.

Disjunctive Modal Transition Systems {#subsec:dmts}
------------------------------------

We extend standard MTS only as far as needed for defining conjunction and disjunction, by introducing disjunctive must-transitions that are disjunctive wrt. exit states only (see Fig. \[fig:dmtsandopex\]). The following extension also has no $\tau$-must-transitions since these are not considered in the definition of the observational modal refinement of [@LarNymWas2007].

A *disjunctive Modal Transition System* (dMTS) is a tuple $Q =
  (Q, A, {\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$, where

(1) $Q$ is a set of states,

(2) $A$ is an alphabet not containing the special, silent action $\tau$,

(3) ${\stackrel{}{\longrightarrow}} \,\subseteq Q \times A \times {({\mathcal{P}({Q})} \setminus \emptyset)}$ is the *must-transition* relation,

(4) ${\stackrel{}{\dashrightarrow}} \,\subseteq Q \times (A \cup \{\tau\}) \times Q$ is the *may-transition* relation.

We require *syntactic consistency*, i.e., $q {\stackrel{a}{\longrightarrow}}
  Q'$ implies $\forall q' {\in} Q'.\, q {\stackrel{a}{\dashrightarrow}} q'$. \[def:dmts\]

More generally, the must-transition relation in a standard DMTS [@LarXin90] may be a subset of $Q \times {({\mathcal{P}({A \times
  Q})} \setminus \emptyset)}$. For notational convenience, we write $q {\stackrel{a}{\longrightarrow}} q'$ whenever $q {\stackrel{a}{\longrightarrow}} {\{{q'}\}}$; all must-transitions in standard MTS have this form.

Our refinement relation on dMTS abstracts from internal computation steps in the same way as [@LarNymWas2007], i.e., by considering the following *weak may-transitions* for $\alpha \in A \cup
\{\tau\}$: $q {\,\raisebox{1.0ex}{$\stackrel{{\varepsilon}}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}\,} q'$ if $q
{\stackrel{\tau}{\dashrightarrow}}^{\ast}\! q'$, and $q {\,\raisebox{1.0ex}{$\stackrel{\alpha}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}\,} q'$ if $\exists q''.\, q {\,\raisebox{1.0ex}{$\stackrel{{\varepsilon}}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}\,} q'' {\stackrel{\alpha}{\dashrightarrow}}
q'$.

Let $P, Q$ be dMTSs. Relation ${\mathcal{R}} \subseteq P \times Q$ is an *(observational) modal refinement relation* if for all ${({p},{q})} \in {\mathcal{R}}$:

1.  $q {\stackrel{a}{\longrightarrow}} Q'$ implies $\exists P'.\,
        p {\stackrel{a}{\longrightarrow}} P'$ and $\forall p' {\in} P'\,\exists q' {\in} Q'.\;
        {({p'},{q'})} \in {\mathcal{R}}$,

2.  $p {\stackrel{\alpha}{\dashrightarrow}} p'$ implies $\exists q'.\, q
        {\,\raisebox{1.0ex}{$\stackrel{\hat{\alpha}}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}\,} q'$ and ${({p'},{q'})} \in {\mathcal{R}}$.

We write $p {\sqsubseteq_{\textrm{dMTS}}}q$ and say that $p$ *dMTS-refines* $q$ if there exists an observational modal refinement relation ${\mathcal{R}}$ such that ${({p},{q})} \in {\mathcal{R}}$. \[def:dmtssim\]

Again, ${\sqsubseteq_{\textrm{dMTS}}}$ is a preorder and the largest observational modal refinement relation. Except for disjunctiveness, dMTS-refinement is exactly defined as for MTS in [@LarNymWas2007]. In the following figures, any (disjunctive) must-transition drawn also represents implicitly the respective may-transition(s), unless explicitly stated otherwise.

Conjunction on dMTS {#subsec:dmtsconj}
-------------------

Technically similar to parallel composition for IA, conjunction will be defined in two stages. State pairs can be logically inconsistent due to unsatisfiable must-transitions; in the second stage, we remove such pairs incrementally.

Let $P = (P, A, {\stackrel{}{\longrightarrow}}_P,$ ${\stackrel{}{\dashrightarrow}}_P)$ and $Q = (Q,
  A, {\stackrel{}{\longrightarrow}}_Q, {\stackrel{}{\dashrightarrow}}_Q)$ be dMTSs with common alphabet. The conjunctive product $P {\&}Q {=_{\text{df}}}(P \times Q, A,
  {\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$ is defined by its operational transition rules as follows:

  ------------- ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ---- ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  [(Must1)]{}   ${({p},{q})} {\stackrel{a}{\longrightarrow}}                                                                                                                                                    if   $p {\stackrel{a}{\longrightarrow}}_P P'$ and $q {\,\raisebox{1.0ex}{$\stackrel{a}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,}$
                   {\{{{({p'},{q'})}}\,|\,{p' \in P',\, q {\,\raisebox{1.0ex}{$\stackrel{a}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,} q'}\}}$        

  [(Must2)]{}   ${({p},{q})} {\stackrel{a}{\longrightarrow}}                                                                                                                                                    if   $p {\,\raisebox{1.0ex}{$\stackrel{a}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,}$ and $q {\stackrel{a}{\longrightarrow}}_Q Q'$
                   {\{{{({p'},{q'})}}\,|\,{p {\,\raisebox{1.0ex}{$\stackrel{a}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,} p',\, q' \in Q'}\}}$        

  [(May1)]{}    ${({p},{q})} {\stackrel{\tau}{\dashrightarrow}} {({p'},{q})}$                                                                                                                                   if   $p {\,\raisebox{1.0ex}{$\stackrel{\tau}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,} p'$

  [(May2)]{}    ${({p},{q})} {\stackrel{\tau}{\dashrightarrow}} {({p},{q'})}$                                                                                                                                   if   $q {\,\raisebox{1.0ex}{$\stackrel{\tau}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,} q'$

  [(May3)]{}    ${({p},{q})} {\stackrel{\alpha}{\dashrightarrow}} {({p'},{q'})}$                                                                                                                                if   $p {\,\raisebox{1.0ex}{$\stackrel{\alpha}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,} p'$ and $q {\,\raisebox{1.0ex}{$\stackrel{\alpha}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,} q'$
  ------------- ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ---- ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

\[def:dmtsconjprod\]

It might be surprising that a single transition in the product might stem from a transition sequence in one of the components (cf. the first four items above) and that the components can also synchronize on $\tau$ (cf. Rule (May3)). The necessity of this is discussed below; we only repeat here that conjunction is inherently different from parallel composition where, for instance, there is no synchronization on $\tau$.

Given a conjunctive product $P {\&}Q$, the set ${F}\subseteq P
  \times Q$ of *(logically) inconsistent states* is defined as the least set satisfying the following rules:

  ---------- ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- --------- -----------------------
  [(F1)]{}   $p \!{\stackrel{a}{\longrightarrow}}_P$, $q \not\!\!\!{\,\raisebox{1.0ex}{$\stackrel{a}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,}$   implies   ${({p},{q})} \in {F}$
  [(F2)]{}   $p \not\!\!\!{\,\raisebox{1.0ex}{$\stackrel{a}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,}$, $q \!{\stackrel{a}{\longrightarrow}}_Q$   implies   ${({p},{q})} \in {F}$
  [(F3)]{}   ${({p},{q})} {\stackrel{a}{\longrightarrow}} R'$ and $R' \subseteq {F}$                                                                                                                              implies   ${({p},{q})} \in {F}$
  ---------- ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- --------- -----------------------

The conjunction $P {\wedge}Q$ of dMTSs $P, Q$ is obtained by deleting all states ${({p},{q})} \in {F}$ from $P {\&}Q$. This also removes any may- or must-transition exiting a deleted state and any may-transition entering a deleted state; in addition, deleted states are removed from targets of disjunctive must-transitions. We write $p {\wedge}q$ for the state ${({p},{q})}$ of $P {\wedge}Q$; these are the consistent states by construction, and $p {\wedge}q$ is only defined for such a state. \[def:dmtsandop\]

Regarding well-definedness, first observe that $P {\&}Q$ is a dMTS, where syntactic consistency follows from Rule (May3). Now, $P {\wedge}Q$ is a dMTS, too: if $R'$ becomes empty for some ${({p},{q})}
{\stackrel{a}{\longrightarrow}} R'$, then also ${({p},{q})}$ is deleted when constructing $P {\wedge}Q$ from $P {\&}Q$ according to (F3). Finally, our conjunction operator is also commutative and associative.

![Examples motivating the rules of Def. \[def:dmtsconjprod\].[]{data-label="fig:exdmtsconj"}](exdmtsconj.png)

Before we formally state that operator ${\wedge}$ is indeed conjunction on dMTS, we present several examples depicted in Fig. \[fig:exdmtsconj\], which motivate the rules of Def. \[def:dmtsconjprod\]. In each case, $r$ is a common implementation of $p$ and $q$ (but not $r'$ in Ex. I), whence these must be logically consistent. Thus, Ex. I explains Rule (Must1). If we only had ${\stackrel{\tau}{\dashrightarrow}}$ in the precondition of Rule (May1), $p {\wedge}q$ of Ex. II would just consist of a $c$-must- and an $a$-may-transition; the only $\tau$-transition would lead to a state in ${F}$ due to $b$. This would not allow the $\tau$-transition of $r$, explaining Rule (May1). In Ex. III and with only ${\stackrel{\alpha}{\dashrightarrow}}$ in the preconditions of Rule (May3), $p {\wedge}q$ would just have three $\tau$-transitions to inconsistent states (due to $b$, $c$, resp.). This explains the weak transitions for $\alpha \not= \tau$ in Rule (May3). According to Rules (May1) and (May2), $p {\wedge}q$ in Ex. IV has four $\tau$-transitions to states in ${F}$ (due to $d$). With preconditions based on at least one ${\stackrel{\tau}{\dashrightarrow}}$ instead of ${\,\raisebox{1.0ex}{$\stackrel{\tau}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}\,}$ in the $\tau$-case of Rule (May3), there would be three more $\tau$-transitions to states in ${F}$ (due to $b$ or $c$). Thus, it is essential that Rule (May3) also allows the synchronization of two weak $\tau$-transitions, which in this case gives $p {\wedge}q {\stackrel{\tau}{\dashrightarrow}} p' {\wedge}q'$.

![Example illustrating dMTS-conjunction.[]{data-label="fig:dmtsandopex"}](dmtsandopex.png)

Fig. \[fig:dmtsandopex\] shows a small example illustrating the treatment of disjunctive must-transitions in the presence of inconsistency. In $P {\&}Q$, the $a$-must-transition of $Q$ combines with the three $a$-transitions of $P$ to a truly disjunctive must-transition with a three-element target set. The inconsistency of state $(4,6)$ due to $b$ propagates back to state $(3,5)$. The inconsistent states are then removed in $P {\wedge}Q$.

Let $P, Q, R$ be dMTSs. Then, (i) $(\exists r \in R.\, r {\sqsubseteq_{\textrm{dMTS}}}p$ and $r {\sqsubseteq_{\textrm{dMTS}}}q)$ if and only if $p {\wedge}q$ is defined. In addition, in case $p {\wedge}q$ is defined: (ii) $r {\sqsubseteq_{\textrm{dMTS}}}p$ and $r {\sqsubseteq_{\textrm{dMTS}}}q \text{ if and only if } r {\sqsubseteq_{\textrm{dMTS}}}p {\wedge}q$. \[thm:dmtsandisand\]

This key theorem states in Item (ii) that conjunction behaves as it should, i.e., ${\wedge}$ on dMTSs is the greatest lower bound wrt. ${\sqsubseteq_{\textrm{dMTS}}}$. Item (i) concerns the intuition that two specifications $p$ and $q$ are logically inconsistent if they do not have a common implementation; formally, $p {\wedge}q$ is undefined in this case. Alternatively, we could have added an explicit inconsistent element ${\textit{ff}}$ to our setting, so that $p {\wedge}q =
{\textit{ff}}$. This element ${\textit{ff}}$ would be defined to be a refinement of every $p'$ and equivalent to any ${({p'},{q'})} \in
{F}$ of some $P {\&}Q$. Additionally, ${\textit{ff}}{\wedge}p'$ and $p' {\wedge}{\textit{ff}}$ would be defined as ${\textit{ff}}$, for any $p'$.

The proof of the above theorem requires us to first introduce the following concept for formally reasoning about inconsistent states:

A *dMTS-witness* $W$ of $P {\&}Q$ is a subset of $P \times
  Q$ such that the following conditions hold for all ${({p},{q})} \in
  W$:

  ---------- -------------------------------------------------- --------- -------------------------------------------------------------------------------------------------------------------------------------------------
  [(W1)]{}   $p \!{\stackrel{a}{\longrightarrow}}_P$            implies   $q {\,\raisebox{1.0ex}{$\stackrel{a}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,}$
  [(W2)]{}   $q \!{\stackrel{a}{\longrightarrow}}_Q$            implies   $p {\,\raisebox{1.0ex}{$\stackrel{a}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,}$
  [(W3)]{}   ${({p},{q})} {\stackrel{a}{\longrightarrow}} R'$   implies   $R' \cap W \not= \emptyset$
  ---------- -------------------------------------------------- --------- -------------------------------------------------------------------------------------------------------------------------------------------------

\[def:dmtswitness\]

Conditions (W1)–(W3) correspond to the negations of the premises of Conditions (F1)–(F3) in Def. \[def:dmtsandop\]. This implies Part (i) of the following lemma, while Part (ii) is essential for proving Thm. \[thm:dmtsandisand\](i):

Let $P {\&}Q$ be a conjunctive product of dMTSs and $R$ be a dMTS.

1.  For any dMTS-witness $W$ of $P {\&}Q$, we have ${F}\cap W = \emptyset$.

2.  The set $\{ {({p},{q})} \in P \times Q \;|\; \exists
        r \in R.\, \text{$r {\sqsubseteq_{\textrm{dMTS}}}p$}$ and $r {\sqsubseteq_{\textrm{dMTS}}}q \}$ is a dMTS-witness of $P {\&}Q$.

\[lem:dmtswitness\]

We are now able to prove Thm. \[thm:dmtsandisand\]:

The following corollary of Thm. \[thm:dmtsandisand\] now easily follows:

dMTS-refinement is compositional wrt. conjunction, i.e., if $p
  {\sqsubseteq_{\textrm{dMTS}}}q$ and $p {\wedge}r$ is defined, then $q {\wedge}r$ is defined and $p {\wedge}r {\sqsubseteq_{\textrm{dMTS}}}q {\wedge}r$. \[cor:dmtsandopcomp\]

Thus, we have succeeded in our ambition to define a syntactically consistent conjunction for MTS, for a weak MTS-variant with disjunctive must-transitions.

![Example illustrating Larsen’s MTS-conjunction; ${\stackrel{a}{\dashrightarrow}}$ drawn separately.[]{data-label="fig:larsen"}](larsen.png)

Larsen [@Lar89] also defines a conjunction operator on MTS, but almost always the result violates syntactic consistency. A simple example is shown in Fig. \[fig:larsen\] where $q$ refines $p$ in Larsen’s setting as well as in our dMTS-setting; in this figure, may-transitions are drawn explicitly, i.e, a must- is not necessarily also a may-transition. Since Larsen’s $p \land q$ is not syntactically consistent, this $p \land q$ and $q$ are, contrary to the first impression, equivalent. In our dMTS-setting, $P {\wedge}Q$ is isomorphic to $Q$ which will also hold for our MIA-setting below (with action $b$ read as output and where $a$ could be either an input or an output).

![Example showing that conjunction cannot be defined on MTS. (A similar example is given in [@BenCerKre2011] without proof.)[]{data-label="fig:mtsand"}](mtsand.png)

Indeed, conjunction cannot be defined on MTS in general, e.g., for the $P$ and $Q$ in Fig. \[fig:mtsand\](a). The states $p$ and $q$ have $r$ as well as $s$ as common implementations; thus, $r$ and $s$ must be implementations of $p {\wedge}q$. An MTS $P {\wedge}Q$ would need in state $p {\wedge}q$ (i) an immediate $a$-must-transition (due to $q$) followed by (ii) a must-$b$ and no $c$ or a must-$c$ and no $b$ (due to $p$). In the first (second) case, $s$ ($r$) is not an implementation of $p {\wedge}q$, which is a contradiction. Using dMTS, the conjunction $P {\wedge}Q$ is as shown in Fig. \[fig:mtsand\](b).

The above shortcoming of MTS has been avoided by Larsen et al. in [@LarSteWei95] by limiting conjunction to so-called *independent* specifications that make inconsistencies obsolete; this restriction also excludes the above example. Recently, Bauer et al. [@BauJuhLarLegSrb2012] have defined conjunction for a version of MTS extended by partially ordered labels; when refining an MTS, also the labels can be refined, and this has various applications. However, the conjunction operator is only defined under some restriction, which corresponds to requiring determinism in the standard MTS-setting. Another MTS-inspired theory including a conjunction operator has been introduced by Raclet et al. [@RacBadBenCaiLegPas2011]. While their approach yields the desired $p {\wedge}q$ as in our dMTS-setting, it is language-based and thus deals with deterministic systems only.

Disjunction on dMTS {#subsec:dmtsdisj}
-------------------

We will see in Sec. \[subsec:iaembeddingdmts\] that input-transitions (output-transitions) in IA correspond to must-transitions (may-transitions) in dMTS. In this light, the following definition of disjunction corresponds closely to the one for IA. In particular, initial must-transitions are also combined, but this time the choice between disjuncts is not delayed.

Let $P = (P, A, {\stackrel{}{\longrightarrow}}_P,$ ${\stackrel{}{\dashrightarrow}}_P)$ and $Q = (Q,
  A, {\stackrel{}{\longrightarrow}}_Q,$ ${\stackrel{}{\dashrightarrow}}_Q)$ be dMTSs with common alphabet. The disjunction $P {\vee}Q$ is defined as the tuple $(\{
  p {\vee}q \;|\; p \in P,\, q \in Q \} \cup P \cup Q, A,
  {\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$, where ${\stackrel{}{\longrightarrow}}$ and ${\stackrel{}{\dashrightarrow}}$ are the least sets satisfying ${\stackrel{}{\longrightarrow}}_P
  \subseteq {\stackrel{}{\longrightarrow}}$, ${\stackrel{}{\dashrightarrow}}_P \subseteq
  {\stackrel{}{\dashrightarrow}}$, ${\stackrel{}{\longrightarrow}}_Q \subseteq {\stackrel{}{\longrightarrow}}$, ${\stackrel{}{\dashrightarrow}}_Q \subseteq {\stackrel{}{\dashrightarrow}}$ and the following operational rules:

  ------------ -------------------------------------------------------- ---- ------------------------------------------------------------------------------------
  [(Must)]{}   $p {\vee}q {\stackrel{a}{\longrightarrow}} P' \cup Q'$   if   $p {\stackrel{a}{\longrightarrow}}_P P'$, $q {\stackrel{a}{\longrightarrow}}_Q Q'$
  [(May1)]{}   $p {\vee}q {\stackrel{\alpha}{\dashrightarrow}} p'$      if   $p {\stackrel{\alpha}{\dashrightarrow}}_P p'$
  [(May2)]{}   $p {\vee}q {\stackrel{\alpha}{\dashrightarrow}} q'$      if   $q {\stackrel{\alpha}{\dashrightarrow}}_Q q'$
  ------------ -------------------------------------------------------- ---- ------------------------------------------------------------------------------------

\[def:dmtsorop\]

This definition clearly yields well-defined dMTSs respecting syntactic consistency. It also gives us the desired least-upper-bound property:

Let $P$, $Q$, and $R$ be dMTSs with states $p$, $q$ and $r$, resp. Then, $p {\vee}q {\sqsubseteq_{\textrm{dMTS}}}r$ if and only if $p {\sqsubseteq_{\textrm{dMTS}}}r$ and $q
  {\sqsubseteq_{\textrm{dMTS}}}r$. \[thm:dmtsorisor\]

Analogously to the IA-setting we may obtain the following corollary to the above theorem:

dMTS-refinement is compositional wrt. disjunction. \[cor:dmtsoropcomp\]

Embedding of IA into dMTS {#subsec:iaembeddingdmts}
-------------------------

We can now adopt the embedding of IA into MTS from [@LarNymWas2007] to our setting:

Let $P$ be an IA with $A = I \cup O$. Then, the embedding ${[{P}]_{\text{dMTS}}}$ of $P$ into (d)MTS is defined as the (d)MTS $(P\cup\{{u_{P}}\}, A, {\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$, where ${u_{P}} \notin P$ and:

  --------------------------------------------------- ---- ---------------------------------------------------------------------------------
  $p {\stackrel{\alpha}{\dashrightarrow}} p'$         if   $p {\stackrel{\alpha}{\longrightarrow}}_P p'$ and $\alpha \in A \cup \{\tau\}$;
  $p {\stackrel{a}{\longrightarrow}} p'$              if   $p {\stackrel{a}{\longrightarrow}}_P p'$ and $a \in I$;
  $p {\stackrel{a}{\dashrightarrow}} {u_{P}}$         if   $p \,\not\!{\stackrel{a}{\longrightarrow}}_P$ and $a \in I$;
  ${u_{P}} {\stackrel{a}{\dashrightarrow}} {u_{P}}$   if   $a \in A$.
  --------------------------------------------------- ---- ---------------------------------------------------------------------------------

\[def:iaembeddingdmts\]

For the remainder of this section we simply write ${[{p}]_{\text{}}}$ for $p
\in {[{P}]_{\text{dMTS}}}$. Observe that ${[{P}]_{\text{dMTS}}}$ does not have truly disjunctive transitions; hence, it is an MTS. In [@LarNymWas2007], it is shown that this embedding respects refinement, i.e., $p {\sqsubseteq_{\textrm{IA}}}q$ if and only if ${[{p}]_{\text{}}} {\sqsubseteq_{\textrm{dMTS}}}{[{q}]_{\text{}}}$. Since conjunction (disjunction) on IA and dMTS is the greatest lower bound (least upper bound) wrt. ${\sqsubseteq_{\textrm{IA}}}$ and ${\sqsubseteq_{\textrm{dMTS}}}$ (up to equivalence), resp., we have by general order theory:

For all IAs $P$ and $Q$ with $p \in P$ and $q \in Q$:

1.  ${[{p {\wedge}q}]_{\text{}}} \,{\sqsubseteq_{\textrm{dMTS}}}\, {[{p}]_{\text{}}} {\wedge}{[{q}]_{\text{}}}$;

2.  ${[{p {\vee}q}]_{\text{}}} \,{\sqsupseteq_{\textrm{dMTS}}}\, {[{p}]_{\text{}}} {\vee}{[{q}]_{\text{}}}$.

\[prop:iaembeddingdmts\]

![Example refuting the reverse refinement in Prop. \[prop:iaembeddingdmts\](a). All non-labelled transitions depict $i$-may-transitions.[]{data-label="fig:conjiaembeddingdmts"}](conjiaembeddingdmts.png)

![Example refuting the reverse refinement in Prop. \[prop:iaembeddingdmts\](b) ($a \in A = \{i,j,k\}$).[]{data-label="fig:disjiaembeddingdmts"}](disjiaembeddingdmts.png)

The reverse refinements do not hold due to the additional dMTSs that are not embeddings of IA. To see this for conjunction, consider the example in Fig. \[fig:conjiaembeddingdmts\], where $P$ and $Q$ are IAs. State $r$ in dMTS $R$ is a common implementation of state ${[{p}]_{\text{}}}$ and state ${[{q}]_{\text{}}}$, i.e., their conjunction is sufficiently large to cover $r$. However, $r$ does not refine ${[{p {\wedge}q}]_{\text{}}}$ since the initial $i$-must-transition of the latter cannot be matched by the former. Hence, ${[{p {\wedge}q}]_{\text{}}}$ and ${[{p}]_{\text{}}} {\wedge}{[{q}]_{\text{}}}$ cannot be equivalent. To see this for disjunction, consider $r$ and $s$ in Fig. \[fig:iaoropex\] on the right. Fig. \[fig:disjiaembeddingdmts\] shows all relevant dMTSs, and ${[{r {\vee}s}]_{\text{}}}$ does not refine ${[{r}]_{\text{}}} {\vee}{[{s}]_{\text{}}}$ since it does not have a must-transition after $i$.

Modal Interface Automata {#sec:mia}
========================

An essential point of Larsen, Nyman and Wasowski’s paper [@LarNymWas2007] is to enrich IA with modalities to get a flexible specification framework where inputs and outputs can be prescribed, allowed or prohibited. To do so, they consider IOMTS, i.e., MTS where visible actions are partitioned into inputs and outputs, and define parallel composition in IA-style.

![Example demonstrating the compositionality flaw of IOMTS.[]{data-label="fig:iomtsflaw"}](iomtsflaw.png)

Our example of Fig. \[fig:iomtsflaw\] shows that their approach has a serious flaw, namely observational modal refinement is not a precongruence for the parallel composition of [@LarNymWas2007]. In this example, the IOMTS $P$ has input alphabet $\{a\}$ and empty output alphabet, while $Q$ and $Q'$ have input alphabet $\{i\}$ and output alphabet $\{a\}$. Obviously, $q' {\sqsubseteq_{\textrm{dMTS}}}q$. When composing $P$ and $Q$ in parallel, $p|q$ would reach an error state after an $i$-must-transition in [@LarNymWas2007] since the potential output $a$ of $Q$ is not expected by $P$. In contrast, $p|q'$ has an $i$-must- and $i$-may-transition not allowed by $P|Q$, so that $p|q' \not{\sqsubseteq_{\textrm{dMTS}}}p|q$. This counterexample also holds for (strong) modal refinement as defined in [@LarNymWas2007] and is particularly severe since all systems are deterministic and all must-transitions concern inputs only. The problem is that $p|q$ forbids input $i$.

In [@LarNymWas2007], precongruence of parallel composition is not mentioned. Instead, a theorem relates the parallel composition of two IOMTSs to a different composition on two refining implementations, where an implementation in [@LarNymWas2007] is an IOMTS in which may- and must-transitions coincide. This theorem is incorrect as is pointed out in [@RacBadBenCaiLegPas2011] and repaired in the deterministic setting of that paper; the repair is again not a precongruence result, but still compares the results of two different composition operators. However, a natural solution to the precongruence problem can be adopted from the IA-framework [@DeAHen2005] where inputs are always allowed implicitly. Consequently, if an input transition is specified, it will always be a must.

In the remainder, we thus define and study a new specification framework, called *Modal Interface Automata* (MIA), that takes the dMTS-setting for an alphabet consisting of input and output actions, requires input-determinism, and demands that every input-may-transition is also an input-must-transition. The advantage over IA is that outputs can be prescribed via output-must-transitions, which precludes trivial implementations like *BlackHole* discussed in Sec. \[sec:ia\].

A *Modal Interface Automaton* (MIA) is a tuple $Q = (Q, I, O,
  {\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$, where $(Q, I \cup O,
  {\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$ is a dMTS with disjoint alphabets $I$ for inputs and $O$ for outputs and where for all $i
  \in I$: (a) $q {\stackrel{i}{\longrightarrow}} Q'$ and $q {\stackrel{i}{\longrightarrow}} Q''$ implies $Q' = Q''$; (b) $q {\stackrel{i}{\dashrightarrow}} q'$ implies $\exists Q'.\, q
  {\stackrel{i}{\longrightarrow}} Q'$ and $q' \in Q'$. \[def:mia\]

In the conference version of this article, we have considered truly disjunctive must-transitions only for outputs, so as to satisfy input determinism; this suffices for developing MIA-conjunction. However, for disjunction we have seen that such transitions are also needed for inputs. The above definition of MIA therefore permits one disjunctive must-transition for each input. This allows some choice on performing an input but, surprisingly, it is input-deterministic enough to support compositionality for parallel composition (cf. Thm. \[thm:miaparopcomp\]).

Let $P, Q$ be MIAs with common input and output alphabets. Relation ${\mathcal{R}} \subseteq P \times Q$ is an *(observational) MIA-refinement relation* if for all ${({p},{q})} \in {\mathcal{R}}$:

1.  $q {\stackrel{a}{\longrightarrow}} Q'$ implies $\exists P'.\,
        p {\stackrel{a}{\longrightarrow}} P'$ and $\forall p' {\in} P'\,\exists q' {\in} Q'.\;
        {({p'},{q'})} \in {\mathcal{R}}$,

2.  $p {\stackrel{\alpha}{\dashrightarrow}} p'$ with $\alpha \in O \cup
        {\{{\tau}\}}$ implies $\exists q'.\, q
        {\,\raisebox{1.0ex}{$\stackrel{\hat{\alpha}}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}\,} q'$ and ${({p'},{q'})} \in {\mathcal{R}}$.

We write $p {\sqsubseteq_{\textrm{MIA}}}q$ and say that $p$ *MIA-refines* $q$ if there exists an observational MIA-refinement relation ${\mathcal{R}}$ such that ${({p},{q})} \in {\mathcal{R}}$. Moreover, we also write $p {=_{\textrm{MIA}}}q$ in case $p {\sqsubseteq_{\textrm{MIA}}}q$ and $q {\sqsubseteq_{\textrm{MIA}}}p$ (which is an equivalence weaker than ‘bisimulation’). \[def:miasim\]

One can easily check that ${\sqsubseteq_{\textrm{MIA}}}$ is a preorder and the largest observational MIA-refinement relation. Its definition coincides with dMTS-refinement except that Cond. (ii) is restricted to outputs and the silent action $\tau$. Thus, inputs are always allowed implicitly and, in effect, treated just like in IA-refinement. Due to the output-must-transitions in the MIA-setting, MIA-refinement can model, e.g., STG-bisimilarity [@VogWol2002] for systems without internal actions; this is a kind of alternating simulation refinement used for digital circuits.

Conjunction on MIA {#subsec:miaconj}
------------------

Similar to conjunction on dMTS, we define conjunction on MIA by first constructing a conjunctive product and then eliminating all inconsistent states.

Let $P = (P, I, O, {\stackrel{}{\longrightarrow}}_P,$ ${\stackrel{}{\dashrightarrow}}_P)$ and $Q =
  (Q, I, O, {\stackrel{}{\longrightarrow}}_Q, {\stackrel{}{\dashrightarrow}}_Q)$ be MIAs with common input and output alphabets and disjoint state sets $P$ and $Q$. The conjunctive product $P {\&}Q {=_{\text{df}}}((P \times Q) \cup P \cup Q, I,
  O, {\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$ inherits the transitions of $P$ and $Q$ and has additional transitions as follows, where $i \in I$, $o \in O$ and $\alpha \in O \cup \{\tau\}$:

  -------------- ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ---- ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  [(OMust1)]{}   ${({p},{q})} {\stackrel{o}{\longrightarrow}}                                                                                                                                                    if   $p {\stackrel{o}{\longrightarrow}}_P P'$ and $q {\,\raisebox{1.0ex}{$\stackrel{o}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,}$
                    {\{{{({p'},{q'})}}\,|\,{p' \in P',\, q {\,\raisebox{1.0ex}{$\stackrel{o}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,} q'}\}}$        

  [(OMust2)]{}   ${({p},{q})} {\stackrel{o}{\longrightarrow}}                                                                                                                                                    if   $p {\,\raisebox{1.0ex}{$\stackrel{o}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,}$ and $q {\stackrel{o}{\longrightarrow}}_Q Q'$
                    {\{{{({p'},{q'})}}\,|\,{p {\,\raisebox{1.0ex}{$\stackrel{o}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,} p',\, q' \in Q'}\}}$        

  [(IMust1)]{}   ${({p},{q})} {\stackrel{i}{\longrightarrow}} P'$                                                                                                                                                if   $p {\stackrel{i}{\longrightarrow}}_P P'$ and $q \,\not\!{\stackrel{i}{\longrightarrow}}_Q$

  [(IMust2)]{}   ${({p},{q})} {\stackrel{i}{\longrightarrow}} Q'$                                                                                                                                                if   $p \,\not\!{\stackrel{i}{\longrightarrow}}_P$ and $q {\stackrel{i}{\longrightarrow}}_Q Q'$

  [(IMust3)]{}   ${({p},{q})} {\stackrel{i}{\longrightarrow}} P' \times Q'$                                                                                                                                      if   $p {\stackrel{i}{\longrightarrow}}_P P'$ and $q {\stackrel{i}{\longrightarrow}}_Q Q'$

  [(May1)]{}     ${({p},{q})} {\stackrel{\tau}{\dashrightarrow}} {({p'},{q})}$                                                                                                                                   if   $p {\,\raisebox{1.0ex}{$\stackrel{\tau}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,} p'$

  [(May2)]{}     ${({p},{q})} {\stackrel{\tau}{\dashrightarrow}} {({p},{q'})}$                                                                                                                                   if   $q {\,\raisebox{1.0ex}{$\stackrel{\tau}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,} q'$

  [(May3)]{}     ${({p},{q})} {\stackrel{\alpha}{\dashrightarrow}} {({p'},{q'})}$                                                                                                                                if   $p {\,\raisebox{1.0ex}{$\stackrel{\alpha}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,} p'$ and $q {\,\raisebox{1.0ex}{$\stackrel{\alpha}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,} q'$

  [(IMay1)]{}    ${({p},{q})} {\stackrel{i}{\dashrightarrow}} p'$                                                                                                                                                if   $p {\stackrel{i}{\dashrightarrow}}_P p'$ and $q \,\not\!{\stackrel{i}{\dashrightarrow}}_Q$

  [(IMay2)]{}    ${({p},{q})} {\stackrel{i}{\dashrightarrow}} q'$                                                                                                                                                if   $p \,\not\!{\stackrel{i}{\dashrightarrow}}_P$ and $q {\stackrel{i}{\dashrightarrow}}_Q q'$

  [(IMay3)]{}    ${({p},{q})} {\stackrel{i}{\dashrightarrow}} {({p'},{q'})}$                                                                                                                                     if   $p {\stackrel{i}{\dashrightarrow}}_P p'$ and $q {\stackrel{i}{\dashrightarrow}}_Q q'$
  -------------- ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- ---- ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

\[def:miaconjprod\]

This product is defined analogously to IA-conjunction for inputs (plus the corresponding ‘may’ rules) and to the dMTS-product for outputs and $\tau$. Thus, it combines the effects shown in Fig. \[fig:iaandopex\] (where all outputs are treated as may) and Fig. \[fig:dmtsandopex\] (where all actions are outputs).

Given a conjunctive product $P {\&}Q$, the set ${F}\subseteq P
  \times Q$ of (logically) *inconsistent states* is defined as the least set satisfying the following rules:

  ---------- --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- --------- -----------------------
  [(F1)]{}   $p \!{\stackrel{o}{\longrightarrow}}_P$, $q \not\!\!\!{\,\raisebox{1.0ex}{$\stackrel{o}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,}$, $o \in O$   implies   ${({p},{q})} \in {F}$
  [(F2)]{}   $p \not\!\!\!{\,\raisebox{1.0ex}{$\stackrel{o}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,}$, $q \!{\stackrel{o}{\longrightarrow}}_Q$, $o \in O$   implies   ${({p},{q})} \in {F}$
  [(F3)]{}   ${({p},{q})} {\stackrel{a}{\longrightarrow}} R'$ and $R' \subseteq {F}$                                                                                                                                         implies   ${({p},{q})} \in {F}$
  ---------- --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- --------- -----------------------

The conjunction $P {\wedge}Q$ of MIAs $P, Q$ with common input and output alphabets is obtained by deleting all states ${({p},{q})} \in
  {F}$ from $P {\&}Q$ as for dMTS in Def. \[def:dmtsandop\]. We write $p {\wedge}q$ for state ${({p},{q})}$ of $P {\wedge}Q$; all such states are defined – and consistent – by construction. \[def:miaandop\]

The conjunction $P {\wedge}Q$ is a MIA and is thus well-defined. This can be seen by a similar argument as we have used above in the context of dMTS-conjunction, while input-determinism can be established by an argument similar to that in the IA-setting. Note that, in contrast to the dMTS-situation, Rules (F1) and (F2) only apply to outputs. Fig. \[fig:dmtsandopex\] is also an example for conjunction in the MIA-setting if all actions are read as outputs.

To reason about inconsistency we use a notion of witness again. This may be defined analogously to the witness notion for dMTS but replacing $a \in A$ in Def. \[def:dmtswitness\](W1) and (W2) by $a
\in O$. We then obtain the analogous lemma to Lemma \[lem:dmtswitness\], which is needed in the proof of the analogue theorem to Thm. \[thm:dmtsandisand\]:

A *MIA-witness* $W$ of $P {\&}Q$ is a subset of $(P \times
  Q) \cup P \cup Q$ such that the following conditions hold for all ${({p},{q})} \in W$:

  ---------- ------------------------------------------------------- --------- -------------------------------------------------------------------------------------------------------------------------------------------------
  [(W1)]{}   $p \!{\stackrel{o}{\longrightarrow}}_P$ with $o\in O$   implies   $q {\,\raisebox{1.0ex}{$\stackrel{o}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{Q}\,}$
  [(W2)]{}   $q \!{\stackrel{o}{\longrightarrow}}_Q$ with $o\in O$   implies   $p {\,\raisebox{1.0ex}{$\stackrel{o}{\underset{\text{\normalsize $\dashrightarrow$}}{\raisebox{-1.0ex}[0ex][0ex]{$\dashrightarrow$}}}$}_{P}\,}$
  [(W3)]{}   ${({p},{q})} {\stackrel{a}{\longrightarrow}} R'$        implies   $R' \cap W \not= \emptyset$
  ---------- ------------------------------------------------------- --------- -------------------------------------------------------------------------------------------------------------------------------------------------

\[def:miawitness\]

Let $P {\&}Q$ be a conjunctive product of MIAs. Then, for any MIA-witness $W$ of $P {\&}Q$, we have (i) ${F}\cap W =
  \emptyset$. Moreover, (ii) the set $W {=_{\text{df}}}\{ {({p},{q})} \in P
  \times Q \;|\; \exists\,\text{MIA}\,R$ and $r \in R.\, r {\sqsubseteq_{\textrm{MIA}}}p
  \text{ and } r {\sqsubseteq_{\textrm{MIA}}}q \} \cup P \cup Q$ is a MIA-witness of $P
  {\&}Q$. \[lem:miawitness\]

We can now state and prove the desired largest-lower-bound theorem, from which compositionality of ${\sqsubseteq_{\textrm{MIA}}}$ wrt. ${\wedge}$ follows in analogy to the IA- and dMTS-settings:

Let $P, Q$ be MIAs. We have *(i)* $(\exists\,\text{MIA}\,R$ and $r \in
  R.\, r {\sqsubseteq_{\textrm{MIA}}}p$ and $r {\sqsubseteq_{\textrm{MIA}}}q)$ if and only if $p {\wedge}q$ is defined. Further, in case $p {\wedge}q$ is defined and for any MIA $R$ and $r \in R$: *(ii)* $r {\sqsubseteq_{\textrm{MIA}}}p \text{ and } r {\sqsubseteq_{\textrm{MIA}}}q
  \text{ if and only if } r {\sqsubseteq_{\textrm{MIA}}}p {\wedge}q$. \[thm:miaandisand\]

In analogy to Corollary \[cor:dmtsandopcomp\] we obtain:

MIA-refinement is compositional wrt. conjunction. \[cor:miaandopcomp\]

Disjunction on MIA {#subsec:miadisj}
------------------

The disjunction of two MIAs $P$ and $Q$ can be defined in the same way as for dMTS, except for the special treatment of inputs in the may-rules which guarantees that $P {\vee}Q$ is a MIA and, especially, that Def. \[def:mia\](b) is satisfied:

Let $P = (P, I, O, {\stackrel{}{\longrightarrow}}_P,$ ${\stackrel{}{\dashrightarrow}}_P)$, $Q = (Q,
  I, O, {\stackrel{}{\longrightarrow}}_Q,$ ${\stackrel{}{\dashrightarrow}}_Q)$ be MIAs with common input and output alphabets and disjoint state sets $P$ and $Q$. The disjunction $P {\vee}Q$ is defined by $(\{ p {\vee}q \;|\; p \in
  P,\, q \in Q \} \cup P \cup Q, I, O, {\stackrel{}{\longrightarrow}},
  {\stackrel{}{\dashrightarrow}})$, where ${\stackrel{}{\longrightarrow}}$ and ${\stackrel{}{\dashrightarrow}}$ are the least sets satisfying ${\stackrel{}{\longrightarrow}}_P \subseteq {\stackrel{}{\longrightarrow}}$, ${\stackrel{}{\dashrightarrow}}_P \subseteq {\stackrel{}{\dashrightarrow}}$, ${\stackrel{}{\longrightarrow}}_Q
  \subseteq {\stackrel{}{\longrightarrow}}$, ${\stackrel{}{\dashrightarrow}}_Q \subseteq {\stackrel{}{\dashrightarrow}}$ and the following operational rules:

  ------------ -------------------------------------------------------- ---- ------------------------------------------------------------------------------------------------------------------------------
  [(Must)]{}   $p {\vee}q {\stackrel{a}{\longrightarrow}} P' \cup Q'$   if   $p {\stackrel{a}{\longrightarrow}}_P P'$ and $q {\stackrel{a}{\longrightarrow}}_Q Q'$
  [(May1)]{}   $p {\vee}q {\stackrel{\alpha}{\dashrightarrow}} p'$      if   $p {\stackrel{\alpha}{\dashrightarrow}}_P p'$ and, in case $\alpha \in I$, also $q \!{\stackrel{\alpha}{\dashrightarrow}}_Q$
  [(May2)]{}   $p {\vee}q {\stackrel{\alpha}{\dashrightarrow}} q'$      if   $q {\stackrel{\alpha}{\dashrightarrow}}_Q q'$ and, in case $\alpha \in I$, also $p \!{\stackrel{\alpha}{\dashrightarrow}}_P$
  ------------ -------------------------------------------------------- ---- ------------------------------------------------------------------------------------------------------------------------------

\[def:miaorop\]

It is easy to see that this definition is well-defined, i.e., the resulting disjunctions are indeed MIAs, and we additionally have:

Let $P$, $Q$ and $R$ be MIAs with states $p$, $q$ and $r$, resp. Then, $p {\vee}q {\sqsubseteq_{\textrm{MIA}}}r$ if and only if $p {\sqsubseteq_{\textrm{MIA}}}r$ and $q
  {\sqsubseteq_{\textrm{MIA}}}r$. \[thm:miaorisor\]

The theorem’s proof is as for dMTS (cf. Thm. \[thm:dmtsorisor\]) but, in the (ii)-cases, only $\alpha \in O \cup \{\tau\}$ has to be considered. Analogously to dMTS we obtain the following corollary to Thm. \[thm:miaorisor\]:

MIA-refinement is compositional wrt. disjunction. \[cor:miaoropcomp\]

![MIA-disjunction is more intuitive than IA-disjunction.[]{data-label="fig:miadisjintuitive"}](miadisjintuitive.png)

To conclude this section we argue that MIA-disjunction is more intuitive than IA-disjunction. The example in Fig. \[fig:miadisjintuitive\] shows MIAs $P$, $Q$, $P {\vee}Q$ as well as a MIA $R$, where state $r$ corresponds to the IA-disjunction of states $p$ and $q$ when we understand $P$ and $Q$ as IAs. As expected (cf. p. ), $p {\vee}q$ is a refinement of $r$, but not vice versa. MIA-disjunction can now be considered to be more intuitive since the first transition in the disjunction decides which disjunct has to be satisfied afterward, in contrast to IA-disjunction.

![MIA-disjunction is an inclusive-or.[]{data-label="fig:miainclusiveor"}](miainclusiveor.png)

Moreover, Fig. \[fig:miainclusiveor\] shows that MIA-disjunction is an inclusive-or: an implementation of $p {\vee}q$ can have an $o1$-transition followed by $i$ and another $o1$-transition followed by $j$; interestingly, $r {\sqsubseteq_{\textrm{MIA}}}p {\vee}q$ satisfies ‘half’ of $p$ and ‘half’ of $q$. In general, for each action  separately, a refinement of some disjunction has to satisfy at least all initial $a$-must-transitions of one of its disjuncts.

Parallel Composition on MIA {#subsec:miaparop}
---------------------------

In analogy to the IA-setting [@DeAHen2005] we provide a parallel operator on MIA. Here, error states are identified, and all states are removed from which reaching an error state is unavoidable in some implementation, as is done for IOMTS in [@LarNymWas2007].

MIAs $P_1$ and $P_2$ are *composable* if $A_1 \cap A_2 = (I_1
  \cap O_2) \cup (O_1 \cap I_2)$, as in IA. For such MIAs we define the *product* ${\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$, where $I = (I_1 \cup I_2)
  \setminus (O_1 \cup O_2)$ and $O = (O_1 \cup O_2) \setminus (I_1
  \cup I_2)$ and where ${\stackrel{}{\longrightarrow}}$ and ${\stackrel{}{\dashrightarrow}}$ are defined as follows:

  ------------- --------------------------------------------------------------------------- ---- ---------------------------------------------------------------------------------------------------------
  [(Must1)]{}   ${({p_1},{p_2})} {\stackrel{a}{\longrightarrow}} P'_1 \times {\{{p_2}\}}$   if   $p_1 {\stackrel{a}{\longrightarrow}} P'_1$ and $a \notin A_2$
  [(Must2)]{}   ${({p_1},{p_2})} {\stackrel{a}{\longrightarrow}} {\{{p_1}\}} \times P'_2$   if   $p_2 {\stackrel{a}{\longrightarrow}} P'_2$ and $a \notin A_1$
  [(May1)]{}    ${({p_1},{p_2})} {\stackrel{\alpha}{\dashrightarrow}} {({p'_1},{p_2})}$     if   $p_1 {\stackrel{\alpha}{\dashrightarrow}} p'_1$ and $\alpha \notin A_2$
  [(May2)]{}    ${({p_1},{p_2})} {\stackrel{\alpha}{\dashrightarrow}} {({p_1},{p'_2})}$     if   $p_2 {\stackrel{\alpha}{\dashrightarrow}} p'_2$ and $\alpha \notin A_1$
  [(May3)]{}    ${({p_1},{p_2})} {\stackrel{\tau}{\dashrightarrow}} {({p'_1},{p'_2})}$      if   $p_1 {\stackrel{a}{\dashrightarrow}} p'_1$ and $p_2 {\stackrel{a}{\dashrightarrow}} p'_2$ for some $a$.
  ------------- --------------------------------------------------------------------------- ---- ---------------------------------------------------------------------------------------------------------

\[def:miaparprod\]

Recall that there are no $\tau$-must-transitions since they are irrelevant for refinement.

Given a parallel product $P_1 {\otimes}P_2$, a state ${({p_1},{p_2})}$ is an *error state* if there is some $a \in A_1 \cap A_2$ such that (a) $a \in O_1$, $p_1 \!{\stackrel{a}{\dashrightarrow}}$ and $p_2
  \,\not\!{\stackrel{a}{\longrightarrow}}$, or (b) $a \in O_2$, $p_2 \!{\stackrel{a}{\dashrightarrow}}$ and $p_1 \,\not\!{\stackrel{a}{\longrightarrow}}$.

Again we define the set $E \subseteq P_1 \times P_2$ of *incompatible* states as the least set such that ${({p_1},{p_2})} \in E$ if (i) ${({p_1},{p_2})}$ is an error state or (ii) ${({p_1},{p_2})} {\stackrel{\alpha}{\dashrightarrow}} {({p'_1},{p'_2})}$ for some $\alpha \in O \cup \{\tau\}$ and ${({p'_1},{p'_2})} \in E$.

The *parallel composition* $P_1 {|}P_2$ of $P_1$ and $P_2$ is now obtained from $P_1 {\otimes}P_2$ by *pruning*, namely removing all states in $E$ and every transition that involves such states as its source, its target or one of its targets; all may-transitions underlying a removed must-transition are deleted, too. If ${({p_1},{p_2})} \in P_1 {|}P_2$, we write $p_1 {|}p_2$ and call $p_1$ and $p_2$ *compatible*. \[def:miaparop\]

Parallel products and parallel compositions are well-defined MIAs. Syntactic consistency is preserved, as is input-determinism since input-transitions are directly inherited from one of the *composable* systems. In particular, Cond. (b) in Def. \[def:mia\] holds due to the additional clause regarding the deletion of may-transitions. In addition, targets of disjunctive must-transitions are never empty since all must-transitions that remain after pruning are taken from the product without modification.

As an example why pruning is needed, consider Fig. \[fig:iaparopex\] again and read the $\tau$-transitions as may-transitions and all other transitions as must-transitions. Further observe that pruning is different from removing inconsistent states in conjunction. For truly disjunctive transitions ${({p_1},{p_2})} {\stackrel{a}{\longrightarrow}} P'$ of the product $P_1 {\otimes}P_2$, the state ${({p_1},{p_2})}$ is removed already if $P' \cap E \not= \emptyset$, i.e., there exists some ${({p'_1},{p'_2})} \in P' \cap E$, and not only if $P' \subseteq E$. This is clear for $a \in O$ since ${({p_1},{p_2})} {\stackrel{a}{\dashrightarrow}}
{({p'_1},{p'_2})}$ by syntactic consistency and, therefore, ${({p_1},{p_2})}$ is deleted itself by Cond. (ii) above. Note that Cond. (ii) corresponds directly to the IA-case since output-transitions there correspond to may-transitions here (see Sec. \[subsec:iaembeddingdmts\]). For $a \in I$, reaching the error state can only be prevented if the environment does not provide $a$; intuitively, this is because $P'$ has w.l.o.g. the form $P'_1 \times
\{p_2\}$ in the product of $P_1$ and $P_2$ (i.e., $p'_2 = p_2$). The implementor of $P_1$ might choose to implement $p_1 {\stackrel{a}{\longrightarrow}} p'_1$ such that – when $P_1$’s implementation is composed with $P_2$’s – the error state is reached. To express the requirement on the environment not to exhibit $a$, must-transition ${({p_1},{p_2})}
{\stackrel{a}{\longrightarrow}} P'$ and all underlying may-transitions have to be deleted.

Let $P_1$, $P_2$ and $Q_1$ be MIAs with $p_1 \in P_1$, $p_2 \in
  P_2$, $q_1 \in Q_1$ and $p_1 {\sqsubseteq_{\textrm{MIA}}}q_1$. Assume that $Q_1$ and $P_2$ are composable; then:

1.  $P_1$ and $P_2$ are composable.

2.  If $q_1$ and $p_2$ are compatible, then so are $p_1$, $p_2$ and $p_1 {|}p_2 {\sqsubseteq_{\textrm{MIA}}}q_1 {|}p_2$.

\[thm:miaparopcomp\]

![Example illustrating the need of input-determinism for MIA.[]{data-label="fig:miainputdet"}](miainputdet.png)

This precongruence property of MIA-refinement would not hold if we would do away with input-determinism in MIA. To see this, consider the example of Fig. \[fig:miainputdet\] for which $p {\sqsubseteq_{\textrm{MIA}}}q$; however, $p {|}r {\sqsubseteq_{\textrm{MIA}}}q {|}r$ does not hold since $q$ and $r$ are compatible while $p$ and $r$ are not. An analogue reasoning applies to IA, although we do not know of a reference in the IA literature where this has been observed.

Embedding of IA into MIA {#subsec:embedding}
------------------------

To conclude, we provide an embedding of IA into MIA in the line of [@LarNymWas2007]:

Let $P$ be an IA. The embedding ${[{P}]_{\text{MIA}}}$ of $P$ into MIA is defined as the MIA $(P, I, O, {\stackrel{}{\longrightarrow}}, {\stackrel{}{\dashrightarrow}})$, where (i) $p {\stackrel{i}{\longrightarrow}} p'$ if $p {\stackrel{i}{\longrightarrow}}_P p'$ and $i \in I$, and (ii) $p {\stackrel{\alpha}{\dashrightarrow}} p'$ if $p {\stackrel{\alpha}{\longrightarrow}}_P p'$ and $\alpha \in I \cup O \cup \{\tau\}$. \[def:iaembeddingmia\]

In the remainder of this section we simply write ${[{p}]_{\text{}}}$ for $p
\in {[{P}]_{\text{MIA}}}$. This embedding is much simpler than the one of [@LarNymWas2007] since MIA more closely resembles IA than IOMTS does. In particular, the following theorem is obvious:

For IAs $P, Q$ with $p \in P$, $q \in Q$: $\,p {\sqsubseteq_{\textrm{IA}}}q$ if and only if ${[{p}]_{\text{}}} {\sqsubseteq_{\textrm{MIA}}}{[{q}]_{\text{}}}$. \[thm:iaembeddingmia\]

Our embedding respects operators ${\wedge}$ and ${|}$, unlike the one in [@LarNymWas2007]:

For IAs $P, Q$ with $p \in P$, $q \in Q$:

1.  ${[{p}]_{\text{}}} {\wedge}{[{q}]_{\text{}}}$ ${=_{\textrm{MIA}}}$ ${[{p {\wedge}q}]_{\text{}}}$;

2.  ${[{p}]_{\text{}}} \,{|}\, {[{q}]_{\text{}}}$ ${=_{\textrm{MIA}}}$ ${[{p {|}q}]_{\text{}}}$.

\[thm:miaembedding\]

We observe that the IA-embedding into MIA is ‘better’ wrt. conjunction than that into dMTS since refinement holds in both directions. The reason is that MIA-refinement is coarser (i.e., larger) than dMTS-refinement applied to MIAs (which are dMTSs after all): input may-transitions do not have to be matched in the former. Thus, there can be more lower bounds wrt. MIA-refinement and the greatest lower bound can be larger.

For IAs $P, Q$ with $p \in P$, $q \in Q$, we have: ${[{p}]_{\text{}}}
  {\vee}{[{q}]_{\text{}}} \,{\sqsubseteq_{\textrm{MIA}}}\, {[{p {\vee}q}]_{\text{}}}$. \[prop:thm:miaembeddingdisj\]

This result holds by general order theory due to Thm. \[thm:iaembeddingmia\]. The reverse refinement for disjunction is not valid as we have already seen in Fig. \[fig:miadisjintuitive\], and this difference repairs a shortcoming of IA-disjunction as discussed on p. .

Conclusions and Future Work {#sec:conclusions}
===========================

We introduced *Modal Interface Automata* (MIA), an interface theory that is more expressive than *Interface Automata* (IA) [@DeAHen2005]: it allows one to mandate that a specification’s refinement must implement some output, thus excluding trivial implementations, e.g., one that accepts all inputs but never emits any output. This was also the motivation behind *IOMTS* [@LarNymWas2007] that extends *Modal Transition Systems* (MTS) [@Lar89] by inputs and outputs; however, the IOMTS-parallel operator in the style of IA is not compositional. Apart from having disjunctive must-transitions, MIA is a subset of IOMTS, but it has a different refinement relation that is a precongruence for parallel composition.

Most importantly and in contrast to IA and IOMTS, the MIA theory is equipped with a conjunction operator for reasoning about components that satisfy multiple interfaces simultaneously. Along the way, we also introduced conjunction on IA and a disjunctive extension of MTS – as well as disjunction on IA, MTS and MIA – and proved these operators to be the desired greatest lower bounds (resp., least upper bounds) and thus compositional. Compared to the language-based modal interface theory of [@RacBadBenCaiLegPas2011], our formalism supports nondeterministic specifications and allows limited nondeterminism (in the sense of deterministic *disjunctive* transitions) even for inputs. Hence, MIA establishes a theoretically clean and practical interface theory that fixes the shortcomings of related work.

![In Logic LTS [@LueVog2010], disjunction is internal choice.[]{data-label="fig:intchoice"}](intchoice.png)

From a technical perspective, our MIA-theory borrows from our earlier work on Logic LTS [@LueVog2010]. There, we started from a very different conjunction operator appropriate for a deadlock-sensitive CSP-like process theory, and then derived a ‘best’ suitable refinement relation. In [@LueVog2010], disjunction is simply internal choice $\sqcap$, as sketched in Fig. \[fig:intchoice\]. For MIA, $p
\sqcap q$ is not suited at all since both $p$ and $q$ require that input $i$ is performed immediately.

Future work shall follow both theoretical and practical directions. On the theoretical side, we firstly wish to study MIA’s expressiveness in comparison to other theories via thoroughness [@FecFruLueSch2009]. More substantially, however, we intend to enrich MIA with temporal-logic operators, in the spirit of truly mixing operational and temporal-logic styles of specification in the line of our *Logic LTS* in [@LueVog2011]. Important guidance for this will be the work of Feuillade and Pinchinat [@FeuPin2007], who have introduced a temporal logic for modal interfaces that is equally expressive to MTS. In contrast to [@LueVog2011], their setting is not mixed, does not consider nondeterminism, and does not include a refinement relation. Indeed, a unique feature of Logic LTS is that its refinement relation subsumes the standard temporal-logic satisfaction relation.

On the practical side, we plan to study the algorithmic complexity implied by MIA-refinement, on the basis of existing literature for MTS. For example, Antonik et al. [@AntHutLarNymWas2010] discuss related decision problems such as the existence of a common implementation; Fischbein and Uchitel [@FisUch2008] generalize the conjunction of [@LarSteWei95] and study its algorithmic aspects; Beneš et al. [@BenCerKre2011] show that refinement problems for DMTS are not harder than in the case of MTS and also consider conjunction; Raclet et al. [@RacBadBenCaiLegPas2011] advocate deterministic automata for modal interface theories in order to reduce complexity. In addition, we wish to adapt existing tool support for interface theories to MIA, e.g., the *MIO Workbench* [@BauMaySchHen2010].

Acknowledgement {#acknowledgement .unnumbered}
===============

We thank the anonymous reviewers for their constructive comments and for pointing out additional related work. Part of this research was supported by the DFG (German Research Foundation) under grant nos. LU 1748/3-1 and VO 615/12-1 (“Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic”).
