Query Checking for Linear Temporal Logic

TitleQuery Checking for Linear Temporal Logic
Publication TypeConference Paper
Year of Publication2017
AuthorsHuang, Samuel, and Cleaveland Rance
Date Published25 August 2017
PublisherSpringer, Cham
ISBN Number978-3-319-67113-0

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.