The Quotient in Preorder Theories

The logic synthesis community has been a pioneer in defining and solving special cases of the quotient problem for combinational and sequential logic circuit design ([25, 13]) under names like circuit rectification or engineering change or component replacement. In combinational synthesis, much work has been reported to support algebraic and Boolean division: given dividend $f$ and divisor $g$, find the quotient $q$ and remainder $r$ such $f=q\cdot g+r$ (for $\cdot,+$ standard Boolean operators AND and OR, respectively), as key operation to restructure multi-level Boolean networks [18]. The quotient problem for combinational circuits was formulated as a general replacement problem in [10]: given the combinational circuits $A$ and $C$ whose synchronous composition produces the circuit specification $B$, what are the legal replacements of $C$ that are consistent with the input-output relation of $B$? The valid replacements for $C$ were defined as the combinational circuits $x$ such that $A\circ x\subseteq B$, and the largest solution for $x$ was characterized by the closed formula $x=\left(A\circ B^{\bot}\right)^{\bot}$, where $(\cdot)^{\bot}$ is a unary operator that complements the input-output relation of the circuit to which it is applied (switching the inputs and outputs), while a hiding operation gets rid of the internal signals.

In sequential optimization, the typical question addressed was, given a finite-state machine (FSM) $A$, find an FSM $x$ such that their synchronous composition produces an FSM behaviorally equivalent to a specification FSM $B$, i.e., solve over FSMs the equation $A\circ x=B$, where $\circ$ is synchronous composition and equality is FSM input-output equivalence. Various topologies were solved, starting with serial composition where the unknown was either the head or tail machine, to more complex interconnections with feedback. As a matter of fact, sometimes both $A$ and $x$ were known, but the goal was to change them into FSMs yielding better logical implementations, while preserving their composition, with the objective to optimize a sequential circuit by computing and exploiting the flexibility due to its modular structure and its environment (see [18, 39, 22]). An alternative formulation of FSM network synthesis was provided by encoding the problem in the logic WS1S (Weak Second-Order Logic of 1 Successor), which enables to characterize the set of permissible behaviors at a node of a given network of FSMs by WS1S formulas [2], corresponding to regular languages and so to effective operations on finite state automata. ¹¹1A detailed survey of previous work in this area can be found in [24, 41].

Another stream of contributions has been motivated by component-based design of parallel systems with an interleaving semantics (denoted in our exposition by the composition operator $\diamond$). The problem is stated by Merlin and Bochmann [32] as follows: “Given a complete specification of a given module and the specifications of some submodules, the method described below provides the specification of an additional submodule that, together with the other submodules, will provide a system that satisfies the specification of the given module.” The problem was reduced to solving equations or inequalities over process languages, which are usually prefix-closed regular languages represented by labeled transition systems. A closed-form solution of the inequality $A\diamond x\subseteq B$ over prefix-closed regular languages, written as $proj_{\_}x(A\diamond B)-proj_{\_}x(A\diamond\overline{B})$ (where $proj_{\_}x$ is a projection over the alphabet of $x$), was given in [32, 20].²²2For a discussion about the maximality of this solution and for more references, we refer to [41], Sec. 5.2.1. This approach to solve the equation $A\diamond x=B$ has been further extended to obtain restricted solutions that satisfy properties such as safety and liveness, or are restricted to be FSM languages, which need to be input-progressive and avoid divergence (see [20, 8, 41]). The quotient problem has been investigated also for delay-insensitive processes to model asynchronous sequential circuits, see [14, 31, 33]. Equations of the form $A\diamond x\leq B$ were defined, and their largest closed-form solutions were written as $x=\left(A\diamond B^{\sim}\right)^{\sim}$, where $(\cdot)^{\sim}$ is a suitable unary operation.

