Temporal logic query checking: A tool for model exploration

Arie Gurfinkel

doi:10.1109/TSE.2003.1237171

Temporal logic query checking: A tool for model exploration

2003-10-01

37

OA

AI

DOI：10.1109/TSE.2003.1237171

原文链接

原文求助

摘要

En 中文

Temporal logic query checking was first introduced by:W. Chain 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 ?(1), known as a placeholder. Given a Kripke, structure and a propositional formula phi, we say that phi satisfies the query if replacing the placeholder by phi 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 chiChek. 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.

Keyword:

CTL

query checking

model checking

TLQSolver

model understanding

multi-valued logic

Temporal logic query checking: A tool for model exploration

摘要

期刊

机构