This paper presents two frameworks for abstraction-refinement in model checking. The first one handles ACTL specification. The abstraction is conservative for ACTL verification, but not for falsification. Spurious counterexamples in the abstract model are used to guide a refinement that eliminates these counterexamples.
The other framework handles full CTL. On abstract models, CTL formulas are interpreted with respect to the 3-valued semantics and can be evaluated to either true, false, or the indefinite value ⊥. The abstraction is conservative for CTL verification as well as falsification. Only if a formula is evaluated to ⊥ in the abstract model, its value in the concrete model is unknown and refinement is needed. However, now the goal of the refinement is to eliminate indefinite results and to turn them into either definite true or definite false.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com