An important application from discrete control theory is the model matching problem: design a controller whose composition with a plant matches a given specification (see [3, 17]). Another significant application of the quotient computation has been the protocol design problem, and in particular, the protocol conversion problem (see [28, 19, 36, 34, 26, 21, 42, 12]). Protocol converter synthesis has been studied also over a variant of Input/Output Automata (IOA, [30]), called Interface Automata (IA, [16, 15]), yielding a similar quotient equation $A\diamond_{\_}{IA}x\subseteq B$ and closed-form solution $\left(A\diamond_{\_}{IA}B^{\bot}\right)^{\bot}$, where $\diamond_{\_}{IA}$ is an appropriate interleaving composition defined for interface automata, and $(\cdot)^{\bot}$ is again a unary operation [7].

Some research focused on modal specifications represented by automata whose transitions are typed with may and must modalities, as in [29, 37], with a solution of the quotient problem for nondeterministic automata provided in  [4]. It is outside the scope of this paper to address the quotient problem for real-time and hybrid systems (see [11, 9] for verification and control in such settings).

As seen above, the quotient problem was studied by different research communities working on various application domains and formalisms. Often similar formulations and solutions were reached albeit obfuscated by the different notations and objectives of the synthesis process. This motivated a concentrated effort to distill the core of the problem, modeling it as solving equations over languages of the form $A\parallel x\preceq B$, where $A$ and $B$ are known components and $x$ is unknown, $\parallel$ is a composition operator, and $\preceq$ is a conformance relation (see [40] and the monograph [41] for full accounts). The notion of language was chosen as the most basic formalism to specify the components of the equation, and language containment $\subseteq$ was selected as conformance relation. Two basic composition operators were defined each encapsulating a family of variants: synchronous composition ($\bullet$) modeling the classical step-lock coordination, and interleaving composition ($\diamond$) modeling asynchrony by which components may progress at different rates (there are subtle issues in comparing the two types, as mentioned in [27, 43]). Therefore two language equations were defined: $A\bullet x\subseteq B$ and $A\diamond x\subseteq B$, where the details of the operations to convert alphabets according to the interconnection topologies are hidden in the formula. It turned out that the largest solutions have the same structure, respectively, $\overline{A\bullet\overline{B}}$ and $\overline{A\diamond\overline{B}}$. This led to investigate the algebraic properties required by the composition operators to deliver the previous largest closed-form solutions to unify the two formulas [40]. This effort assumed that the underlying objects were sets, and that their operations were given in terms of set operations. This work, thus, could not account for quotient computations in more complex theories, like interface automata.

As a parallel development, in recent years we have seen the growth of a rigorous theory of system design based on the algebra of contracts (see the monograph [6]). In this theory, a strategic role is played by assume-guarantee (AG) contracts, in which the missing component problem arises: when the given components are not capable of discharging the obligations of the requirements, define a quotient operation that computes the contract for a component, so that by its addition to the original set the resulting system fulfills the requirements. The quotient of AG contracts was completely characterized very recently by a closed-form solution proved in [38]. Once again, the syntax of the quotient has the form $\left(A\parallel B^{-1}\right)^{-1}$ for contracts $A$ and $B$ and standard contract operations.

In summary, even though the concrete models of the components, composition operators, conformance relations and inversion functions vary significantly across chosen models and application domains, the quotient formulas have similar syntax across theories.

The motivation of this paper is to propose the underlying mathematical structure common to all these instances of quotient computation to be able to derive directly the solution formula for any equation satisfying the properties of this common structure.

We show that we can compute the quotient by only assuming the axioms of a preorder, enriched with a binary operation of source multiplication and a unary involution operation. In particular we introduce the new algebraic notion of preordered heaps characterized by a condition, called admissibility, which guarantees the existence of the solution and yields a closed form for it. Then we show that a number of theories in computer science meet this condition, e.g., Boolean lattices, AG contracts, and interface automata; so for all of them we are able to (re-)derive axiomatically the formulas that compute their related quotients. We also introduce the concept of sieved heaps to deal with structures defined over multiple domains, and we show that the equations $A\bullet x\leq B$ admit a solution also over sieved heaps, generalizing the known solutions of equations on languages over multiple alphabets with respect to synchronous and interleaving composition, well studied in the literature.

