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.