Temporal Logic Query Checking

A temporal logic query checker takes as input a Kripke structure and a temporal logic formula with a hole, and returns the set of propositional formulas that, when put in the hole, are satisfied by the Kripke structure. By allowing the temporal properties of a system to be discovered, query checking is useful in the study and reverse engineering of systems. Temporal logic query checking was first proposed in (2). In this paper, we generalize and simplify Chan's work by showing how a new class of alternating automata can be used for query checking with a wide range of temporal logics.