Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Labelled Transition Systems (LTSs) [15] are a formalism for modelling and reasoning about system behaviour. Modal Transition Systems (MTSs) [17] are an extension of LTSs that distinguishes between required, prohibited and possible transitions, allowing a model to be only partially specified. MTSs come equipped with the notion of refinement, supporting a development process where abstract model specifications can be gradually refined into more concrete ones, until a fully defined model – an LTS – is obtained. An MTS thus serves as a specification for a set of LTSs – its implementations.

Refinement of MTSs was investigated along two different dimensions. The first examines modal vs. thorough refinements [1, 2, 16]. Given MTSs M and N, we say that N modally refines M if there exists a relation R between the states of M and N such that required transitions in M are simulated by N, and possible transitions from N are simulated by M. In contrast, N thoroughly refines M if its set of implementations (denoted by \([\![ N ]\!]\)) is a subset of \([\![ M ]\!]\). Modal refinement is sound but not complete with respect to implementations. That is, if N modally refines M then \([\![ N ]\!]\) \(\subseteq \) \([\![ M ]\!]\), but the opposite does not always hold [16]. Thorough refinement however, is much more complex to determine (EXPTIME-complete for thorough refinement vs. PTIME-complete for modal refinement [6]), making modal refinement more attractive for practical applications.

The second dimension of MTS refinement is that of refinement flavour. Three different flavours have been defined for refinement of MTSs: strong [17], where required transitions in the original model must exist in the refined model; observational [11, 14], where unobservable (\(\tau \)-labelled) transitions are taken into account; and alphabet refinement [12], where MTSs defined on different sets of labels can be compared. In an alphabet refinement, labels in one MTS that are not known to the other MTS are being hidden, by replacing them with \(\tau \) transitions. An observational refinement is then used for the comparison.

The first part of this paper deals with the refinement definition of an extension of MTSs, known as Disjunctive MTSs (DMTSs) [18]. In a DMTS, a disjunction of required transitions can be defined, increasing the expressiveness of model specifications. DMTSs have been attracting growing attention in recent years. Their conjunction as well as model checking were considered in [4], and structural refinement was defined for them in [7]. Different variants of DMTSs have been defined and analyzed [8, 9, 19], and DMTSs are treated as first-class citizens in the family of transition systems [1, 5, 16].

Yet, to the best of our knowledge, modal observational refinement of DMTSs was never fully defined. While strong refinement was already given in [18], where DMTSs were first introduced, we found only two places in the literature where observational refinement of DMTSs was considered. In [19] the authors proposed a modal observational refinement definition for a subset of DMTS called dMTS, where all transitions of a single disjunct must have the same label. \(\tau \)-labels were allowed on “possible” transitions only. In [3], we proposed an observational implementation definition. Using that definition, a model L was said to be a refinement of a DMTS M only if L was an LTS (making it a thorough refinement definition). \(\tau \)-transitions were allowed to exist only in L and not in M. Modal observational refinement for full DMTSs is thus still missing from the literature.

Such a definition is the first contribution of our paper. We provide the definition, which is subtle and non-trivial, and prove that it agrees with the relevant definitions from the literature. Specifically, we prove that it agrees with [3] when implementations are concerned; with strong refinement of DMTS [18] when the compared models have no \(\tau \)-transitions; and with observational refinement of MTSs [14] when models compared are MTSs. Most importantly, we prove that our definition is sound with respect to implementations.

The second part of the paper deals with the operation of conjunction, or merge of modal transition systems. Given two models, it is often desirable to compute a new model that captures all of their common implementations. Such an operation supports independent development of different aspects of an intended behaviour, followed by the composition of them into a single model that accurately captures all aspects. The merge of two (D)MTSs M and N is a (D)MTS that is a common refinement of both, and is the least refined one. Thus it is sometimes called the least common refinement or the LCR.

Merge has been investigated in the literature for MTSs as well as for DMTSs, for strong, observational and alphabet refinements [3, 4, 10, 12, 13, 19, 20]. It was shown that MTSs are not closed for merge under strong refinement [10, 13] (which implies that they are not closed under observational and alphabet merges as well, since observational merge must agree with strong merge when no \(\tau \)-transitions are involved). For DMTSs, a strong merge algorithm was given in [4]. Observational merge however, was only considered for the restricted subset of dMTS where \(\tau \)-labels are allowed on possible transitions only [19].

Our second contribution is thus an observational merge algorithm for DMTS. Using our new observational refinement definition, we show that the strong merge algorithm of [4] can be naturally extended to support observational merge as well.

Our third contribution deals with minimal common refinements (MCRs) [20] under alphabet refinement. An MCR of two models M and N is a common refinement P of them such that no other common refinement is less refined than it. Other common refinements may exist though, that are incomparable with P. For cases where a least common refinement (LCR) does not exist, it was suggested that the merge of two models could be represented by a (possibly infinite) set of MCRs. Algorithms for finding MCRs in special cases were proposed in [10, 12, 20], for strong as well as for alphabet merge. It was assumed that, unlike LCR, an MCR of two models always existed (given that the models are consistent, i.e., they have at least one implementation in common). We prove this assumption to be wrong: we give an example of two DMTSs that, although consistent, do not have an MCR under alphabet refinement.

Table 1 summarizes the known results for refinement and merge of MTSs and DMTSs. We use ‘(?)’ to indicate the parts that were missing before this paper, and mark our results in blue.

Table 1. Known results for MTS and DMTS. Our contributions are indicated by (?).
Full size table

The rest of the paper is organized as follows. In Sect. 2 we give preliminary definitions. We present observational refinement of DMTSs in Sect. 3, and then answer positively the question of merge for DMTSs under observational refinement (Sect. 4). Section 5 answers negatively the question of the existence of an MCR under alphabet refinement. We conclude the paper in Sect. 6. Proofs of most theorems are omitted due to lack of space.

2 Preliminaries

2.1 LTSs and MTSs

All models considered in this paper are finite-state, where the set of states, the set of labels and the set of transitions are all finite.

We start with the concept of Labelled Transition Systems (LTSs) [15] which are commonly used for modeling concurrent systems.

Definition 1

(LTS [15]). A Labeled Transition System (LTS) is a structure \((S, L, \delta , s^0)\), where S is a set of states, L is a set of labels, \( \delta \subseteq (S \times L \times S)\) is the transition relation, and \(s^0\in S\) is the initial state.

Modal Transition Systems (MTSs) [17] are used to specify sets of LTSs. An MTS distinguishes between two types of transitions – possible and required. Transitions that do not appear at all are considered to be prohibited.

Definition 2

