EXPTIME-complete Decision Problems for Modal and Mixed Specifications
Adam Antonik, Michael Huth, Kim G. Larsen, Ulrik Nyman, Andrzej Wąsowski · Electronic Notes in Theoretical Computer Science · 2009
Modal and mixed transition systems are formalisms that allow mixing of over- and under-approximation in a single specification. We show EXPTIME-completeness of three fundamental decision problems for such specifications: whether a set of modal or mixed specifications has a common implementation, whether a sole mixed specification has an implementation, and whether all implementations of one mixed specification are implementations of another mixed or modal one. These results are obtained by a chain of reductions starting with the acceptance problem for linearly bounded alternating Turing machines.