Query Checking for Linear Temporal Logic

The query-checking problem for temporal logic may be formulated as follows. Given a Kripke structure M and a temporal-logic query of form ϕ[var]ϕ[var], which may be thought of as a temporal formula with a missing propositional subformula varvar, find the most precise propositional formula f that, when substituted for varvar in ϕ[var]ϕ[var], ensures M satisfies the resulting temporal property. Query checking has been used for system comprehension, specification reconstruction, and other related applications in the formal analysis of systems.

In this paper we present an automaton-based methodology for query checking over linear temporal logic (LTL). While this problem is known to be hard in the general case, we show that by exploiting several key observations about the interplay between the input model M and the query ϕ[var]ϕ[var], we can produce results for many problems of interest. In support of this claim, we report on preliminary experimental data for an implementation of our technique.