The paper is structured as follows. Sec. 2 develops the basic mathematical machinery of preordered heaps, whereas Sec. 3 shows that various theories are preordered heaps. Sec. 4 introduces sieved heaps, whereas Sec. 5 applies them to equations over languages with multiple alphabets. Sec. 6 concludes. Some proofs are omitted due to space constraints.

As we discussed in the introduction, many times in engineering and computer science one encounters expressions of the form $A\bullet x\leq B$, and one wishes to solve for the largest $x$ that satisfies the expression. The symbols have different specific meanings in the various domains, yet in all applications we know, the syntax for computing the quotient always has the form $\overline{A\bullet\overline{B}}$, where $\overline{(\cdot)}$ is an involution (i.e., a unary operator which is its own inverse). To give meaning to the inequality, at a minimum we need a preorder and a binary operation; to give meaning to the quotient expression, we need to assume the existence of an involution. In all compositional theories, the refinement order has the connotation of specificity: if $a\leq b$ then $a$ is a refinement of $b$. The binary operation is usually interpreted as composition. The product $a\bullet b$ is understood as the design obtained when operating both $a$ and $b$ in a topology given by the mathematical description of each component. The unary operation is sometimes understood as giving an external view on an object. If a component has mathematical description $a$, then $\overline{a}$ gives the view that the environment has of the design element. In Boolean algebras, this unary operation is negation. In interface theories, it’s usually an operation which switches inputs and output behaviors.

We thus introduce an algebraic structure consisting of a preorder, a binary operation which is monotonic in both arguments, and an involution which is antitone. We have called the binary operation source multiplication for reasons having to do with category theory: we will show that this operation serves as the left functor of an adjunction. Therefore, its application to an object of the preorder yields the source of one of the two arrows in the adjunction. Why not simply call it multiplication? Because source multiplication together with the involution generate another binary operation. This second operation we call target multiplication because its application to an object yields the target of one of the arrows in the adjunction. The unary operation will simply be called involution.

The algebraic structure will be called preordered heap. The inspiration came from engineering design. In some design methodologies, design elements at the same level of abstraction are not comparable in the refinement order. Indeed, a refinement of a design element usually yields a design element in a more concrete layer. But we are placing all components under the same mathematical structure. This suggested the name heap. We add the adjective preorder simply to differentiate the concept from existing algebraic heaps. We are ready for the definition:

We have discussed all elements in the definition of a preordered heap, except for the admissibility conditions. What are they? Consider left admissibility: $\mu_{a}\circ\gamma\circ\mu^{a}\circ\gamma\leq\text{id}$. Let $b\in P$ and set $B=(\gamma\circ\mu^{a}\circ\gamma)(b)$. Left admissibility means that $B$ satisfies the expression $\mu(a,x)\leq b$. Similarly, set $C=(\gamma\circ\mu_{a}\circ\gamma)(b)$. Right admissibility means that $C$ satisfies $\mu(x,a)\leq b$. When $\mu$ is commutative, we of course have $B=C$. We will soon show a surprising fact: the axioms of a preordered heap are sufficient to guarantee that $B$ and $C$ are in fact the largest solutions to both expressions, i.e., $B$ and $C$ are the quotients for left and right source multiplication, respectively. We show this immediately after introducing an important binary operation called target multiplication, but first we consider an example.

For the rest of this section, let $(P,\leq,\mu,\gamma)$ be a preordered heap. We define the target multiplication $\tau\colon P\times P\to P$ as $\tau=\gamma\circ\mu\circ(\gamma\times\gamma)$. Since $\gamma^{2}=\text{id}$ (axiom A1), we can also write $\mu=\gamma\circ\tau\circ(\gamma\times\gamma)$, i.e., the diagram commutes.

