Temporal Logic Query Checking: A Tool for Model Exploration

Abstract

Temporal logic query checking was first introduced by William Chan to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol ?, known as a placeholder. Given a Kripke structure and a propositional formula p, we say that p satisfies the query if replacing the placeholder by p results in a temporal logic formula satisfied by the Kripke structure. A solution to a temporal logic query on a Kripke structure is the set of all propositional formulas that satisfy the query.

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.