context. There are also many relationships between action planning and model checking [30] and reﬁnement methods have 
been very successful in the latter case. Hoffmann et al. [54] suggested that reﬁnement is appropriate for proving that there 
is no solution, while heuristic search is better for ﬁnding solutions. This could explain why model checking focuses on re-
ﬁnement, while planning focuses on heuristic search. However, there is a recent trend in planning to consider also instances 
that may not have a solution [9,13,32,52], which can be expected to lead to a renewed interest in reﬁnement. Furthermore, 
even though heuristic search is usually not considered good for proving unsolvability, Hoffmann et al. [52] demonstrate that 
the merge-and-shrink heuristic [49] may sometimes be successfully applied also to this problem, which begs for a better 
understanding of the relationships between reﬁnement and heuristics. In addition, a number of new reﬁnement methods
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen