Sixteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2001)

Paper: Temporal Logic Query Checking (at LICS 2001)

Authors: Glenn Bruns Patrice Godefroid


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.


    author = 	 {Glenn Bruns and Patrice Godefroid},
    title = 	 {Temporal Logic Query Checking},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2001},
    year =	 2001,
    editor =	 {Joseph Halpern},
    month =	 {June}, 
    pages =      {409--417},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}