Automated Abstraction-Refinement of Hybrid Automata for Monotonic CTL Model Checking