(MTS [17]). A Modal Transition System (MTS) M is a structure \((S, L, \delta ^p, \delta ^r, s^0)\), where S is a set of states, L is a set of labels, \(s_0\in S\) is the initial state, \( \delta ^p \subseteq (S \times L \times S)\) is the possible transition relation, \( \delta ^r \subseteq (S \times L \times S)\) is the required transition relation. In addition, it is required that \( \delta ^r \subseteq \delta ^p\).

Note that in an MTS, every ‘required’ transition is also ‘possible’. When the required and possible transitions coincide, the MTS is actually an LTS.

We use the notation \(m \mathop {\longrightarrow _{p}}\limits ^{\ell } m'\) to denote a possible transition \((m,\ell ,m')\in \delta ^p\), and \(m \mathop {\longrightarrow _r}\limits ^{\ell } m'\) to denote a required transition \((m,\ell ,m')\in \delta ^r\). In figures, we use \(m \mathop {\longrightarrow }\limits ^{\ell ?} m'\) for a possible transition and \(m \mathop {\longrightarrow }\limits ^{\ell } m'\) for a required transition. If the model is an LTS, all transitions are simply \(i \mathop {\longrightarrow }\limits ^{\ell } i'\).

Strong refinement for MTSs has been defined by Larsen and Thomsen [17].

Definition 3

(Strong Modal Refinement of MTS [17]). Let \(M=(S_M, L, \delta ^p_M,\) \(\delta ^r_M, m^0)\) and \(N=(S_N, L, \delta ^p_N,\) \(\delta ^r_N, n^0)\) be MTSs. We say that N is a strong refinement of M (denoted M \(\preceq _s\) N) if there exists a strong refinement relation \(R_s\subseteq S_M\times S_N\), such that \((m^0,n^0)\in R_s\) and if \((m,n)\in R_s\) then

  1. 1.

    for every transition \((n \mathop {\longrightarrow _{p}}\limits ^{\ell } n')\) in N, there exists a transition \((m \mathop {\longrightarrow _{p}}\limits ^{\ell } m')\) in M such that \((m^\prime , n^\prime )\in R_s\); and

  2. 2.

    for every transition \((m \mathop {\longrightarrow _r}\limits ^{\ell } m')\) in M, there exists \( (n \mathop {\longrightarrow _r}\limits ^{\ell } n')\) in N such that \((m',n')\in R_s\).

Since every LTS is also an MTS, we can compare MTSs and LTSs using modal refinement. Let M be an MTS and I be an LTS. We say that I is an implementation of M if M \(\preceq _s\) I. The set of all implementations of a model M is denoted by \([\![ M ]\!]\). An MTS N is said to thoroughly refine a model M if \([\![ N ]\!]\) \(\subseteq \) \([\![ M ]\!]\). As mentioned above, modal refinement is sound with respect to implementations: M \(\preceq _s\) N implies \([\![ N ]\!]\) \(\subseteq \) \([\![ M ]\!]\), but it is not complete [16].

Adding Unobservable Actions. MTSs have also been considered in a situation where some of the actions are internal (labeled \(\tau \)), and are unobservable to the outside viewer. When \(\tau \)-transitions are present, we use a relaxed, observational, version of refinement, allowing a finite sequence of \(\tau \)-transitions to exist between observable ones. Huttel and Larsen [14] were the first to suggest an observational refinement for MTSs. Fischbein et al. [10, 11] demonstrated some unintuitive phenomena allowed by the definition of [14], and proposed a different, more intuitive observational refinement, which we adopt here.

We use \(L_{\tau }\) to denote the set of labels \(L\cup \{\tau \}\). We use \(m\mathop {\longrightarrow _r}\limits ^{\hat{\ell }} m^\prime \) (or \(m\mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} m^\prime \)) to mean that either \(\ell \not = \tau \) and \(m\mathop {\longrightarrow _r}\limits ^{\ell } m^\prime \) (\(m\mathop {\longrightarrow _{p}}\limits ^{\ell } m^\prime \)) holds, or \(\ell =\tau \) and \(m=m'\). If \(\ell =\tau \), no transition (and therefore no label) exists at all. Note that \(\hat{\ell }\) can never be \(\tau \).

Definition 4

(Observational Modal Refinement of MTSs [10]). Let \(M=(S_M, L_\tau , \delta ^p_M, \delta ^r_M, m^0)\) and \(N=(S_N, L_\tau , \delta ^p_N, \delta ^r_N, n^0)\) be MTSs. We say that N is an observational refinement of M, denoted \(M \preceq _{\mathrm {o}}N\), if there exists a relation \(R_o\subseteq S_M\times S_N\) such that \((m^0,n^0) \in R_o\), and whenever \((m,n)\in R_o\), we have:

  1. 1.

    for every \((n\mathop {\longrightarrow _{p}}\limits ^{\ell } n^\prime )\) in N, there exists a sequence of transitions in M: \(m_0 \mathop {\longrightarrow _{p}}\limits ^{\tau } m_1 \mathop {\longrightarrow _{p}}\limits ^{\tau } \cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } m_j \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} m'\), such that \(m=m_0\), \((m_k, n) \in R_o\) for \(0\le k \le j\), and \((m', n') \in R_o\); and

  2. 2.

    for every \((m\mathop {\longrightarrow _r}\limits ^{\ell } m^\prime )\) in M, there exist a sequence of transitions in N: \(n_0 \mathop {\longrightarrow _r}\limits ^{\tau } n_1 \mathop {\longrightarrow _r}\limits ^{\tau } \cdots \mathop {\longrightarrow _r}\limits ^{\tau } n_j \mathop {\longrightarrow _r}\limits ^{\hat{\ell }} n'\), such that \(n=n_0\), \((m, n_k) \in R_o\) for \(0\le k \le j\), and \((m', n') \in R_o\).

Note that by Definition 4, a refining \(\tau \)-sequence can be of length 0. If \(\ell =\tau \), then no refining transition is required to exist at all. Like in the strong refinement case, if I is an LTS and \(M \preceq _{\mathrm {o}}N\), we say that I is an observational implementation of M. The set of observational implementations of M is denoted by \([\![ M ]\!]\) \(_o\). N is a thorough observational refinement of M iff \([\![ N ]\!]\) \(_o\) \(\subseteq \) \([\![ M ]\!]\) \(_o\).

2.2 DMTSs

Disjunctive Modal Transition Systems (DMTSs) [18] extend MTS by allowing required transitions to be disjunctive.

Definition 5

(DMTS [18]). A Disjunctive Modal Transition System (DMTS) M is a structure \((S, L, \delta ^p, \varDelta ^r, s^0)\), where S is a set of states, L is a set of labels, \( \delta ^p \subseteq (S \times L \times S)\) is the possible transition relation, \( \varDelta ^r \subseteq (S \times 2^{L \times S})\) is the disjunctive required transition relation, and \(s^0\in S\) is the initial state.

We denote a disjunctive required transition in \( \varDelta ^r\) by \(\langle s,V \rangle \), where V is a set of pairs \(V = \{(l_1,s_1),\ldots ,(l_n,s_n)\}\) with \(l_1,\ldots ,l_n\in L\) and \(s_1,\ldots ,s_n\in S\). A disjunct \((l_i,s_i)\in V\) is sometimes called a leg, and the entire disjunctive transition – a DT. In figures, a disjunction between transitions is shown using a bullet. For example, is a DT with two legs, on a and b. For example, Fig. 1 shows a DMTS \({\mathsf A}\). It has two DTs emanating from state 0: one with two legs, on labels c and \(\tau \), and the other with 3 legs, on labels b, \(\tau \) and c.

We follow [4] to require also that (1) if \(\langle s,V \rangle \in \varDelta ^r\) then V is not empty, and (2) for all \(\langle s,V \rangle \in \varDelta ^r\) and \((\ell ,s')\in V\), we have that \((s,\ell , s')\in \delta ^p\). That is, every leg in every DT is possible in the model.

A DMTS N strongly refines a DMTS M, if, roughly speaking, every possible transition in N is also possible in M (like in the MTS case), and if for every DT in M, there exists a DT in N with at least one leg from the original DT.

Definition 6

(Strong Modal Refinement of DMTS [18]). Let \(M=(S_M, L, \delta ^p_M,\) \(\varDelta ^r_M, m^0)\) and \(N=(S_N, L, \delta ^p_N,\) \(\varDelta ^r_N, n^0)\) be DMTSs. We say that N is a strong refinement of M, denoted \(M \preceq _{\mathrm {S}}N\), if there exists a strong refinement relation \(R_S\subseteq S_M\times S_N\), such that \((m^0,n^0)\in R_S\), and if \((m,n)\in R_S\) then

  1. 1.

    for every possible transition \((n \mathop {\longrightarrow _{p}}\limits ^{\ell } n')\) in N, there exists a transition \((m \mathop {\longrightarrow _{p}}\limits ^{\ell } m')\) in M such that \((m^\prime , n^\prime )\in R_S\); and

  2. 2.

    for every DT \(\langle m,V \rangle \in \varDelta ^r_M\), there exists a DT \(\langle n,U \rangle \in \varDelta ^r_N\), such that for every leg \((\ell , n')\in U\) there exists a leg \((\ell , m')\in V\) with \((m',n')\in R_S\).

Like in the MTS case, we now consider models with \(\tau \)-transitions. A DT \(\langle m,V \rangle \) can thus include legs \((\tau ,m')\in V\). To the best of our knowledge, modal observational refinement for DMTSs has not been defined and we do so in Sect. 3.

[3] defined observational implementation for DMTSs, thereby handling the case where the refining model is an LTS:

Definition 7

(Observational Implementation of DMTSs [3]). Let \(M= (S_M, L_\tau , \delta ^p_M, \varDelta ^r_M, m^0)\) be a DMTS and \(I=(S_I, L_\tau , \delta _I, i^0)\) be an LTS. We say that I is an observational implementation of M if there exists an observational implementation relation \(R_{OI}\subseteq S_M\times S_I\), such that \((m^0,i^0)\in R_{OI}\), and for all \((m,i) \in R_{OI}\) the following hold:

  1. 1.

    for every transition \(i \mathop {\longrightarrow }\limits ^{\ell } i'\) in I, there exists a sequence of possible transitions in M, \(m_0 \mathop {\longrightarrow _{p}}\limits ^{\tau } m_1 \mathop {\longrightarrow _{p}}\limits ^{\tau } \ldots \mathop {\longrightarrow _{p}}\limits ^{\tau } m_j \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} m'\), such that \(m=m_0\), \((m_k, i) \in R_{OI}\) for \(0\le k \le j\), and \((m', i') \in R_{OI}\); and

  2. 2.

    for every DT \( \langle m,V \rangle \in \varDelta ^r_M\), there exists a sequence of transitions in I, \(i_0 \mathop {\longrightarrow }\limits ^{\tau } i_1 \mathop {\longrightarrow }\limits ^{\tau } \ldots \mathop {\longrightarrow }\limits ^{\tau } i_j \mathop {\longrightarrow }\limits ^{\hat{\ell }} i'\), such that \(i=i_0\), \((m, i_k) \in R_{OI}\) for \(0\le k \le j\), and there exists a leg \( (\ell ,m')\in V\) such that \((m',i') \in R_{OI}\).

Both strong and observational refinements compare models that are defined on the same set of labels (alphabet). Yet it is often useful to consider models that share only a subset of their alphabets [20]. We do that via alphabet refinement: we first hide labels of N that are unknown to M, by replacing them with \(\tau \)’s, and then use observational refinement to compare them.

Definition 8

(Hiding). Let \(M = (S_M, \alpha M, \delta ^p,\varDelta ^r, m^0)\) be a DMTS and X be a set of labels. M with the labels of X hidden, denoted \(M \diagdown X\), is a DMTS \((S_M, (\alpha M \setminus X) \cup \{\tau \}\), \(\delta ^{p}_1\), \(\varDelta ^{r}_1\), \(m^0)\), where \(\varDelta ^{r}_1\) is derived from \(\varDelta ^{r}\) by replacing every leg \((\ell ,m')\in V\) in a DT \(\langle m,V \rangle \in \varDelta ^{r}\), with a leg \((\tau ,m')\) if and only if \(\ell \in X\). The set \(\delta ^{p}_1\) is derived from \(\delta ^{p}\) in the same way, replacing possible transitions \(m\mathop {\longrightarrow _{p}}\limits ^{\ell }m'\) by \(m\mathop {\longrightarrow _{p}}\limits ^{\tau }m'\) if and only if \(\ell \in X\). For a set of labels Y, we use M@Y to denote \(M \diagdown (\alpha M \setminus Y)\).

Definition 9

(Alphabet Refinement [20]). A (D)MTS \(N=(S_N, L_N, \delta ^p_N,\) \(\varDelta ^r_N, n^0)\) is an alphabet refinement of a DMTS \(M=(S_M, L_M, \delta ^p_M,\) \(\varDelta ^r_M, m^0)\), denoted \(M\preceq _{\mathrm {A}}N\), if \(L_M \subseteq L_N\) and \(N@L_M\) is an observational refinement of M.

2.3 Merge

A merge of two models M and N is a common refinement of M and N that is the least refined. The merge of two models is therefore also called their least common refinement (LCR). For thorough refinement, the merge is a model P such that \([\![ P ]\!]\) = \([\![ M ]\!]\) \(\cap \) \([\![ N ]\!]\). For modal refinement, we look for P such that \(M\preceq P\) and \(N\preceq P\), and for every other common refinement Q, we have that \(P\preceq Q\) (where \(\preceq \) can be a strong, observational or alphabet refinement relation). In practice, there are many cases where an LCR does not exist. To relax the requirement of an LCR, the concept of a minimal common refinement (MCR) [20] was introduced. P is an MCR of M and N if there does not exist a common refinement that is less refined than P. There could, however, exist common refinements that are incomparable to P.

MTSs are not closed for merge (no LCR and no MCR) for strong refinement [10, 13]. This implies that they are not closed for observational and alphabet refinements as well, since if an observational merge algorithm were to exist for MTSs, it would also have to apply to the case with no \(\tau \)-transitions. Note that the other direction does not hold: if a merge over a strong refinement exists, it does not imply the existence of its counterpart for observational or alphabet refinement.

DMTSs were shown to be closed for strong merge [4]. Note that the existence of an LCR implies the existence of an MCR, but the other direction does not hold. It was shown that DMTSs are not closed for alphabet merge (no LCR exists) [3].

3 Observational Refinement of DMTS

In this section, we define modal observational refinement for DMTSs, a notion that we found missing from the literature. In Sect. 3.1, we define observational refinement for DMTS, and in Sect. 3.2, we provide “sanity checks” showing that our observational refinement is a reasonable extension of existing definitions.

3.1 Observational Refinement Definition

In the MTS world, the difference between strong and observational refinements is that a finite path of \(\tau \)-transitions is allowed to occur before a transition labelled \(\ell \) (see Definition 4). In the DMTS world, for strong refinement, a disjunctive transition replaces MTS’s required transition. For the observational case for DMTSs, we introduce a new construction which we call a disjunctive cone.

We start with defining a must path.

Definition 10

(Must Path). Let \(M=(S, L_\tau , \delta ^p, \varDelta ^r, s)\) be a DMTS, and let \(x_0, x'\in S\) be states. A must path of length i from \(x_0\) to \(x'\) in M is a sequence of ‘legs’ \(x_0 \mathop {\longrightarrow }\limits ^{l_1} x_1 \mathop {\longrightarrow }\limits ^{l_2} \cdots \mathop {\longrightarrow }\limits ^{l_{i-1}} x_{i-1}\mathop {\longrightarrow }\limits ^{l_{i}} x^\prime \) such that there exist \(V_0, V_1, ..., V_{i-1} \in 2^{L_\tau \times S}\) with \(\langle x_0,V_0 \rangle \in \varDelta ^r\), \((l_1,x_1)\in V_0\), \(\langle x_1,V_1 \rangle \in \varDelta ^r\), \((l_2,x_2)\in V_1\), \(\cdots \), \(\langle x_{i-1},V_{i-1} \rangle \in \varDelta ^r\) and \((l_i,x')\in V_{i-1}\).

A must path \(\pi = x_0 \mathop {\longrightarrow }\limits ^{l_1} x_1 \mathop {\longrightarrow }\limits ^{l_2} \cdots \mathop {\longrightarrow }\limits ^{l_{i-1}} x_{i-1}\mathop {\longrightarrow }\limits ^{l_{i}} x^\prime \) is maximal in M if either \(x'=x_i\) for some \(x_i\) on \(\pi \) (that is, \(\pi \) has a loop), or if from \(x^\prime \) there is no outgoing required transition in M.

Definition 11

(Disjunctive Cone). Let \(M=(S, L_{\tau }, \delta ^p, \varDelta ^r, s^0)\) be a DMTS, and \(x \in S\) be a state. A disjunctive cone with a root x in M is a DMTS \(C_x = (S_c, L_{\tau },\delta ^p_c, \varDelta ^r_c,x)\) such that \(S_c\subseteq S\), \(\delta ^p_c\subseteq \delta ^p\), \(\varDelta ^r_c \subseteq \varDelta ^r\), and for every \(s\in S_c\) (1) there exists a must path from x to s, and (2) there exists at most one DT \(\langle s,V \rangle \in \varDelta ^r _c\).

A disjunctive cone \(C\subseteq M\) is a connected sub-model of M, where each state has a single (or none) outgoing DT. Note that each DT in M is either entirely in C or not at all (that is, all legs of the DT should be taken). A disjunctive cone is a natural extension of a path in MTS to the disjunctive setting of DMTS.

Since every DT may have \(\tau \)-legs, a disjunctive cone may have must paths that consist of only \(\tau \)-transitions. For a given disjunctive cone \(C_x\) with a root x, we denote the set of all maximal must paths in \(C_x\) that start at x and include only \(\tau \)-transitions by \(T_{C_x}\).

Example 1

(Disjunctive Cone). Consider a DMTS \(\mathsf B\) in Fig. 1. State 6 of \(\mathsf B\) has two outgoing DTs: \(\langle 6,\{(c,7)\} \rangle \) and \(\langle 6,\{(b,8),(\tau ,9)\} \rangle \). The sub-DMTSs \({\mathsf C}_6^1\subset {\mathsf B}\) and \({\mathsf C_6^2}\subset {\mathsf B}\) are two of \(\mathsf B\)’s disjunctive cones with root 6, each containing a single DT from 6.

Let \(\langle m,V \rangle \) be a DT in a DMTS M. When dealing with modal refinement, we have to compare it to a DT \(\langle n,U \rangle \) in a refining model N. As in the case of MTS, we use \((\hat{\ell },n')\in U\) to mean that either \(\ell \not =\tau \), or \(\ell =\tau \) and \(n'=n\). Here as well, \(\hat{\ell }\) itself can never be \(\tau \). Note, however, that if \((\hat{\ell },n')\in U\) is the single leg in U and if \(\ell =\tau \), then the leg \((\hat{\ell },n')\) does not actually exist, which makes U empty. This contradicts our requirement that a DT should never be empty. We thus use the notation DT* for a DT \(\langle n,U \rangle \) where U is potentially empty. Note that if a DT* \(\langle n,\emptyset \rangle \) observationally refines a DT \(\langle m,V \rangle \) via some observational refinement \(R_O\), it means that there exists a leg \((\tau ,m')\) in V such that \((m',n)\in R_O\).

We now introduce the main definition of the paper.

Definition 12

(Observational Refinement of DMTS). Let \(M=(S_M, L_{\tau }, \delta ^p_M,\) \(\varDelta ^r_M, m^0)\) and \(N=(S_N, L_{\tau }, \delta ^p_N,\) \(\varDelta ^r_N, n^0)\) be DMTSs. We say that N observationally refines M (\(M \preceq _{\mathrm {O}}N\)) if there exists an observational refinement relation \(R_O\subseteq S_M\times S_N\), such that \((m^0,n^0)\in R_O\), and if \((m,n)\in R_O\) then the following hold:

  1. 1.

    for every transition \((n\mathop {\longrightarrow _{p}}\limits ^{\ell } n^\prime )\) in N, there exists a possible path in M: \(m_0 \mathop {\longrightarrow _{p}}\limits ^{\tau } m_1\mathop {\longrightarrow _{p}}\limits ^{\tau } m_2 \mathop {\longrightarrow _{p}}\limits ^{\tau }\cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } m_j \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} m'\) such that \(m_0 = m\) and \((m_i, n) \in R_O\) for \(0\le i \le j\) and \((m',n') \in R_O\); and

  2. 2.

    for every DT \(\langle m,V \rangle \in \varDelta ^r_M\), there exists a disjunctive cone \(C_n \subseteq N\) with root n and set of \(\tau \)-paths \(T_{C_n}\), such that all paths in \(T_{C_n}\) are finite, and for every \(\pi = n_0\mathop {\longrightarrow _r}\limits ^{\tau }n_1\mathop {\longrightarrow _r}\limits ^{\tau }n_2 \mathop {\longrightarrow _r}\limits ^{\tau } \cdots \mathop {\longrightarrow _r}\limits ^{\tau }n_j\) in \(T_{C_n}\), for every \(n_i\) on \(\pi \) where \(0\le i \le j\),

    1. (a)

      \((m,n_i)\in R_O\), and

    2. (b)

      there exists a DT* \(\langle n_i,U_i \rangle \in \varDelta ^r_c\), such that for every leg \((\hat{\ell }, n_i^\prime )\in U_i\) there is a leg \((\ell , m')\in V\) with \((m',n^\prime _i)\in \mathcal{R}_O\).

Fig. 1.
figure 1

Example DMTSs. DMTS \(\mathsf B\) is an observational refinement of DMTS \(\mathsf A\). Sub-DMTSs \({\mathsf C}_6^1\subset {\mathsf B}\) and \({\mathsf C}_6^2 \subset {\mathsf B}\) are examples of disjunctive cones.

Full size image

The refining disjunctive cone in N for a DT \(\langle m,V \rangle \) consists of DTs that may have both \(\tau \)-labelled and \(\ell \)-labelled legs, with \(\ell \not = \tau \). All the \(\ell \)-labelled legs must have a corresponding leg in V. \(\tau \)-legs do not correspond to legs in V. Thus, if a DT includes only \(\tau \)-labelled legs, then it satisfies Condition 2(b) of Definition 12 vacuously, although the DT is not empty. This is because Condition 2(b) talks only about legs that are not labelled with \(\tau \). Note also that the DT \(\langle n_i,U_i \rangle \) must include the leg \((\tau ,n_{i+1})\) (for \(i<j\)), since \(n_i\) has at most one outgoing DT in \(C_n\). Paths with \(\tau \)-transitions are finite, guaranteeing that a DT with no \(\tau \)-legs is reached eventually on every \(\tau \)-path.

Example 2

(Observational Refinement). The DMTS \(\mathsf {B}\) in Fig. 1 is an observational refinement of the DMTS \(\mathsf {A}\) from the same figure, with the observational refinement relation \(R_O = \{(0,6), (5,7), (2,8), (0,9), (3,10), (0,11), (3,12)\}\). The disjunctive cone \(\mathsf {C_6^1}\) refines the DT \(\langle 0,V \rangle \in {\mathsf A}\), where \(V = \{(b,2),(\tau ,1),(c,3)\}\). The set of \(\tau \)-paths of \(\mathsf {C_6^1}\) consists of the transition \(6\mathop {\longrightarrow }\limits ^{\tau }9\). Both (0, 6) and (0, 9) belong to \(R_O\) as required by Condition \({\mathsf 2.}\)(a) of Definition 12. Condition \({\mathsf 2.}\)(b) of Definition 12 also holds: from state 6 there exists a DT with leg (b, 8) refining V, and from state 9 the leg (c, 10) refines V as well.

3.2 Compatibility with Existing Definitions

We verify the validity of Definition 12 by proving a few theorems that ensure its compatibility with the relevant definitions from Sect. 2. The proofs of all theorems are given in the Appendix.

Theorem 1 ensures our definition agrees with observational implementation refinement for DMTSs.

Theorem 1

(Compatibility with Observational Implementations). Let M be a DMTS and I be an LTS. I is an observational implementation of M (Definition 7) if and only if it is an observational refinement of M (Definition 12).

For DMTSs with no \(\tau \)-transitions, Theorem 2 indicates that our definition agrees with strong refinement of DMTSs (Definition 6).

Theorem 2

(Compatibility with Strong Refinement). Let M and N be two \(\tau \)-free DMTSs. Then \(M \preceq _{\mathrm {S}}N\) if and only if \(M \preceq _{\mathrm {O}}N\).

Next, since DMTSs extend MTSs, we need to make sure that observational refinement for DMTSs agrees with the one for MTSs.

Theorem 3

(Compatibility with the MTS Refinement). Let M and N be MTSs. Then \(M \preceq _{\mathrm {o}}N\) (Definition 4) if and only if \(M \preceq _{\mathrm {O}}N\) (Definition 12).

Finally, Theorem 4 is the main result of this section, stating that our definition is in fact sound, that is, if N refines M according to Definition 12, then the set of implementations of N is included in the set of implementations of M.

Theorem 4

(Soundness). If \(M \preceq _{\mathrm {O}}N\) then \([\![ N ]\!]\) \(\subseteq \) \([\![ M ]\!]\).

Note that an observational refinement relation for DMTS cannot be complete with respect to implementations. This is because the definition must be compatible with strong refinement and with MTS refinement, and thus the simple examples showing non-completeness for MTSs [16] hold in this case as well.

4 DMTS Merge Under Observational Semantics

In this section, we examine the question of DMTS merge in light of the new modal observational refinement semantics. DMTSs were shown to be closed for merge under strong refinement semantics [4]. We show that DMTSs are closed under observational merge as well.

In order for two DMTSs to be merged, the models must be consistent, that is, they must have at least one common observational implementation. The algorithm for merging two DMTSs is based on a consistency relation between the states of the models to be merged. States m and n are in a consistency relation if for each DT \(\langle m,V \rangle \), at least one leg in V has a corresponding possible transition from n (possibly after a finite sequence of possible \(\tau \)-transitions) and vice versa:

Definition 13

(Observational DMTSs Consistency Relation (based on [4])). An observational consistency relation between DMTSs \(M = (S_M, L_\tau , \delta ^p_M, \varDelta ^r_M, m^0)\) and \(N=(S_N, L_\tau ,\delta ^p_N, \varDelta ^r_N, n^0)\) is a relation \(\mathcal{C}\subseteq S_M\times S_N\) s.t. \((m^0,n^0) \in \mathcal{C}\) and \(\forall (m,n)\in \mathcal{C}\), the following holds:

  1. 1.

    \(\forall \langle m,V \rangle \in \varDelta _M^r\), \(\exists (l,m^\prime )\in V\) and a sequence of possible transitions \(n_0 \mathop {\longrightarrow _{p}}\limits ^{\tau } n_1\mathop {\longrightarrow _{p}}\limits ^{\tau } \cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } n_j \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} n'\) in N such that \((m,n_i)\in \mathcal{C}\) for \(0\le i\le j\), and \((m^\prime , n^\prime )\in \mathcal{C}\); and

  2. 2.

    \(\forall \langle n,U \rangle \in \varDelta _N^r\), \(\exists (\ell ,n^\prime )\in U\) and \(m_0 \mathop {\longrightarrow _{p}}\limits ^{\tau } m_1\mathop {\longrightarrow _{p}}\limits ^{\tau } \cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } m_j \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} m'\) in M such that \((m_i,n)\in \mathcal{C}\) for \(0\le i\le j\) and \((m^\prime , n^\prime )\in \mathcal{C}\).

Based on a consistency relation \(\mathcal C\) between M and N, we can now merge them into a single DMTS that represents models that are common to both. The composition is done by constructing, for each DT \(\langle m,V \rangle \) in M (or N), a corresponding DT \(\langle p,W \rangle \) in the merged model P, where a leg \((\ell ,p')\) exists in W whenever (i) \((\ell ,m')\) exists in V, (ii) a sequence of transitions \(n_0 \mathop {\longrightarrow _{p}}\limits ^{\tau } n_1\mathop {\longrightarrow _{p}}\limits ^{\tau } \cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } n_j \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} n'\) is possible in N, such that \((m,n_i)\in \mathcal{C}\) for \(0\le i\le j\), and (iii) \((m',n')\in \mathcal{C}\).

Definition 14

(Merge (based on [4])). Let M and N be DMTSs with the same vocabulary L, and let \(\mathcal C\) be a consistency relation between them. The \(+\) operator between M and N is defined as \([M+ N]_\mathcal{C} = (\mathcal{C},L_\tau ,\delta ^p_{M+N},\varDelta ^r_{M+N}, (m^0,n^0)) \). \(\delta ^p_{M+N}\) and \(\varDelta ^r_{M+N}\) are defined to be the smallest relations that satisfy the following rules:

$$\begin{aligned} \begin{array}{ll} (RP) &{} \frac{\langle m,V \rangle }{\langle (m,n), W \rangle }, where \, W = \{(l, (m^\prime ,n^\prime ))\ | \ (l,m^\prime )\in \, \wedge \\ &{} n \mathop {\longrightarrow _{p}}\limits ^{\tau } n_1\mathop {\longrightarrow _{p}}\limits ^{\tau } \cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } n_j \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} n' \, in \, N, \wedge (m,n_j)\in \mathcal{C} \wedge (m^\prime ,n^\prime )\in \mathcal{C} \}\\ (PR) &{} \frac{ \langle n,U \rangle }{\langle (m,n), W \rangle }, where \, W = \{(l, (m^\prime ,n^\prime ))\ | \ (l,n^\prime )\in U \; \wedge \\ &{} m \mathop {\longrightarrow _{p}}\limits ^{\tau } m_1\mathop {\longrightarrow _{p}}\limits ^{\tau } \cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } m_k \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} m' \, in \, M, \wedge (m_j,n)\in \mathcal{C} \wedge (m^\prime ,n^\prime )\in \mathcal{C} \}\\ (PP1) &{} \frac{m\mathop {\longrightarrow _{p}}\limits ^{\ell } m^\prime , \ n \mathop {\longrightarrow _{p}}\limits ^{\tau } n_1\mathop {\longrightarrow _{p}}\limits ^{\tau } \cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } n_j \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} n' \wedge (m_j,n)\in \mathcal{C} \wedge (m^\prime ,n^\prime )\in \mathcal{C} }{ (m,n) \mathop {\longrightarrow _{p}}\limits ^{\ell } (m^\prime ,n^\prime )} \\ (PP2) &{} \frac{n\mathop {\longrightarrow _{p}}\limits ^{\ell } n^\prime , \ m \mathop {\longrightarrow _{p}}\limits ^{\tau } m_1\mathop {\longrightarrow _{p}}\limits ^{\tau } \cdots \mathop {\longrightarrow _{p}}\limits ^{\tau } m_k \mathop {\longrightarrow _{p}}\limits ^{\hat{\ell }} m' \wedge (m,n_j)\in \mathcal{C} \wedge (m^\prime ,n^\prime )\in \mathcal{C} }{ (m,n) \mathop {\longrightarrow _{p}}\limits ^{\ell } (m^\prime ,n^\prime )} \end{array} \end{aligned}$$

