This paper presents two frameworks for abstraction-refinement in model checking. The first is the CounterExample-Guided Abstraction-Refinement (CEGAR) which can verify universal fragments of temporal logics and is based on a 2-valued semantics of temporal logics. The other is the Three-valued Abstraction-Refinement (TVAR) and is based on a 3-valued semantics of these logics.
We also present an application of the 3-valued framework for fully automatic compositional model checking. Based on this and other successful applications of the 3-valued framework we conclude that the additional power it provides is worth the extra efforts of having non-standard definitions and algorithms.
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