We could have defined a preordered heap in terms of target multiplication instead of source multiplication. The two operations are closely linked. In fact, we will see in the next section that these operations form an adjoint pair.

For $a,b\in P$, we are interested in the conditions under which we can find the largest $x\in P$ such that $\mu(a,x)\leq b$. The following theorem says that source multiplication in a preordered heap is “invertible.”

The fact that $(\mu_{a},\tau^{\gamma a})$ is an adjoint pair means that left source multiplication by $a$ is “inverted” by right target multiplication by $\gamma a$, i.e.,

$$\mu(a,x)\leq b\quad\text{if and only if}\quad x\leq\tau(b,\gamma a).$$

In other words, the largest solution of $\mu(a,x)\leq b$ is $x=\tau(b,\gamma a)$. Using the familiar multiplicative notation for source multiplication, and $(\cdot)/a=\tau^{\gamma a}$ for “right division by $a$,” we have shown that the largest solution of $ax\leq b$ is $x=b/a$. Calling $a\backslash(\cdot)=\tau_{\gamma a}$ “left division by $a$,” we have shown that the largest solution of $xa\leq b$ is $x=a\backslash b$. These two divisions are related as follows:

Theorem 2.2 is our main result. It shows that preordered heaps have sufficient structure for the computation of quotients. When we prove that a structure is a preordered heap, this theorem immediately yields the existence of an adjoint for multiplication, and its closed form.

In general, to show that a theory is a preordered heap, we must identify its involution and source multiplication. Then we have to verify the admissibility conditions. How difficult is that? Our original problem was identifying the largest $x$ satisfying $\mu(a,x)\leq b$ for some notion of multiplication $\mu$, involution $\gamma$, and preorder $\leq$. As we discussed, left admissibility requires that $\tau^{\gamma a}b$ satisfies the inequality $\mu(a,x)\leq b$, and right admissibility requires that $\tau_{\_}{\gamma a}b$ satisfies $\mu(x,a)\leq b$. What the theorem tells us is that they are the largest solutions to $\mu(a,x)\leq b$ and $\mu(x,a)\leq b$, respectively. In other words, the theorem saves us the effort of making an argument for the optimality of the solutions.

Theorem 2.2 also suggests the following observation. For a given $a\in P$, we have adjoint pairs $(\mu_{\_}a,\tau^{\gamma a})$ and $(\mu^{a},\tau_{\_}{\gamma a})$. As we noticed, this means we can find the largest $x$ such that $\mu(a,x)\leq b$ or $\mu(x,a)\leq b$. But it also means that we can find the smallest $x$ such that $b\leq\tau(a,x)$ or $b\leq\tau(x,a)$. This is because, $\mu_{\_}{\gamma a}$ is the left adjoint of $\tau^{a}$, and $\mu^{\gamma a}$ is the left adjoint of $\tau_{\_}{a}$. For all examples we will discuss, source multiplication plays the role of the usual composition operation of the theory. But preordered heaps make it clear that $\mu$ and $\tau$ are closely related operations. In fact, preordered heaps generalize De Morgan’s identities (see section 2.2). Thus, while inequalities of the form $\mu(a,x)\leq b$ are more common in the literature, preordered heaps indicate that we can also solve inequalities of the form $b\leq\tau(a,x)$. As we will see, for some theories there is clear understanding of how target multiplication can be used, but for others its use is unknown.

In the definition of a preordered heap, we did not assume that source multiplication has an identity. Here we consider briefly what happens when it does. Multiplicative identities are common, and in fact, there exists a multiplicative identity in all compositional theories we know.