The difference between the above definition and the one in [4] is in the treatment of the \(\tau \)-transitions (just like the difference between the strong and the observational refinement). When constructing a DT \(\langle (m,n),W \rangle \in [M+ N]_\mathcal{C}\) that corresponds to a DT \(\langle m,V \rangle \in M\) (rule RP), we skip \(\tau \)-transitions in N that lead to an appropriate transition corresponding to a leg in V. The skipped \(\tau \)-transitions are instead considered by rule PR when a DT in \([M+ N]_\mathcal{C}\) is introduced for N.

Fig. 2.
figure 2

\(\mathsf H\) is an observational merge of \(\mathsf F\) and \(\mathsf G\). The nodes of \(\mathsf H\) are labelled with pairs of the consistency relation between \(\mathsf F\) and \(\mathsf G\).

Full size image

Example 3

Consider DMTSs \(\mathsf F\) and \(\mathsf G\) from Fig. 2. The two models are consistent, with the maximal consistency relation \(\mathcal{C} = \{ (0,5),(3,5),(4,6),(0,7),(1,8),\) \((2,8) \}\). DMTS \(\mathsf H\) is their merge. It includes two DTs, one corresponding to the single DT of \(\mathsf F\) (constructed by the RP rule), and the other – corresponding to the DT of \(\mathsf G\) (constructed by the PR rule).

When \(\mathcal C\) is the largest consistency relation between M and N, the composition \([M+ N]_\mathcal{C}\) becomes the merge of M and N. We state that formally below.

Theorem 5

(Correctness of Observational DMTS Merge). Let M and N be DMTSs with the same vocabulary. If \(\mathcal C\) is the largest consistency relation between the states of M and N, then \([M+ N]_\mathcal{C}\) is the LCR of M and N.

5 No MCR Under Alphabet Refinement

We now look at the merge of two models that are defined over different alphabets. In such a case, we deal with the alphabet merge, that is, we use the alphabet refinement (Definition 9) to determine if a model P is a common refinement of models M and N. In [3], we showed that DMTSs are not closed for merge under thorough alphabet refinement. Since modal refinement is sound with respect to implementations, this implies non-closure of merge w.r.t. modal alphabet refinement as well. Thus the question of the existence of an LCR is answered negatively. What about an MCR? Recall that the existence of an LCR implies the existence of an MCR, but the opposite direction does not hold. Can the merge of two DMTSs be represented as a set of minimal common refinements \(P_1, P_2, \cdots \) such that no other common refinement is strictly less refined than them? In this section, we answer the MCR question negatively as well.

What makes alphabet merge different from strong and observational ones is the fact that different types of refinements are mixed together. Let M and N be DMTSs over the alphabets \(L_M\) and \(L_N\), respectively, with no \(\tau \)-transitions. A common refinement P of M and N is defined over the alphabet \(L_M \cup L_N\). We then use hiding and observational refinement to compare P to M and N. Let Q be another common refinement of M and N. Note that P and Q are now defined over the same alphabet, and if no \(\tau \)-transitions exist, we use strong refinement to compare them. Thus, transitions in P that were considered unobservable when a relation was defined between P and M, are treated as observable in a refinement relation between P and Q. While the number of \(\tau \)-transitions for the observational refinement does not matter, as long as the sequence is finite, this number does matter for strong refinement. This difference makes it impossible to find a minimal common alphabet refinement, as we show in this section.

