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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aloul, F.A., Ramani, A., Markov, I.L., Saka llah, K.A.: PBS: A Backtrack-Search Psuedo-Boolean Solver and Optimizer. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT (2002)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 279–290. Springer, Heidelberg (1997)
Bruns, G., Godefroid, P.: Temporal logic query checking. In: LICS, pp. 409–417 (2001)
Chaki, S., Strichman, O.: Three optimizations for assume-guarantee reasoning with L*. J. on Formal Methods in System Design 32(3), 267–284 (2008)
Chan, W.: Temporal-Logic Queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450–463. Springer, Heidelberg (2000)
Chechik, M., Gurfinkel, A., Devereux, B.: χChek: A multi-valued model-checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 505. Springer, Heidelberg (2002)
Clarke, E.M., Draghicescu, I.A.: Expressibility results for linear-time and branching-time logics. In: Proc. Workshop on LTBTPO LNCS, vol. 354, pp. 428–437. Springer, Heidelberg (1988)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of PSTV, pp. 3–18 (1995)
Gurfinkel, A., Chechik, M., Devereux, B.: Temporal logic query checking: A tool for model exploration. IEEE Trans. Software Eng. 29(10), 898–914 (2003)
Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Second SPIN Workshop, pp. 23–32. AMS, Providence (1996)
Hornus, S., Schnoebelen, P.: On solving temporal logic queries. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 163–177. Springer, Heidelberg (2002)
Peled, D.: Software Reliability Methods. Springer, Heidelberg (2001)
Samer, M., Veith, H.: A syntactic characterization of distributive ltl queries. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1099–1110. Springer, Heidelberg (2004)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Thirioux, X.: Simple and efficient translation from LTL formulas to Buchi automata. Electronic Notes in Theoretical Computer Science 66(2), 145–159 (2002); FMICS 2002, 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems (ICALP 2002 Satellite Workshop)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. First IEEE Symp. Logic in Comp. Sci, pp. 332–344 (1986)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 110(2) (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chockler, H., Gurfinkel, A., Strichman, O. (2011). Variants of LTL Query Checking. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds) Hardware and Software: Verification and Testing. HVC 2010. Lecture Notes in Computer Science, vol 6504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19583-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-19583-9_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19582-2
Online ISBN: 978-3-642-19583-9
eBook Packages: Computer ScienceComputer Science (R0)