Comparing disjunctive modal transition systems with an one-selecting variant

An expressive class of abstractions for labeled transition systems is that of disjunctive modal transition systems (DMTS), featuring may- and must transitions as well as disjunctive hypertransitions (OR). In order to describe exclusive choice adequately, we develop a variant of DMTSs called 1-selecting modal transition systems (OMTS) that, roughly speaking, interprets hypertransitions exclusively (XOR). These abstract models, DMTSs and OMTSs, are compared with respect to their expressive power. By giving transformations or showing their non-existence, we show that the two setting can express the same sets of labeled transition systems, but 1-selecting modal transition systems have a richer refinement preorder.