Temporal Logic Query Checking (Extended Abstract)

A temporal logic query checker takes as input a Kripke structure and a temporal logic formula with a hole, and returns that 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 [Cha00]. 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.