Suppose $P$ is a preordered heap and $e\in P$ is a left identity for source multiplication, i.e., $\mu_{e}\simeq\text{id}$. By Theorem 2.2, $(\text{id},\tau^{\gamma e})$ is an adjoint pair. The right adjoint of id is id. Since adjoints are unique up to isomorphism, $\tau^{\gamma e}\simeq\text{id}$. This means that $\gamma e$ is a right identity element for $\tau$. Moreover, in view of (2), $\tau_{\gamma e}\simeq\text{id}$. By Theorem 2.2, $(\mu^{e},\text{id})$ is an adjoint pair. By the same reasoning just followed, we must have $\mu^{e}\simeq\text{id}$. We record this result:

Assume-guarantee contracts are an algebra and a methodology to support compositional system design and analysis. Fix once and for all a set $B$ whose elements we call behaviors. Subsets of $B$ are referred to as behavioral properties or trace properties. An AG contract is a pair of properties $C=(A,G)$ satisfying $A\boldsymbol{\cup}G=B$. Contracts are used as specifications: a component adheres to contract $C$ if it meets the guarantees $G$ when instantiated in an environment that satisfies the assumptions $A$. The specific form of these properties is not our concern now; we are only interested in the algebraic definitions. The algebra of assume-guarantee contracts was introduced by R. Negulescu [33] (there called process spaces) to deal with assume-guarantee reasoning for concurrent programs. The algebra was reintroduced, together with a methodology for system design, by Benveniste et al. [5] to apply assume-guarantee reasoning to the design and analysis of any engineered system. Now we describe the operations of this algebra.

For $C^{\prime}=(A^{\prime},G^{\prime})$ another contract, the partial order of AG contracts, called refinement, is given by $C\leq C^{\prime}$ when $G\subseteq G^{\prime}$ and $A\supseteq A^{\prime}$. The involution of AG contracts, called reciprocal, is given by $\gamma C=(G,A)$. This operation is clearly antitone and meets axiom A1. Source multiplication is contract composition: $\mu(C,C^{\prime})=\left(A\boldsymbol{\cap}A^{\prime}\boldsymbol{\cup}\neg(G\boldsymbol{\cap}G^{\prime}),G\boldsymbol{\cap}G^{\prime}\right)$. This operation yields the tightest contract obeyed by the composition of two design elements, each obeying contracts $C$ and $C^{\prime}$, respectively. Composition is monotonic in the refinement order of AG contracts. We need to verify the admissibility conditions. Since source multiplication for AG contracts is commutative, we verify (1):

	$\displaystyle(\mu_{C}$	$\displaystyle\circ\gamma)^{2}C^{\prime}=(\mu_{C}\circ\gamma)\circ(\mu_{C})(G^{\prime},A^{\prime})=\mu_{C}(G\boldsymbol{\cap}A^{\prime},A\boldsymbol{\cap}G^{\prime}\boldsymbol{\cup}\neg(G\boldsymbol{\cap}A^{\prime}))$
		$\displaystyle=(A\boldsymbol{\cap}G\boldsymbol{\cap}A^{\prime}\boldsymbol{\cup}\neg G\boldsymbol{\cup}\neg(A\boldsymbol{\cap}G^{\prime}\boldsymbol{\cup}\neg A^{\prime}),G\boldsymbol{\cap}(A\boldsymbol{\cap}G^{\prime}\boldsymbol{\cup}\neg A^{\prime}))$
		$\displaystyle=(A\boldsymbol{\cap}A^{\prime}\boldsymbol{\cup}\neg G\boldsymbol{\cup}\neg A\boldsymbol{\cap}A^{\prime}\boldsymbol{\cup}\neg G^{\prime}\boldsymbol{\cap}A^{\prime},G\boldsymbol{\cap}(A\boldsymbol{\cap}G^{\prime}\boldsymbol{\cup}\neg A^{\prime}))$
		$\displaystyle=(A^{\prime}\boldsymbol{\cup}\neg G,G\boldsymbol{\cap}(A\boldsymbol{\cap}G^{\prime}\boldsymbol{\cup}\neg A^{\prime}))\leq(A^{\prime},G^{\prime})=C^{\prime},$

