## Heuristics for Hierarchical Partitioning with Applications to Model Checking

*Oliver Moller and Rajeev Alur*
Given a collection of connected components, it is often
desired to cluster together parts of strong correspondence,
yielding a hierarchical structure. We address the
automation of this process and apply heuristics to battle the
combinatorial and computational complexity.

We define a cost function that captures the quality of a structure relative to
the connections and favors shallow structures with a low degree of
branching. Finding a structure with minimal cost is
NP-complete. We present a greedy polynomial-time algorithm that creates
an approximative good solution incrementally by local evaluation of a
heuristic function.
We argue for a heuristic function based on four criteria:
the number of enclosed connections,
the number of components,
the number of touched connections and
the depth of the structure.

We report on an application in the context of formal verification, where our
algorithm serves as a preprocessor for a temporal scaling technique, called
* ``Next'' heuristic*. The latter is applicable in
reachability analysis and is included in a recent version of the Mocha
model checking tool.
We demonstrate performance and benefits of our method and use an asynchronous
parity computer
and an opinion-poll protocol
as case studies.

*11th Advanced Research Working Conference
on Correct Hardware Design and Verification Methods*
(CHARME'01), 2001.