Variants of LTL Query Checking

Hana Chockler; Arie Gurfinkel; Ofer Strichman

doi:10.1007/978-3-642-19583-9_11

Variants of LTL Query Checking

Hana Chockler^*, Arie Gurfinkel, Ofer Strichman

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter

8 Citations (Scopus)

Abstract

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 language	English
Title of host publication	Hardware and Software: Verification and Testing
Subtitle of host publication	6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers
Editors	S Barner, Harris, D Kroening, O Raz
Place of Publication	BERLIN
Publisher	Springer-Verlag Berlin Heidelberg
Pages	76-92
Number of pages	17
ISBN (Print)	978-3-642-19582-2
DOIs	https://doi.org/10.1007/978-3-642-19583-9_11
Publication status	Published - 2011
Event	6th Haifa Verification Conference - Haifa, Israel Duration: 4 Oct 2010 → 7 Oct 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	SPRINGER-VERLAG BERLIN
Volume	6504
ISSN (Print)	0302-9743

Conference

Conference	6th Haifa Verification Conference
Country/Territory	Israel
City	Haifa
Period	4/10/2010 → 7/10/2010

Access to Document

10.1007/978-3-642-19583-9_11

Cite this

Chockler, H., Gurfinkel, A., & Strichman, O. (2011). Variants of LTL Query Checking. In S. Barner, Harris, D. Kroening, & O. Raz (Eds.), Hardware and Software: Verification and Testing: 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers (pp. 76-92). (Lecture Notes in Computer Science; Vol. 6504). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-642-19583-9_11

Chockler, Hana ; Gurfinkel, Arie ; Strichman, Ofer. / Variants of LTL Query Checking. Hardware and Software: Verification and Testing: 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers. editor / S Barner ; Harris ; D Kroening ; O Raz. BERLIN : Springer-Verlag Berlin Heidelberg, 2011. pp. 76-92 (Lecture Notes in Computer Science).

@inbook{43edc857d7484ec38fe0669bc65dd89f,

title = "Variants of LTL Query Checking",

abstract = "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.",

author = "Hana Chockler and Arie Gurfinkel and Ofer Strichman",

year = "2011",

doi = "10.1007/978-3-642-19583-9_11",

language = "English",

isbn = "978-3-642-19582-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag Berlin Heidelberg",

pages = "76--92",

editor = "S Barner and Harris and D Kroening and O Raz",

booktitle = "Hardware and Software: Verification and Testing",

note = "6th Haifa Verification Conference ; Conference date: 04-10-2010 Through 07-10-2010",

}

Chockler, H, Gurfinkel, A & Strichman, O 2011, Variants of LTL Query Checking. in S Barner, Harris, D Kroening & O Raz (eds), Hardware and Software: Verification and Testing: 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers. Lecture Notes in Computer Science, vol. 6504, Springer-Verlag Berlin Heidelberg, BERLIN, pp. 76-92, 6th Haifa Verification Conference, Haifa, Israel, 4/10/2010. https://doi.org/10.1007/978-3-642-19583-9_11

Variants of LTL Query Checking. / Chockler, Hana; Gurfinkel, Arie; Strichman, Ofer.
Hardware and Software: Verification and Testing: 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers. ed. / S Barner; Harris; D Kroening; O Raz. BERLIN: Springer-Verlag Berlin Heidelberg, 2011. p. 76-92 (Lecture Notes in Computer Science; Vol. 6504).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

TY - CHAP

T1 - Variants of LTL Query Checking

AU - Chockler, Hana

AU - Gurfinkel, Arie

AU - Strichman, Ofer

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-19583-9_11

DO - 10.1007/978-3-642-19583-9_11

M3 - Chapter

SN - 978-3-642-19582-2

T3 - Lecture Notes in Computer Science

SP - 76

EP - 92

BT - Hardware and Software: Verification and Testing

A2 - Barner, S

A2 - Harris, null

A2 - Kroening, D

A2 - Raz, O

PB - Springer-Verlag Berlin Heidelberg

CY - BERLIN

T2 - 6th Haifa Verification Conference

Y2 - 4 October 2010 through 7 October 2010

ER -

Chockler H, Gurfinkel A, Strichman O. Variants of LTL Query Checking. In Barner S, Harris, Kroening D, Raz O, editors, Hardware and Software: Verification and Testing: 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers. BERLIN: Springer-Verlag Berlin Heidelberg. 2011. p. 76-92. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-19583-9_11

Variants of LTL Query Checking

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this