A.: On modal refinement and consistency

Abstract. Almost 20 years after the original conception, we revisit sev-eral fundamental questions about modal transition systems. First, we demonstrate the incompleteness of the standard modal refinement us-ing a counterexample due to Hüttel. Deciding any refinement, complete with respect to the standard notions of implementation, is shown to be computationally hard (co-NP hard). Second, we consider four forms of consistency (existence of implementations) for modal specifications. We characterize each operationally, giving algorithms for deciding, and for synthesizing implementations, together with their complexities. 1 Background and Overview Modal transition systems (MTSs) are a generalization of labeled transition sys-tems (LTSs). Similarly to LTSs modal transition systems use labeled transitions between states to model behaviors. Unlike LTSs, they distinguish allowed and required behaviors (over- and under-approximations), which makes them a suit-able semantic model for abstraction in program analysis and verification