Abstract
Given a model M and a temporal logic formula Φ[?], 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 = Φ[? ←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. © 2011 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Chockler, H., Gurfinkel, A., & Strichman, O. (2011). Variants of LTL query checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6504 LNCS, pp. 76–92). https://doi.org/10.1007/978-3-642-19583-9_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
