Modal and Mixed Specifications: Key Decision Problems and their Complexities

Modal and mixed transition systems are specification formalisms that allow mixing of
over- and under-approximation. We discuss three fundamental decision problems for
such specifications: whether a set of specifications has a common implementation,
whether a sole specification has an implementation, and whether all implementations of
one specification are implementations of another one. For each of these decision problems
we investigate the worst-case computational complexity for the modal and mixed case.
We show that the first decision problem is EXPTIME-complete for modal as well as for
mixed specifications. We prove that the second decision problem is EXPTIME-complete
for mixed specifications (while it is known to be trivial for modal ones). The third
decision problem is furthermore demonstrated to be EXPTIME-complete for mixed
specifications.