@inproceedings{MA:CHARME01,
  author = 	 {M{\"o}ller, M. Oliver and Alur, Rajeev},
  title = 	 {{H}euristics for {H}ierarchical {P}artitioning with {A}pplication to {M}odel {C}hecking},
  booktitle = 	 {{C}orrect {H}ardware {D}esign and {V}erification {M}ethods,
		 11th IFIP WG 10.5 Advanced Research Working Conference,
		 CHARME 2001, Livingston, Scotland, UK},
  publisher =    {Springer-Verlag Inc.},
  editor  =      {Tiziana Margaria and Tom Melham},
  series =       {Lecture Notes in Computer Science},
  volume =       {2144},
  address =      {New York, NY, USA},
  month =        sep,
  year = 	 {2001},
  pages = 	 {71--85},
  abstract = 	 {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 approximates good solutions
  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 [aw99]. 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.},
}