Monotonic Abstraction-Refinement for CTL

The goal of this work is to improve the efficiency and effectiveness of the abstraction-refinement framework for CTL over the 3-valued semantics. We start by proposing a symbolic (BDD-based) approach for this framework. Next, we generalize the definition of abstract models in order to provide a monotonic abstraction-refinement framework. To do so, we introduce the notion of hyper-transitions. For a given set of abstract states, this results in a more precise abstract model in which more CTL formulae can be proved or disproved.We suggest an automatic construction of an initial abstract model and its successive refined models. We complete the framework by adjusting the BDD-based approach to the new monotonic framework. Thus, we obtain a monotonic, symbolic framework that is suitable for both verification and falsification of full CTL.