On Modal Refinement and Consistency

Almost 20 years after the original conception, the authors revisit several fundamental questions about modal transition systems. First, they demonstrate the incompleteness of the standard modal refinement using a counterexample due to Huttel. Deciding any refinement, complete with respect to the standard notions of implementation, is shown to be computationally hard (co-NP hard). Second, they consider four forms of consistency (existence of implementations) for modal specifications. They characterize each operationally, giving algorithms for deciding, and for synthesizing implementations, together with their complexities.