Playing with Abstraction and Representation.

In this paper, we discuss partition refinement as an algorithmic pattern for explicating semantic properties of a system directly in the corresponding model structure in a co-inductive fashion. In particular, we review a landscape of analysis and verification approaches under this unifying perspective, which enables us to highlight their mutual profiles, while it at the same time establishes a basis for their combination: The common pattern establishes comparability, which reveals complementarity, and indicates where and under which circumstances the considered approaches may profit from one another. It can thus be regarded as a guideline for systematically exploring the benefits of the corresponding methods and their combinations.