Heuristics for Hierarchical Partitioning with Application to Model Checking

Resumé

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 shown to be NP-complete. We present a greedy
polynomial-time algorithm that creates an approximate good solution incrementally
by local evaluation of a heuristic function. We compare some simple heuristic
functions and argue for one 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 verication, where our
algorithm serves as a preprocessor for a temporal scaling technique, called \"ext" heuristic
[AW99]. The latter is applicable in enumerative reachability analysis and is included
in the recent version of the Mocha model checking tool.
We demonstrate performance and benefits of our method and use an asynchronous
parity computer, a standard leader election algorithm, and an opinion poll protocol as
case studies.