Modal Transition System (MTS) is a well studied formal-
ism for partial model specification. It allows a modeller to distinguish
between required, prohibited and possible transitions. Disjunctive MTS
(DMTS) is an extension of MTS that has been getting attention in re-
cent years. A key concept for (D)MTS is
refinement
, supporting a devel-
opment process where abstract specifications are gradually refined into
more concrete ones. Refinement comes in different flavours:
strong
,
ob-
servational
(where
τ
-labelled transitions are taken into account), and
alphabet
(allowing the comparison of models defined on different alpha-
bets). Another important operation on (D)MTS is that of
merge
: given
two models
M
and
N
, their merge is a model
P
which refines both
M
and
N
, and which is the least refined one.
In this paper, we fill several missing parts in the theory of DMTS refine-
ment and merge. First and foremost, we define observational refinement
for DMTS. While an elementary concept, such a definition is missing
from the literature to the best of our knowledge. We prove that our defi-
nition is sound and that it complies with all relevant definitions from the
literature. Based on the new observational refinement for DMTS, we ex-
amine the question of DMTS merge, which was defined so far for strong
refinement only. We show that observational merge can be achieved as a
natural extension of the existing algorithm for strong merge of DMTS.
For alphabet merge however, the situation is different. We prove that
DMTSs do not have a merge under alphabet refinement.