In Sect. 5.1, we introduce two lemmas proven in the Appendix. We use them to prove the main theorem in Sect. 5.2.

5.1 Facts About Strong Refinement

We examine a strong refinement relation between two DMTSs, and show that a sequence of possible transitions is preserved under such a relation, and so does a sequence of required transitions.

Definition 15

(Maybe Path). Let \(M=(S_M, L_\tau , \delta ^p, \varDelta ^r, s_m)\) be a DMTS and \(y, y^\prime \in S_M\) be states. A sequence of possible transitions \(y \mathop {\longrightarrow _{p}}\limits ^{l_1} y_1 \mathop {\longrightarrow _{p}}\limits ^{l_2} ... \mathop {\longrightarrow _{p}}\limits ^{l_{i-1}} y_{i-1}\mathop {\longrightarrow _{p}}\limits ^{l_{i}} y^\prime \) in M is called a maybe path of length i from y to \(y^\prime \).

Lemma 1

Let \(M=(S_M, L_\tau , \delta ^p, \varDelta ^r, s_m)\) and \(N=(S_N, L_\tau , \delta ^p, \varDelta ^r, s_n)\) be DMTSs such that \(M \preceq _{\mathrm {S}}N\), with a strong refinement relation \(R_S\). Let \((m,n)\in R_S\). Let \(y_1 \in S_N\) be a state in N. If there exists a maybe path from n to \(y_1\) of length i in N, then there must exist a state \(x_1\in S_M\) and a maybe path of length i from m to \(x_1\) such that \((x_1,y_1)\in R_S\).

