Paper: Temporal Logic Query Checking (at LICS 2001)

Authors: Glenn Bruns Patrice Godefroid

Abstract

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.

BibTeX

  @InProceedings{BrunsGodefroid-TemporalLogicQueryC,
    author = 	 {Glenn Bruns and Patrice Godefroid},
    title = 	 {Temporal Logic Query Checking},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {409--417},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }