On Modal Refinement and Consistency
Source: Aalborg University
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.