Query checking helps discover temporal properties of the system, and as such is a useful tool for model exploration. In this paper, we show that query-checking is applicable to a variety of model exploration tasks, ranging from invariant computation to test case generation. We illustrate these using a Cruise Control System.
Additionally, we show that query checking is an instance of a
multi-valued model-checking of Chechik et al. This approach enables
us to build an implementation of a temporal logic query checker,
TLQSolver, on top of our existing multi-valued model-checker \Chi
Chek. It also allows us to decide a large class of queries and
introduce witnesses for temporal logic queries --- an essential
notion for effective model exploration.