In the twenty-five years since its invention, model checking has evolved into a powerful framework for the analysis of computer hardware and software. The integration of model checkers into the industrial development chain has raised new methodological questions about model checking, including the use of model checkers to analyze underspecified or unknown systems and the truthfulness of positive verification results. In this paper, we survey recent technical approaches to these questions – temporal logic query solving and vacuity detection – both of which transcend the classical picture of model checking. We focus on temporal logic queries with unique strongest solutions, describe fragments of CTL and LTL query languages with this property, a symbolic query solving algorithm for CTL, and an application of query solving to vacuity detection.
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