Let \(C_x\) be a disjunctive cone. States with no outgoing DTs in \(C_x\) are called front states. We denote the set of front states of \(C_x\) by \(F_{C_x}\). The depth of a disjunctive cone is the length of the longest maximal must path in \(C_x\) (see Definition 10). Note that if \(C_x\) is of depth \(i<\infty \), then all maximal must paths in \(C_x\) are finite, and each of them ends in a front state of \(C_x\).

Example 4

Consider the disjunctive cone \(C_6^1\) in Fig. 1 (Sect. 3.1). Its depth is 2, and its set of front states is \(F_{C_6^1} = \{8,10\}\).

Lemma 2

Let \(M=(S_M, L, \delta ^p, \varDelta ^r, s_m)\) and \(N=(S_N, L, \delta ^p, \varDelta ^r, s_n)\) be DMTSs such that \(M \preceq _{\mathrm {S}}N\) with the strong refinement relation \(R_S\). Let \((m,n)\in R_S\). Let \(C_m\) be a disjunctive cone from m of depth \(i<\infty \), and let \(F_{C_m}\) be the set of front states in \(C_m\). Then there exists a must path \(\pi \) from n to a state \(y\in S_N\) and there exists a state \(x\in F_{C_m}\), such that \((x,y)\in R_S\) and \(|\pi |\le i\).

