Abstraction refinement by controllability and cooperativeness analysis