Variants of LTL Query Checking

Hana Chockler*, Arie Gurfinkel, Ofer Strichman

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapter

8 Citations (Scopus)


Given a model M and a temporal logic formula phi[?], where ? is a placeholder. the query checking problem, as defined for the case of CTL by Chan in 2000, is to find the strongest propositional formula f such that M satisfies phi[? -> f]. The motivation for solving this problem is. among other things, to get insight on the model.

We consider various objectives to the LTL query-checking problem, and study the question of whether there is a better solution than simply enumerating all possible formulas (modulo logical equivalence). It turns out that in most cases the answer is no, but there is one particular objective for which the answer - in practice - is definitely yes. The solution is based on a reduction to a Pseudo-Boolean Solving problem.

Original languageEnglish
Title of host publicationHardware and Software: Verification and Testing
Subtitle of host publication6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers
EditorsS Barner, Harris, D Kroening, O Raz
Place of PublicationBERLIN
PublisherSpringer-Verlag Berlin Heidelberg
Number of pages17
ISBN (Print)978-3-642-19582-2
Publication statusPublished - 2011
Event6th Haifa Verification Conference - Haifa, Israel
Duration: 4 Oct 20107 Oct 2010

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference6th Haifa Verification Conference


Dive into the research topics of 'Variants of LTL Query Checking'. Together they form a unique fingerprint.

Cite this