where in the last step we used the fact that $\neg A^{\prime}\subseteq G^{\prime}$, which follows from $A^{\prime}\boldsymbol{\cup}G^{\prime}=B$. We conclude that AG contracts satisfy the admissibility conditions, and thus have preordered heap structure.

What is target multiplication for AG contracts? From its definition, we have $\tau(C,C^{\prime})=\gamma\circ\mu\circ(\gamma C,\gamma C^{\prime})=\gamma\circ\mu\left((G,A),(G^{\prime},A^{\prime})\right)=\left(A\boldsymbol{\cap}A^{\prime},G\boldsymbol{\cap}G^{\prime}\boldsymbol{\cup}\neg(A\boldsymbol{\cap}A^{\prime})\right)$. This is an operation on contracts called merging. One of the main objectives of the theory of assume-guarantee contracts is to deal with multiple viewpoints, i.e., a multiplicity of design concerns, each having a contract representing the specification for that concern (e.g., functionality, timing, etc.). In [35], it is argued that the operation of merging is used to bring multiple viewpoint specifications into a single contract object.

Since AG contracts are preordered heaps, we get their quotient formulas from Theorem 2.2. The adjoint of $\mu_{C^{\prime}}$ is $\tau^{\gamma C^{\prime}}=\gamma\circ\mu^{C^{\prime}}\circ\gamma$. Applying this to $C$ yields $\tau^{\gamma C^{\prime}}(C)=\gamma\circ\mu^{C^{\prime}}(G,A)=(A\boldsymbol{\cap}G^{\prime},G\boldsymbol{\cap}A^{\prime}\boldsymbol{\cup}\neg(A\boldsymbol{\cap}G^{\prime}))$. This closed-form expression for the quotient of AG contracts was first reported in [38]. Also by Theorem 2.2, the left adjoint of merging by a fixed contract $C^{\prime}$ is the operation $\mu(C,\gamma C^{\prime})=\mu\left((A,G),(G^{\prime},A^{\prime})\right)=\left(A\boldsymbol{\cap}G^{\prime}\boldsymbol{\cup}\neg(G\boldsymbol{\cap}A^{\prime}),G\boldsymbol{\cap}A^{\prime}\right)$. This operation was recently introduced under the name of separation in [35].

We show that Interface Automata as introduced in [16] have preordered heap structure. To achieve this result, we first provide the relevant definitions for interface automata. All definitions match those of  [16], except for our definition of alternating simulation for interface automata.

An interface automaton $P=\langle V_{\_}P,V_{\_}P^{\text{init}},\mathcal{A}_{\_}P^{I},\mathcal{A}_{\_}P^{O},\mathcal{A}_{\_}P^{H},\mathcal{T}_{\_}P\rangle$ consists of the following elements:

• •

  $V_{\_}P$ is a set of states.

• •

  $V_{\_}P^{\text{init}}\subseteq V_{\_}P$ is a set of initial states. Following [16], we require that $V_{\_}P^{\text{init}}$ contains at most one state.

• •

  $\mathcal{A}_{\_}P^{I},\mathcal{A}_{\_}P^{O}$, and $\mathcal{A}_{\_}P^{H}$ are mutually disjoint sets of input, output, and internal actions. We denote by $\mathcal{A}_{\_}P=\mathcal{A}_{\_}P^{I}\boldsymbol{\cup}\mathcal{A}_{\_}P^{O}\boldsymbol{\cup}\mathcal{A}_{\_}P^{H}$ the set of all actions.

• •

  $\mathcal{T}_{\_}P\subseteq V_{\_}P\times\mathcal{A}_{\_}P\times V_{\_}P$ is a set of steps.

Following [16], if $a\in\mathcal{A}_{\_}P^{I}$ (resp. $a\in\mathcal{A}_{\_}P^{O}$, $a\in\mathcal{A}_{\_}P^{H}$), then $(v,a,v^{\prime})$ is called an input (resp. output, internal) step. We denote by $\mathcal{T}_{\_}P^{I}$ (resp. $\mathcal{T}_{\_}P^{O}$, $\mathcal{T}_{\_}P^{H}$) the set of input (resp. output, internal) steps. An action $a\in\mathcal{A}_{\_}P$ is enabled at a state $v\in V_{\_}P$ if there is a step $(v,a,v^{\prime})\in\mathcal{T}_{\_}P$ for some $v^{\prime}\in V_{\_}P$. We indicate by $\mathcal{A}_{\_}P^{I}(v),\mathcal{A}_{\_}P^{O}(v),\mathcal{A}_{\_}P^{H}(v)$ the subsets of input, output, and internal actions that are enabled at the state $v$, and we let $\mathcal{A}_{\_}P(v)=\mathcal{A}_{\_}P^{I}(v)\boldsymbol{\cup}\mathcal{A}_{\_}P^{O}(v)\boldsymbol{\cup}\mathcal{A}_{\_}P^{H}(v)$.

We call illegal those states of the product in which one of the interface automata can take a step through a shared action, but the other can’t. These states are removed from the product in the definition of composition of interface automata. Given two composable interface automata $P$ and $Q$, the set $\textsf{Illegal}(P,Q)$ $\subseteq$ $V_{\_}P\times V_{\_}Q$ of illegal states of $P\otimes Q$ is given by

$$\textsf{Illegal}(P,Q)=\left\{{(v,u)\in V_{\_}P\times V_{\_}Q}\,\,\middle|\,\,{\exists a\in\textsf{shared}(P,Q).\left(\begin{array}[]{c}a\in\mathcal{A}_{\_}P^{O}(v)\wedge a\notin\mathcal{A}_{\_}Q^{I}(u)\\ \vee\\ a\in\mathcal{A}_{\_}Q^{O}(u)\wedge a\notin\mathcal{A}_{\_}P^{I}(v)\\ \end{array}\right)}\right\}.$$

An environment for an interface automaton $R$ is an interface automaton $E$ such that $E$ is composable with $R$, $E$ is nonempty, $\mathcal{A}_{\_}E^{I}=\mathcal{A}_{\_}R^{O}$, and $\textsf{Illegal}(R,E)=\emptyset$. A legal environment for the pair $(P,Q)$ is an environment for $P\otimes Q$ such that no state in $\textsf{Illegal}(P,Q)\times V_{\_}E$ is reachable in $(P\otimes Q)\otimes E$. We say that a pair $(v,u)\in V_{\_}P\times V_{\_}Q$ of states is compatible if there is an environment $E$ for $P\otimes Q$ such that no state in $\textsf{Illegal}(P,Q)\times V_{\_}E$ is reachable in $(P\otimes Q)\otimes E$ from the state $\{(v,u)\}\times V_{\_}E^{\text{init}}$. Two interface automata $P$ and $Q$ are compatible if the initial state $(v,u)\in V_{\_}P^{init}\times V_{\_}Q^{init}$ is compatible. We write $\textsf{Cmp}(P,Q)$ for the set of compatible states of $P\otimes Q$. With these notions, we can define parallel composition for interface automata.

Given two compatible interface automata $P$ and $Q$, the composition $P\parallel Q$ is an interface automaton with the same action sets as $P\otimes Q$. The states are $V_{\_}{P\parallel Q}=\textsf{Cmp}(P,Q)$; the initial states are $V_{\_}{P\parallel Q}^{\text{init}}$ $=$ $V_{\_}{P\otimes Q}^{\text{init}}\boldsymbol{\cap}\textsf{Cmp}(P,Q)$; and the steps are $\mathcal{T}_{\_}{P\parallel Q}$ $=$ $\mathcal{T}_{\_}{P\otimes Q}$ $\boldsymbol{\cap}$ $(\textsf{Cmp}(P,Q)\times\mathcal{A}_{\_}{P\parallel Q}\times\textsf{Cmp}(P,Q))$.

Let $v\in V_{\_}P$, the set $\textsf{IntReach}_{\_}P(v)$ is the smallest set $U\subseteq V_{\_}P$ such that $v\in U$ and if $u\in U$ and $(u,a,u^{\prime})\in\mathcal{T}_{\_}P^{H}$, then $u^{\prime}\in U$. Moreover, we let

$$\textsf{ExtEn}_{\_}P^{O}(v)=\bigcup_{\_}{u\in\textsf{IntReach}(v)}\mathcal{A}_{\_}P^{O}(u)\quad\text{and}\quad\textsf{ExtEn}_{\_}P^{I}(v)=\bigcup_{\_}{u\in\textsf{IntReach}(v)}\mathcal{A}_{\_}P^{I}(u)$$

be the sets of externally enabled output and input actions, respectively, at $v$. And for all externally enabled input and output actions $a\in\textsf{ExtEn}_{\_}P^{I}(v)\boldsymbol{\cup}\textsf{ExtEn}_{\_}P^{O}(v)$, we let

$$\textsf{ExtDest}_{\_}P(v,a)=\left\{{u^{\prime}}\,\,\middle|\,\,{\exists(u,a,u^{\prime})\in\mathcal{T}_{\_}P.\,\,u\in\textsf{IntReach}_{\_}P(v)}\right\}.$$

With these notions, we can define an alternating simulation between interface automata.

Now we use the notion of alternating simulation to establish a preorder for interface automata: the interface automaton $Q$ refines the interface automaton $P$, written $Q\preceq P$, if $\mathcal{A}_{\_}P^{I}\subseteq\mathcal{A}_{\_}Q^{I}$, $\mathcal{A}_{\_}P^{O}\supseteq\mathcal{A}_{\_}Q^{O}$, and there is an alternating simulation $\preceq$ from $Q$ to $P$, a state $v\in V_{\_}P^{\text{init}}$, and a state $u\in V_{\_}Q^{\text{init}}$ such that $u\preceq v$.

Let $P=\langle V_{\_}P,V_{\_}P^{\text{init}},A_{\_}P^{I},A_{\_}P^{O},A_{\_}P^{H},T_{\_}P\rangle$ be an interface automaton. The mirror of $P$, denoted $P^{\top}$, is given by $P^{\top}=\langle V_{\_}P,V_{\_}P^{\text{init}},A_{\_}P^{O},A_{\_}P^{I},A_{\_}P^{H},T_{\_}P\rangle$. The mirror operation is clearly an involution, i.e., $\left(P^{\top}\right)^{\top}=P$. Let the source multiplication $\mu$ be the parallel composition of interface automata, $\gamma$ be the mirror operation, and let the preorder be refinement. We state the main claim of this section:

Since interface automata have preordered heap structure, for given interface automata $P$ and $Q$, Theorem 2.2 enables us to find largest solutions $R$ for equations of the form $\mu(Q,R)\leq P$. The quotient for interface automata was first reported in [7]. Now that we know interface automata have preordered heap structure, we can ask: what is target multiplication for interface automata? The operation is given by $\tau(P,Q)=\left(P^{\top}\parallel Q^{\top}\right)^{\top}$. We propose to call this operation merging in analogy to the case of AG contracts. Similarly, by Theorem 2.2, merging by fixed $Q$, $\tau_{\_}{Q}$, has a left adjoint given by $\mu^{\gamma Q}(P)=P\parallel Q^{\top}$. For the same reason, we propose to call this binary operation separation. In AG contracts, merging and separation are used to handle multiple viewpoints in a design. To the best of our understanding, the notion of handling multiple design viewpoints has not been discussed for interface automata. Maintaining the analogy to AG contracts, we suspect that merging and separation here defined provide interface automata the ability to handle these multiple viewpoints. Exploring this idea is material for future work.