5.2 No MCR

We now prove the main result of the section, stated in the theorem below.

Theorem 6

Consistent DMTSs do not always have a minimal common alphabet refinement.

In order to prove this theorem we introduce two very simple DMTSs, \({\mathsf D}\) and \({\mathsf E}\), shown in Fig. 3. They are consistent with each other and have many common alphabet refinements, yet they do not have an MCR, as we prove below.

Fig. 3.
figure 3

Two DMTSs \({\mathsf D}\) and \({\mathsf E}\) that do not have an MCR. \({\mathsf M}\) is an example of an alphabet common refinement of \({\mathsf D}\) and \({\mathsf E}\), and \({\mathsf C_3}\subset {\mathsf M}\) is a disjunctive cone.

Full size image

Let us first study the nature of a common alphabet refinement \({\mathsf M}\) of \({\mathsf D}\) and \({\mathsf E}\). Since \({\mathsf D} \preceq _{\mathrm {A}}{\mathsf M}\), all states in \({\mathsf M}\) correspond, in the observational alphabet relation, to either \({\mathsf D_0}\) or \({\mathsf D_1}\). We call them 0-states and 1-states, respectively. 0-states in \({\mathsf M}\) are those that appear before a transition labeled b on a path from the initial state. 1-states in \({\mathsf M}\) appear after a transition labeled b. 0-states and 1-states cannot be related via the observation alphabet relation since from a 0-state we eventually reach a b-labelled transition, while from a 1-state such a transition cannot be reached. We thus have the following observation.

Observation 1

Let \({\mathsf M}\) and \({\mathsf N}\) be common refinements of \({\mathsf D} \) and \({\mathsf E}\) such that \({\mathsf M} \preceq _{\mathrm {S}}{\mathsf N}\) with the refinement relation \(R_S\). For every \((x,y)\in R_S\), either both x and y are 0-states, or they are both 1-states.

From every 0-state x, a 1-state is guaranteed to be reached. Otherwise, x cannot correspond to \({\mathsf D_0}\) since there is a required transition on b from \({\mathsf D_0}\). An observational refinement allows a finite number of \(\tau \)-transitions to exist, after which a required transition on b must be present. Thus, from every 0-state x, there must exist a DT such that all of its legs lead, without loops, to a 1-state.

Observation 2

Let \({\mathsf M}\) be a common refinement of \({\mathsf D} \) and \({\mathsf E}\). From every 0-state in \({\mathsf M}\) there must exist a DT such that none of its legs form a loop on c-labelled transitions.

