Making abstract model checking strongly preserving

Usually, abstract model checking is not strongly preserving: it may well exist a temporal specification which is not valid on the abstract model but which is instead satisfied by the concrete model. Starting from the standard notion of bisimulation, we introduce a notion of completeness for abstract models: completeness together with a so-called partitioning property for abstract models implies strong preservation for the past μ-calculus. Within a rigorous abstract interpretation framework, we show that the least refinement of a given abstract model, for a suitable ordering on abstract models, which is complete and partitioning always exists, and it can be constructively characterized as a greatest fixpoint. This provides a systematic methodology for minimally refining an abstract model checking in order to get strong preservation.