Topological Analysis of Refinement

AbstractA modal transition system has a class of implementations, its maximal refinements. This class determines satisfiability and validity judgments, and their compositional approximations, for formulas of Hennessy-Milner logic. Using topology, we prove structural properties of these judgments: refinement is reverse containment of classes of implementations, Hennessy-Milner logic characterizes refinement through validity judgments, implementation classes are topologically closed sets, Hennessy-Milner logic enjoys a compactness theorem on such classes, and a robust consistency measure between modal transition systems is definable. In particular, every formula of Hennessy-Milner logic is the finite disjunction of Hennessy-Milner logic formulas for which validity checks are reducible to model checks