Model Exploration with Temporal Logic Query Checking
A temporal logic query is a temporal logic formula with placeholders.
Given a model, a solution to a query is a set of assignments of
propositional formulas to placeholders, such that replacing the placeholders with
any of these assignments results in a temporal logic formula that
holds in the model. Query checking, first introduced by William
Chan, is an automated technique for finding solutions to
temporal logic queries. It allows discovery of the temporal properties
of the system and as such may be a useful tool for model exploration
and reverse engineering.
This paper describes an implementation of a temporal logic query
checker. It then suggests some applications of this tool, ranging
from invariant computation to test case generation, and illustrates
them using a Cruise Control System.