Symbolic partition refinement with automatic balancing of time and space