Issue No. 10 - October (2003 vol. 29)
Marsha Chechik , IEEE Computer Society
<p><b>Abstract</b>—Temporal logic query checking was first introduced by W. Chan in order to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol <tmath>?_1</tmath>, known as a placeholder. Given a Kripke structure and a propositional formula <tmath>\varphi</tmath>, we say that <tmath>\varphi</tmath> satisfies the query if replacing the placeholder by <tmath>\varphi</tmath> 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 a 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 <tmath>\chi\rm Chek</tmath>. 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.</p>
CTL, query checking, model checking, TLQSolver, model understanding, multi-valued logic.
A. Gurfinkel, M. Chechik and B. Devereux, "Temporal Logic Query Checking: A Tool for Model Exploration," in IEEE Transactions on Software Engineering, vol. 29, no. , pp. 898-914, 2003.