Otherwise, there is a refinement of x that does not reach a 1-state. More formally, we have the following claim.

Claim 1

From every 0-state x in \({\mathsf M}\), there exists a disjunctive cone \(C_x\) with finite maximal must paths such that all of its front states are 1-states.

Proof

Assume by way of contradiction that there exists a 0-state x such that for all disjunctive cones starting from x, at least one front state is a 0-state. Let us examine a maximal such disjunctive cone \(C_x\), in the sense that no DT can be added from any front state s (either because a DT does not exist from s or because adding any DT will form a directed loop). Then s contradicts Observation 2.    \(\square \)

Example 5

DMTS \({\mathsf M}\) in Fig. 3 is a common alphabet refinement of \({\mathsf D}\) and \({\mathsf E}\). Its 0-states are 3,5,8 and its 1-states are 4,6,7,9. DMTS \({\mathsf C_3}\) is a disjunctive cone for which all of its front states are 1-states. By Claim 1, such a disjunctive cone must exist in every common alphabet refinement of \({\mathsf D}\) and \({\mathsf E}\).

Based on the above observations and Claim 1, we can now prove Theorem 6. The idea of the proof is to construct, for any given common refinement \({\mathsf M}\) of \({\mathsf D}\) and \({\mathsf E}\), a common refinement \({\mathsf M^\prime }\) that is strictly less refined than \({\mathsf M}\) (\({\mathsf M^\prime } \preceq _{\mathrm {S}}{\mathsf M}\) and \({\mathsf M} \not \preceq _{\mathrm {S}}{\mathsf M^\prime }\)). This would show that no common refinement can be minimal.

Proof of Theorem 6. Let \({\mathsf M}=(S_M, L, \delta ^p, \varDelta ^r, s^m)\) be a common alphabet refinement of \({\mathsf D}\) and \({\mathsf E}\). We construct a less refined common alphabet refinement \({\mathsf M}^\prime \). We first examine disjunctive cones C in \({\mathsf M}\), from 0-states, with front states that are 1-states. By Claim 1, such a disjunctive cone exists from every 0-state. Let \(\mathcal{DC}\) be the set of all such disjunctive cones in \({\mathsf M}\):

$$ \mathcal{DC} = \{C_x\ | \ x \text{ is } \text{ a } \text{0-state },\ C_x \ \text{ is } \text{ a } \text{ disjunctive } \text{ cone } \text{ where } F_{C_x} \text{ has } \text{ only } \text{1-states }\}$$

Consider the depth \(| C_x |\) of disjunctive cones in \(\mathcal{DC}\). Let \(k_1 = max \{|C_x| \ |\ C_x \in \mathcal{DC}\}\). Let \(k = 2k_1\). We now construct \({\mathsf M}^\prime = (S_M', L, \delta ^{\prime p}, \varDelta ^{\prime r}, s^\prime _m)\) as follows:

  • we define \(s^\prime _m = s_m\);

  • we add k states: \(S_M' = S_M \cup \{y_1,\cdots , y_k\}\);

  • we add k possible transitions to \(\delta ^p\): \(\delta ^{\prime p} = \delta ^{p} \cup \{s^\prime _m\mathop {\longrightarrow _{p}}\limits ^{c} y_1 \mathop {\longrightarrow _{p}}\limits ^{c} y_2 \mathop {\longrightarrow _{p}}\limits ^{c} \cdots \mathop {\longrightarrow _{p}}\limits ^{c} y_k\}\);

  • and we add k required transitions to \(\varDelta ^r\): \(\varDelta ^{\prime r} = \varDelta ^{r} \cup \{y_k\mathop {\longrightarrow _r}\limits ^{c} y_{k-1} \mathop {\longrightarrow _r}\limits ^{c} \cdots \mathop {\longrightarrow _r}\limits ^{c} y_1 \mathop {\longrightarrow _r}\limits ^{c} s^\prime _m\}.\)

Clearly, \({\mathsf M^\prime }\) is a common alphabet refinement of \({\mathsf D}\) and \({\mathsf E}\): all new states are 0-states. Also, \({\mathsf M}\) refines \({\mathsf M^\prime }\) by removing the transition \(s_m\mathop {\longrightarrow _{p}}\limits ^{c} y_1\). Thus, \({\mathsf M^\prime } \preceq _{\mathrm {S}}{\mathsf M}\).

It remains to be shown that \({\mathsf M} \not \preceq _{\mathrm {S}}{\mathsf M^\prime } \). Assume by way of contradiction that \({\mathsf M} \preceq _{\mathrm {S}}{\mathsf M^\prime }\). Thus, there exists a refinement relation \(R_S\) between \({\mathsf M}\) and \({\mathsf M^\prime }\) such that \((s_m,s^\prime _m)\in R_S\). In \({\mathsf M^\prime }\), there is a maybe path from \(s^\prime _m\) to \(y_k\) (by construction). By Lemma 1, there exists a maybe path in \({\mathsf M}\) from \(s_m\) to a state x, and \((x,y_k)\in R_S\). Since \(y_k\) is a 0-state, and x is related to \(y_k\), we have by Observation 1 that x is also a 0-state. By Claim 1, there exists a disjunctive cone \(C_x\) in \({\mathsf M}\) from x, such that all its front states are 1-states. Let i be the depth of \(C_x\). We know that \(i \le k_1\) (by the definition of \(k_1\)). Since \((x,y_k)\in R_S\), by Lemma 2, there exists a must path \(\pi \) from \(y_k\) to a 1-state in \({\mathsf M}^\prime \) with \(|\pi |\le i\). However, by our construction, the shortest must path in \({\mathsf M^\prime }\) from \(y_k\) to a 1-state is of length \(k+1\) (k transitions to get back from \(y_k\) to \(s_m^\prime \) and at least another b-labelled transition to get to a 1-state). Recall that \(k= 2k_1\). We get that \(|\pi |\le i \le k_1\) but also \(|\pi | > 2k_1\) – a contradiction.    \(\square \)

6 Conclusion

In this paper, we revisited DMTSs and added a few pieces to the puzzle of their analysis. We defined DMTS modal observational refinement, a definition that was missing in the literature. We then used this definition to show that DMTSs are closed under observational merge, but that for the alphabet merge, even a minimal common refinement cannot be found.

In [3], we introduced a new formalism, rDMTS, and characterized the class of rDMTSs that are closed for alphabet merge. Since no modal observational refinement existed at that time, we defined merge using thorough refinement. We plan to extend the theory of rDMTSs to support modal alphabet refinement as well. This will provide the first practical solution for merging of models defined over different alphabets, since the complexity of modal refinement is much lower than that of thorough (PTIME-complete vs. EXPTIME-complete [6]).